Reflection algebras and conservation results for theories of iterated truth

TL;DR

This paper investigates the proof-theoretic strength of theories extending Peano arithmetic with iterated truth definitions, using provability logic to analyze conservativity, reflection principles, and ordinal notations.

Contribution

It introduces a canonical ordinal notation system based on reflection principles and establishes conservativity and proof-theoretic bounds for these theories.

Findings

Characterizes proof-theoretic ordinals of iterated truth theories.

Establishes conservativity relationships via reflection principles.

Provides a uniform analysis of proof-theoretic strength measures.

Abstract

We consider extensions of the language of Peano arithmetic by transfinitely iterated truth definitions satisfying uniform Tarskian biconditionals. Without further axioms, such theories are known to be 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. We obtain sharp results on the proof-theoretic strength of these systems using methods of provability logic. Reflection principles naturally define unary operators acting on the semilattice of axiomatizable extensions of our basic theory of iterated truth. The substructure generated by the top element of this algebra provides a canonical ordinal notation system for the class of theories under investigation. Using these notations we obtain conservativity relationships for iterated reflection principles of different logical complexity levels corresponding to the levels of the hyperarithmetical hierarchy, i.e., the analogs of Schmerl's formulas. These relationships, in turn, provide proof-theoretic analysis of our systems and of some related predicatively reducible theories. In particular, we uniformly calculate the ordinals characterizing the standard measures of their proof-theoretic strength, such as provable well-orderings, classes of provably recursive functions, and $\Pi_1^0$-ordinals.