ИСТИНА

We consider extensions of the language of Peano arithmetic by iterated truth definitions satisfying uniform Tarskian biconditionals. Given a language \(L\) we add a new symbol \(T\) for a truth predicate and postulate the equivalence of each sentence \(A\) (obtained by substituting numerical parameters into a formula) with \(T(\#{}A)\) where \(\#{}A\) is the Gödel number of \(A\). This extension procedure can be repeated transfinitely many times. Without further axioms, such extensions are known to be weak and conservative over the original system of arithmetic. Much stronger systems, however, are obtained by adding either induction axioms or, more generally, reflection axioms on top of them. Theories of this kind can be used to interpret some well-known “predicative” fragments of second-order arithmetic such as iterated arithmetical comprehension. Feferman and Schuette studied related systems of ramified analysis and determined the ordinal \(\Gamma_0\) as the bound to transfinite induction provable in “predicative” systems. We obtain sharp results on the proof-theoretic strength of these systems using methods of provability logic, in particular, we calculate their proof-theoretic ordinals and conservativity spectra. We consider a semilattice of theories enriched by suitable reflection operators and isolate the corresponding strictly positive modal logic (reflection calculus) axiomatizing the identities of this structure. The variable-free fragment of the logic provides a canonical ordinal notation system for the class of theories under investigation. This setup allows us to obtain in a technically smooth way suitable conservativity relationships for reflection principles of various strength and, in particular, to obtain new proofs of several classical results in proof theory.