Reflection Algebras for Theories of Iterated Truth Definitions

摘要

We consider extensions of the language of Peano arithmetic by iterated truth definitions satisfying uniform Tarskian biconditionals. Given a first-order language L containing that of arithmetic one can add a new symbol T for a truth predicate and postulate the equivalence of each formula φ(x) of L with T(~┌φ(x)~┐) where ~┌φ(x)~┐ denotes the Goedel number of the result of substituting numeral for x into φ. This extension procedure can be repeated transfinitely many times. Without further axioms, such theories are known to be weak conservative extensions of the original system of arithmetic. Much stronger systems, however, are obtained by adding either induction axioms or reflection axioms on top of them. Theories of this kind can interpret some well-known predicatively reducible fragments of second-order arithmetic such as iterated arithmetical comprehension. Feferman and Schuette studied related systems of ramified analysis. They used their systems to explicate the intuitive idea of a predicative proof and determined the ordinal Γ_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 the semilattice of axiomatizable extensions of a basic theory of iterated truth definitions. We enrich the structure of this semilattice 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 conservativity relationships for iterated reflection principles of various strength which provide a sharp proof-theoretic analysis of our systems. Joint work with F. Pakhomov and E. Kolmakov. This work is supported by a grant of the Russian Science Foundation (project No. 16-11-10252).