A subsystem of clasical analysis proper Takeuti's reduction method for $\prod^{1}_{1}$-analysis
Toshiyasu Arai · Tsukuba Journal of Mathematics · 1985
AfterGentzen's works for the pure number theory, G. Takeuti gave consis- tency proofs of some impredicative subsystems of classical analysis in [5], [7], [8] and [9] ([9] with N. Yasugi).In these proofs, the only ' \"Uberschreitung' beyond the finitist standpoint in Hilbert's sense was the accessibility of some systems of 0. $d$ .$s$ (ordinal diagrams) which were also introduced by Takeuti in [4] and [6].Thus these works may be regarded as nice extensions of Gentzen's.But, unfortunately, it was not shown that the system ofIn this paper, we will propose a subsystem of classical analysis AII which is equivalent to SINN', and prove the consistency of AII by the accessibility of the system $0(\omega+1,1)$ with respect to $<_{0}$ , following Gentzen [2] and Takeuti [8].Also in [1], we will show that the transfinite induction up to each $0$ .$d$ .from the system $0(\omega+1,1)$ with respect to $<_{0}$ is derivable in AII.Thus we will complement Takeuti's consistency proof for $(\Pi_{1}1_{-}CA)+(BI)$ .In \S 1 the definition of AII and some preliminary definitions for a consistency proof will be given.In \S 2 the main lemma will be proved and from which to- gether with the accessibility of the system $0(\omega+1,1)$ with respect to $<_{0}$ , the consistency of AII follows immediately.The author is indebted to Dr. T. Yukami for the seminar under the guidance of him during the preparation of this paper.The author wishes to express his heart-felt thanks to Prof. N. Motohashi for reading this paper in manuscript and suggesting a number of linguistic improvements. \S 1. Preliminary DefinitionsIn this paper, we will use the terminology and notation in the same sense as those in [PT]. $*)$Usually this proof is said to be one for SINN which is equivrlent to $(\Pi_{2}^{2_{-}}CA)$ , but as remarked in [8], footnote 2, it is at the same time one for SINN'.