Ordinal diagram

Ordinal diagrams are a system of ordinal notations created by Gaisi Takeuti, and used to carry out a consistency proof of \(\Pi^1_1\)-comprehensionG. Takeuti, Consistency Proofs of Subsystems of Classical Analysis, Annals of Mathematics, vol. 86 (1967), pp. 299--348.. They have been shown to be wellfounded by Takeuti and YasugiG. Takeuti, M. Yasugi, An accessibility proof of ordinal diagrams, Journal of The Mathematical Society of Japan (1981)..
== Definition ==
Takeuti defined a general method of creating a system of ordinal diagrams from any two well-ordered sets \(I\) and \(A\). Let \(0\) be the smallest element of \(I\). The set of ordinal diagrams is defined inductively as follows:
# \(0\) is an ordinal diagram. It is also said to be connected.
# If \(i\in I\) and \(a\in A\), and \(\alpha\) is an ordinal diagram, \((i,a,\alpha)\) is an ordinal diagram. It is also said to be connected.
# Suppose \(n>1\) and \(\alpha_1,\ldots,\alpha_n\) are connected ordinal diagrams. Then \(\alpha_1+\cdots+\alpha_n\) is a nonconnected ordinal diagram.
Some ordinal diagrams are equivalent. We define certain ordinal diagrams to be equivalent:
# \(0=0\).
# If \(\alpha=\beta\), then \((i,a,\alpha)=(i,a,\beta)\).
# If \(\alpha_1,\ldots,\alpha_n\) is a permutation of \(\beta_1,\ldots,\beta_n\), then \(\alpha+1+\cdots+\alpha_n=\beta_1+\cdots+\beta_n\).
Suppose \(\beta\) occurs in \(\gamma\). Then \(i,a\) are connected to \(b\) in \((i,a,\gamma)\). Suppose every element \(i\) of \(I\) occurring in \(\alpha\) that is connected to \(\beta\) is at least \(j\), then \(\beta\) is \(j\)-active in \(\alpha\). Let \((i,a,\gamma)\) be \(j\)-active in \(\alpha\), then \(\gamma\) is a \(j\)-section of \(\alpha\).
Adjoin an element \(\infty\) to \(I\) to form \(\tilde I\). For \(\tilde\imath\in\tilde I\), define comparison \(<_{\tilde\imath}\) as follows:
# \(0<_{\tilde\imath}\beta\) if \(\beta\) is not \(0\).
# If \(\alpha=\alpha_1+\cdots+\alpha_n\) and \(\beta=\beta_1+\cdots+\beta_m\) with \(n+m>2\) then \(\alpha<_{\tilde\imath}\beta\) prodided one of the following:
## There is a \(q\) such that for all \(p\) \(\alpha_p<_{\tilde\imath}\beta_q\).
## \(n=1\) and \(\alpha=\beta_q\) for some \(q\).
## \(m,n>1\) and there are \(p,q\) such that \(a_p=b_q\) and \(\alpha_1+\cdots+\alpha_{p-1}+\alpha_{p+1}+\cdots+\alpha_n<_{\tilde\imath}\beta_1+\cdots+\beta_{q-1}+\beta_{q+1}+\cdots+\beta_m\).
# Suppose \(\tilde\imath\neq\infty\) and \(\alpha,\beta\) are connected. Let \(\tilde\jmath\) be the least \(j\) such that there is a \(j\)-section of \(\alpha\) or \(\beta\), or \(\infty\) if no such \(j\) exists. Then \(\alpha<_{\tilde\imath}\beta\) provided one of the following:
## There is an \(\tilde\imath\)-section \(\gamma\) of \(\beta\) such that \(\alpha<_{\tilde\imath}\gamma\) or \(\alpha=\gamma\).
## \(\alpha<_{\tilde\jmath}\beta\) and for every \(\tilde\imath\)-section \(\gamma\) of \(\alpha\), \(\gamma<\beta\).
# If \(\tilde\imath=\infty\) and \(\alpha=(i,a,\gamma)\) and \(\beta=(j,b,\delta)\), then \(\alpha<_\infty\beta\) provided one of the following:
## \(i<j\).
## \(i=j\) and \(aG. Takeuti, Proof Theory (1975), Chapter 5, Section 27. that the order type of the system with \(I=\omega+1\) and \(A=1\) is the proof-theoretic ordinal of \(\Pi^1_1\text-CA\). Fundamental sequences have been defined by Takeuti and YasugiG. Takeuti, M. Yasugi, Fundamental sequences of ordinal diagrams (1976)..
Category:Ordinal notations