A consistency proof as system including Feferman's $ID_{\xi}$ by Takeuti's reduction method
Toshiyasu Arai · Tsukuba Journal of Mathematics · 1987
This paper is a sequel to our [1] and [2].Let $\prec$ be a $p.r$ .(primitive recursive) well-ordering on a p.r. subset of the set of natural numbers $N$ , with the least element $0$ and the largest element $\xi$ which is used to denote the order type of the initial segment of $\prec$ determined by $\xi$ .Let $\lambda x.x\oplus 1$ and $\lambda x.x\ominus 1$ be $p.r$ .successor and predecessor functions with respect to $\prec$ , respectively.Strictly speaking, we should suppose that some fixed p.r. definitions (indices) of $\prec,$ $\lambda x.x\oplus 1$ and $\lambda x.x\ominus 1$ are given instead of their graphs.And we will assume that formulae which express the above facts except the well-orderedness of $<$ by using p.r. definitions of $\prec,$ $\lambda x.x\oplus 1$ and $\lambda x.x\ominus 1$ , are all derivable in a weak fragment of arithmetic, say, primitive recursive arithmetic.A complete list of formulae which should be derivable for our purpose can be found in [1, p. 20].For such an ordering $\prec$ , we define a first order theory $AI_{\xi}^{-}$ .The lahgugage of the theory $AI_{\xi}^{-}$ is described as follows.Let $X$ be a unary predicate variable and $Y$ a binary one.For each arithmetical formula $\mathfrak{B}(X, Y, a, b)$ having no free variables except $X,$ $Y,$ $a$ and $b$ , we introduce a binary predicate constant $Q^{\mathfrak{B}}$ whose intended meaning is the disjoint union of the family $\{Q_{\zeta}^{\mathfrak{B}}\}_{C\prec\xi}$ , where $Q_{\zeta}^{\mathfrak{B}}$ $(\zeta\prec\xi)$ are subsets of $N$ defined by the following transfinite recursion on thewhere $Q_{\prec\zeta}^{\mathfrak{B}}$ is the disjoint union of the family $\{Q_{ u}^{\mathfrak{B}}\}_{ u\prec},$ .Then the theory $AI_{\xi}^{-}$ is obtained from the Peano Arithmetic PA in this language by adding an axiom scheme ( $Q\mathfrak{B}$ -initial sequent in 1. 41. 21, below) and an inference rule ( $Q\mathfrak{B}$ : right in 1. 41. 22, below) corresponding to the above mentioned meaning of $Q^{\mathfrak{B}}$As is expected, Feferman's theory $1D_{\xi}$ for the $\xi$ -times iterated inductive defi- nitions is interpretable in our $AI_{\text{\'{e}}}^{-}$ .This is shown in 1.In 2, we give a consistency proof of $AI_{\overline{\epsilon}}$ by the accessibility of the system of ordinal diagrams $O(\xi+1, 1)$ with respect to $<_{0}$ .This is done by Takeuti's