Ordinal collapsing function: Difference between revisions

Content deleted Content added
Tungster24 (talk | contribs)
Removed ψ_Ω(Ω) from the list of example values at Arai's ψ as it was wrongfully stated to be ε_0. The Skolum hull used in the definition of Arai's ψ is closed under the binary Veblen function, ψ_Ω(Ω) would thus be equal to φ(1,1,0) = β_0.
Line 223:
Suppose <math>\mathsf{KP\Pi_N} \vdash \theta</math> for a <math>\mathsf{\Sigma_1}</math> (<math>\Omega</math>)-sentence <math>\mathsf{\theta}</math>. Then, [[Existential quantification|there exists]] a finite <math>n</math> such that for <math>\alpha = \psi_\Omega(\omega_n(\mathbb{K}_N + 1))</math>, <math>L_\alpha \models \theta</math>. It can also be proven that <math>\mathsf{KP\Pi_N}</math> proves that each initial segment <math>\{\alpha \in OT: \alpha < \psi_\Omega(\omega_n(\mathbb{K}_N + 1))\}; n = 1, 2, \ldots</math> is [[Well-founded relation|well-founded]], and therefore, <math>\psi_\Omega(\varepsilon_{\mathbb{K}_N+1})</math> is the [[Ordinal analysis|proof-theoretic ordinal]] of <math>\mathsf{KP\Pi_N}</math>. One can then make the following conversions:
 
* <math>\psi_{\Omega}(\Omega) = |\mathsf{PA}| = \varphi(1, 0)</math>, where <math>\Omega</math> is either the least recursively regular ordinal or the least uncountable cardinal, <math>\mathsf{PA}</math> is [[Peano axioms|Peano arithmetic]] and <math>\varphi</math> is the [[Veblen function|Veblen hierarchy]].
* <math>\psi_{\Omega}(\varepsilon_{\Omega + 1}) = |\mathsf{KP\omega}| = \mathsf{BHO}</math>, where <math>\Omega</math> is either the least recursively regular ordinal or the least uncountable cardinal, <math>\mathsf{KP\omega}</math> is [[Kripke–Platek set theory]] with infinity and <math>\mathsf{BHO}</math> is the [[Bachmann–Howard ordinal]].
* <math>\psi_{\Omega}(\Omega_{\omega}) = |\mathsf{\Pi^1_1-CA_0}| = \mathsf{BO}</math>, where <math>\Omega_{\omega}</math> is either the least limit of admissible ordinals or the least limit of infinite cardinals and <math>\mathsf{BO}</math> is [[Buchholz's ordinal]].