The \(\omega\)-consistency of elementary analysis (Q1375797)

Let EA be the formal system of elementary analysis. It was proved by \textit{K. Schütte} [Proof theory (1977; Zbl 0367.02012)] that we have a proof of the consistency of EA by transfinite induction up to \(\varepsilon_{\varepsilon_0}\). The purpose of this paper is to prove the following two theorems: Theorem 1. The \(\omega\)-consistency of EA can be proved by applying transfinite induction up to \(\varepsilon_{\varepsilon_1}\) for an elementary number theoretical proposition, together with exclusively elementary number theoretical techniques. Theorem 2. The \(\omega\)-consistency of EA cannot be proved by applying transfinite induction to numbers below \(\varepsilon_{\varepsilon_1}\) for the elementary number theoretical propositions, together with exclusively elementary number theoretical techniques. The proof of Theorem 1 is carried out in the same line as that of \(\omega\)-consistency of elementary number theory EN by \textit{Y. Hanatani} [Ann. Jap. Assoc. Philos. Sci. 3, 105-114 (1968; Zbl 0179.01401)], which is an application of \textit{G. Gentzen's} consistency proof of EN [Forsch. z. Logik u. z. Grundlegung d. exakt. Wiss. N.F. 4, 19-44 (1938; Zbl 0019.24103)].