Proof-theoretic investigations on Kruskal's theorem (Q1210137)

One idea of Reverse Mathematics is the following: In order to prove that a theorem \(\varphi\) cannot be derived in a theory Th, it is shown in a weak theory Tw that \(\varphi\) implies the well-foundedness of a denotation system Oz of ordinals, from which the consistency of Th can be inferred. In the paper under review \(\varphi\) is Kruskal's theorem, that the set of finite trees is a well-quasi-ordering with respect to embeddability. \textit{S. G. Simpson} showed [Arch. Math. Logik Grundlagenforsch. 25, 45-65 (1985; Zbl 0598.03045)], following H. Friedman, that this theorem implies the well-ordering of the system of all ordinals less than \(\Gamma_ 0\), the proof-theoretic ordinal of predicative analysis. And he remarks that on one hand there are even greater ordinals for which Kruskal's theorem provides a proof of their well-ordering, but on the other hand Kruskal's theorem can be proven in a system \(\Pi^ 1_ 2-\text{TI}_ 0\) with a certain larger proof-theoretical ordinal. In the paper under review the precise proof-theoretical strength of Kruskal's theorem is determined. It is expressed by the so-called Ackermann ordinal, which is written \(\vartheta\Omega^ \omega\) in the notation of the paper. This ordinal plays also an important role in terms of rewriting theory. Let \(\text{ACA}_ 0\) be the formal system with arithmetical comprehension. It is to be the weak theory Tw above. In the paper under review it is shown that in \(\text{ACA}_ 0\) the equivalence of Kruskal's theorem and \(\text{WF}(\vartheta\Omega^ \omega)\), the well-foundedness of the Ackermann ordinal, is derivable. Further it is proven that \(\vartheta\Omega^ \omega\) is the proof-theoretic ordinal of \((\Phi^ 1_ 2-\text{BI})_ 0\), the system \(\text{ACA}_ 0+ \Pi^ 1_ 2- \text{BI}\), \(\Pi^ 1_ 2-\text{BI}\) being the scheme \(\text{WF}(\prec)\Rightarrow\text{TI}(\prec,\varphi)\) for \(\prec\in\Pi^ 1_ 0\) and \(\varphi\in\Pi^ 1_ 2\). This means that in \((\Pi^ 1_ 2-\text{BI})_ 0\) it is not possible to derive either \(\text{WF}(\vartheta\Omega^ \omega)\) or the Theorem of Kruskal. In the system \((\Pi^ 1_ 2-\text{BI})\), which results from \((\Pi^ 1_ 2- \text{BI})_ 0\) by adding the schema of induction for formulas of second order arithmetic, \(\text{WF}(\vartheta\Omega^ \omega)\) is provable, but this system is even stronger, because its ordinal is \(\vartheta\Omega^{\varepsilon_ 0}\). The uniform reflexion principle for \((\Pi^ 1_ 2-\text{BI})_ 0\), \(\text{RFN}_{\Pi_ 1^ 1}((\Pi^ 1_ 2-\text{BI})_ 0)\), possesses the same strength as Kruskal's theorem. This means \[ \forall n(\text{Pr}_{(\Pi_ 2^ 1- \text{BI})_ 0}(\text{gn}(\varphi(\bar n))\Longrightarrow\varphi(n)), \] where \(\varphi\) is a \(\Pi^ 1_ 1\)-formula with at most one free variable, \(\text{Pr}_{(\Pi_ 2^ 1-\text{BI})_ 0}\) is the \(\Sigma^ 0_ 1\)-provability predicate which expresses provability in \((\Pi^ 1_ 2-\text{BI})_ 0\), \(\bar n\) is the formal term corresponding to the natural number \(n\), and \(\text{gn}(\varphi)\) is the Gödel number of \(\varphi\). The stated results are proved more or less in detail. The denotation systems of ordials used are comprehensively described. For determining the proof-theoretic ordinals, the proven method is applied to embedding the system to be investigated into a semi-formal system with \(\Omega\)- rule whose ordinal can be calculated by well-known means. This procedure also allows the determination of proof-theoretic ordinals for \(\text{ACA}_ 0+\Pi^ 1_ n-\text{BI}\) with \(n>2\).