An ordinal analysis for theories of self-referential truth (Q2267754)

In order to make sense of paradoxes about truth, basically three routes have been explored by different techniques: (i) restricting the expressiveness of the object language (Tarskian hierarchical approach); (ii) revising the underlying logic (e.g. adopting some substructural logic, many-valued logic, and so on); (iii) axiomatizing truth. In direction (iii), \textit{H. Friedman} and \textit{M. Sheard} wrote a seminal paper [Ann. Pure Appl. Logic 33, 1--21 (1987; Zbl 0634.03058)]: they isolated a base theory of truth (conservative over PA) and twelve natural principles about the truth predicate, the so called Optional Axioms (consisting of axioms, axiom schemata and rules of inference). As a main result, they completely classify all maximal consistent nine theories (named with capital letters from \(\mathcal{A}\) to \(\mathcal{I}\)), which consist of Optional Axioms over the base theory. The present work deals with an axiomatic investigation and offers a significant contribution by completing the proof-theoretic analysis of the theories of self-referential truth over Peano arithmetic PA, as introduced by Friedman and Sheard. Let \(S\equiv T\) stand for the statement that \(S\) and \(T\) have the same arithmetical consequences; let \(\text{ACA}_0\) be the subsystem of second-order arithmetic based on arithmetical comprehension and the axiom of mathematical induction. Then the Main Theorem 4.2 states the following equivalences: (i) \(\mathcal{A}\equiv \text{PA}\); (ii) \(\mathcal{B}\equiv \text{ACA}\equiv \mathcal{C}\) (ACA being \(\text{ACA}_0\) with full mathematical induction schema); (iii) \( \mathcal{D}\equiv \mathcal{G}\equiv \mathcal{I}\equiv \text{ACA}_0^+\) (\(\text{ACA}_0^+\) being \(\text{ACA}_0\) extended with the statement that, given any set \(X\) of numbers, the jump hierarchy above \(X\) along \(\omega\) exists); (iv) \( \mathcal{E}\equiv \mathcal{F}\equiv \Sigma^1_1\text{-DC}_0\) (\(\Sigma^1_1\text{-DC}_0\) being \(\text{ACA}_0\) extended with the dependent choice scheme for \(\Sigma^1_1\)-formulas of second-order arithmetic). Apparently, all systems involved are fully predicative (in the traditional Feferman-Schütte sense), ranging in terms of proof-theoretic ordinals from \(\varepsilon_0\) to \(\phi \omega 0\). The proofs involve clever applications of predicative infinitary methods and recursion-theoretic ideas. We underline that two of the systems involved -- though consistent -- are \(\omega\)-inconsistent. We also mention that the classifications suggest unexpected connections between formal semantics and countable combinatorics (see the examples mentioned by the authors at pp. 221--222).