An accessibility proof of ordinal diagrams
Gaisi Takeuti, Mariko Yasugi · Journal of the Mathematical Society of Japan · 1981
This is a sequel to our previous work [2], in which we defined the funda- mental sequences of ordinal diagrams.Here we conclude our first objective: an accessibility proof of ordinal diagrams.Let $S$ be a set with a linear ordering $<$ .An accessibility proof of the system $(S, <)$ is a "concrete" proof which establishes that there is no (strictly) $<$ -decreasing, infinite sequence of elements of S. When there is an accessibility proof of $S,$ $(S, <)$ is said to be accessible, or $S$ is said to be $<$ -accessible.At present there are no means to completely characterize the "concreteness" of accessibility proofs.An example of a "concrete" accessibility proof is seen in the theory of eliminators for $\epsilon_{0}$ (cf.[1]).In the accessibility proof of ordinal diagrams which is to be presented in this article, the notion of strong accessibility plays an essential role.This is not an elementary concept and the inductive definition involving higher order quantifiers is introduced in the course of the proof.Therefore our proof does not deserve a claim of concreteness in strict sense.It is nevertheless an improve- ment from the set-theoretical proof, which employs the transfinite induction (as a general principle), as in our proof the difficulty concentrates in one part, and it is a preparation for the more constructive proof in a subsequent paper.For our present approach to the accessibility of ordinal diagrams, it is necessary to generalize the theory of ordinal diagrams, namely we shall consider systems of ordinal diagrams with three basic well-ordered sets rather than two of them.An account of such systems will be given in the first part of this article.It is also there that a sequence of systems of ordinal diagrams is studied.This materializes the notion of strong accessibility, thereby supplying us with a means to carry out the accessibility proof (the second part).Our major task is to show that every ordinal diagram is strongly accessible, and the crucial part of the proof depends heavily on the construction of fundamental sequences.In the course of our proof, we often use the terms "accessible" and "wellordered" for a set with a linear ordering.The full meaning of the former is that the set has a primitive recursive linear ordering for which fundamental *