An accessibility proof of ordinal diagrams in intuitionistic theories for iterated inductive definitions
Toshiyasu Arai · Tsukuba Journal of Mathematics · 1984
ByToshiyasu ARAI Let $(I,$ $\prec)$ be a non-empty well-ordered system with the least element $0$ , and $\tilde{I}$ be $ I\cup t\infty$ } with the largest element $\infty$ .Let $A$ be a non-empty well-ordered set.Then 0(I, $A$ ) denotes the system of ordinal diagrams (o.d.'s) based on $I$ and A. (cf.[9, \S 26].)The accessibility proof for 0(I, $A$ ) in [9, pp.298-309] shows that every o.d.from $O(I, A)$ is accessible with respect to $<_{i}$ for every $i$ in $\tilde{I}$ . The central notions in this proof are i-fans and i-accessibility forRoughly speaking, an o.d.$\mu$ is an i-fan if for every $j\prec i$ and every j-section $ u$ of $\mu,$ $ u$ is j-accessible, and an $0.d$ . is i-accessible if it is accessible in i-fans with respect to $<_{i}$ .Consider the case when the order type of $(I,$ $\prec)$ is a successor ordinal $\xi+1$ .If we formalize this accessibility proof for $O(\xi+1,1)(=O(I, 1))$ naturally, then this proof can be done in the intuitionistic theory $ID_{\xi+1}^{i}$ for $\xi+1$ -times iterated inductive definitions.The purpose of this paper is to show the following fact: the accessibility of each o.d.from $O(\xi+1,1)$ with respect to $<_{0}$ is derivable in $ID_{\xi}^{i}$ .(Theorem) In the case when $\xi$ equals $\omega$ , this theorem will complement the consistency proof in [1] in the following sense.We will give in [1] a consistency proof for the subsystem $(\Pi_{1}1-CA)+(BI)$ of classical analysis by the accessibility of $0(\omega+1,1)$ with respect to $<_{0}$ .It follows from the well-known equivalence between the classical version $ID_{\omega}$ of $ID_{\omega}^{i}$ and $(\Pi_{1}1-CA)+(BI)$ that this consistency proof is optimal.The author is indebted