A proof-theoretic account of classical principles of truth (Q385807)

It was 30 years ago when \textit{H. Friedman} and \textit{M. Sheard} made a systematic investion of axiomatic theories of the truth predicate over the basic theory PA, Peano Arithmetic [Ann. Pure Appl. Logic 33, 1--21 (1987; Zbl 0634.03058)]. In the past few years, the author and Rathjen have been extending the investigation in two directions: (1) the base logic is changed to intuitionistic, namely, HA, Heyting algebra, is used instead of PA, and (2) proof-theoretic ordinals of these theories and equivalent fragments of analysis (a.k.a. second-order arithmetic) are sought. (The pto (proof-theoretic ordinal) of a theory \(T\) is, by definition, the ordinal number \(\alpha\) such that \(T\) is conservative over PA\(+\) (transfinite induction up to \(\alpha\)).) The aim of this article is to find pto's of intuitionistic truth theories. The author begins by listing 15 principle about truth predicate, like \(A\to T(\ulcorner A\urcorner)\), \(T(\ulcorner A\urcorner)\vee T(\ulcorner\neg A\urcorner)\), and `from \(\neg A\) infer \(\neg T(\ulcorner A\urcorner)\)'. (Of course, one cannot put all these principles in one theory -- Liar's paradox.) Then, the list of 9 maximal consistent theories follows, labeled \(A^i\) through \(I^i\). (The super-script `\(i\)' indicates `intuitionistic'.) The conclusion shows that pto's do not change when the base logic is changed to intuitionistic from classical. So, the pto of \(A^i\) is \(\varepsilon_0\), \(B^i\) and \(C^i\) have \(\varepsilon_{\varepsilon_0}\) as their pto, \(D^i\), \(G^i\) and \(I^i\) share \(\phi_2(0)\), where \(\phi\) is the Veblen function, \(E^i\) and \(F^i\) have \(\phi_\Omega(0)\), and \(H^i\) has \(\psi_\Omega(\varepsilon_{\Omega+ 1})\), where \(\psi\) is the enumerating function of some critical set and \(\Omega\) is the Church-Kleene ordinal. These numbers are obtained by analysing the proof-theoretic strengths of truth theories by means of fragments of analysis. For instance, \(H^i\) is compared to the Kripke-Platek set theory over the natural numbers which is known to be equivalent to \(ID^i_1\) whose pto is known. The situation for \(A^i\), \(B^i\), \(C^i\), \(D^i\), and \(G^i\) are relatively simple. Theories \(E^i\), \(F^i\), and \(I^i\) are embedded into infinitary sequent calculi that have \(\omega\)-rules even within the predicate \(T(\,)\). Constructions of their Kripke \(\omega\)-rules are analysed in fragments of analysis, using various `slash relations', and asymmetric interpretation of truth. Thus, these proofs are much more complicated than the classical settings.