A consistency proof of a system including Feferman's ID_ by Takeuti's reduction method

This is a sequel to our earlier papers [ibid. 8, 209-218 (1984; Zbl 0564.03041) and ibid. 9, 21-29 (1985; Zbl 0612.03024)]. For a recursive ordinal \(\xi\), \(AI_{{\bar \xi}}\) denotes the first-order part of the theory \((\Pi \quad 1_ 1-CA)_{{\bar \xi}},\) second order arithmetic with the axiom of \(\xi\)-times iterated \(\Pi\) \(1_ 1\)-Comprehension Axiom. It is shown that cut-elimination theorem for \(AI_{{\bar \xi}}\)- derivations with \(\Sigma\) \(0_ 1\) end formula follows from the descending chain principle (d.c.p.) for the system of ordinal diagrams (o.d.'s) \(O(\xi +1,1)\) w.r.t. \(<_ 0\). The proof is a refinement of \textit{G. Takeuti}'s reduction method [Proof theory, 2nd ed. (1987; Zbl 0609.03019)]. Thus, a part of results due to \textit{W. Buchholz} and \textit{W. Pohlers} [in their joint book with \textit{S. Feferman} and \textit{W. Sieg}, Iterated inductive definitions and subsystems of analysis (1981; Zbl 0489.03022)] is proved in a different way. There are many misprints in this paper. In a forthcoming paper, we cut-eliminate for a logic calculus corresponding to second order arithmetic with axioms of \(\Pi\) \(1_ 2\)- Separation and Bar-induction by d.c.p. for a system of o.d.'s O(I) and show that for each o.d. \(\alpha <\Omega_ 1\) transfinite induction up to \(\alpha\) is derivable in Feferman's theory \(T_ 0\). Proofs are inspired by recent works of \textit{K. Schütte} and \textit{W. Buchholz} [Sitzungsber., Bayer. Akad. Wiss. Math.-Naturwiss. Kl. 1983, 99-132 (1984; Zbl 0573.03028)] and \textit{G. Jäger} [Arch. Math. Logik Grundlagenforsch. 23, 65-77 (1983; Zbl 0511.03025)].

Recommendations

Cited in

(9)

This page was built for publication: A consistency proof of a system including Feferman's \(ID_{\xi}\) by Takeuti's reduction method

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1100461)