Ordinal collapsing function: Difference between revisions

 
(11 intermediate revisions by one other user not shown)
Line 4:
 
== History ==
The first ordinal collapsing function in the literature was Bachmann's \( \psivarphi \) function, which was regarded as novel at the time and was used to calibrate the size of the [[Bachmann-Howard ordinal]]. However, the definition is quite cumbersome. ABachmann's modernmethod "recast",was proposedextended byto Michaeluse Rathjen<ref>Rathjenhigher cardinals, Michaele.g. "Theto Art of Ordinal Analysis"</ref>, is thatuse \( \psi_\Omega(\alpha)Omega_n\) isfor theall least countablefinite \( \rho n\) soby thatPfeiffer thein countable1964 ordinalsand constructibleto fromuse \(\OmegaOmega_\alpha\) and the set of ordinals belowfor \( \max(1, alpha<I\rho) \)by usingIsles thein following1970,<ref>Buchholz, operationsFeferman, arePohlers, all less than \(\rho\): additionSieg, the''Iterated mapInductive \(Definitions \xiand \mapstoSubsystems \omega^\xiof \),Analysis: andRecent \(Proof-Theoretical \psi_\OmegaStudies''. \)Lecture restrictedNotes toin inputsMathematics less than \( \alpha \1981). OfSpringer course, this definition isBerlin condensedHeidelberg, andISBN is9783540386490.</ref> usuallybut writtenwith insimilarly termscumbersome of \( C \)-setsdefinitions.<ref Belowname="RathjenArt" is the more formal definition/><sup>p.11</sup>
 
A modern "recast", proposed by Michael Rathjen<ref name="RathjenArt">Rathjen, Michael. "[https://www1.maths.leeds.ac.uk/~rathjen/ICMend.pdf The Art of Ordinal Analysis]".</ref>, is that \( \psi_\Omega(\alpha)\) is the least countable \( \rho \) so that the countable ordinals constructible from \(\Omega\) and the set of ordinals below \( \max(1, \rho) \) using the following operations are all less than \(\rho\): addition, the map \( \xi \mapsto \omega^\xi \), and \( \psi_\Omega \) restricted to inputs less than \( \alpha \). Of course, this definition is condensed, and is usually written in terms of \( C \)-sets. Below is the more formal definition.
 
* Let \( \Omega = \aleph_1 \) and \( C_0^\Omega(\alpha, \beta) = \beta \cup \{0, \Omega\} \).
Line 15 ⟶ 17:
== Remarks ==
Rathjen has remarked upon a small detail of various ordinal collapsing functions, which he calls pictorial collapse. In particular, he says that, in the OCF defined in the "History" section, \( \psi_\Omega(\alpha) \) can be viewed as the "\( \alpha \)th collapse of \( \Omega \)" since, as he puts it, the order-type of \( \Omega \) as viewed within \( C^\Omega(\alpha, \psi_\Omega(\alpha)) \) is actually \( \psi_\Omega(\alpha) \).<ref>M. Rathjen, Proof Theory (Stanford encyclopedia of Philosophy), special case of definition 5.11</ref> The same property applies to [[Buchholz's psi-functions]]<ref>W. Buchholz, ''A New System of Proof-Theoretic Ordinal Functions'', Annals of Pure and Applied Logic, vol. 32, pp.195-207, (1986)</ref>, Rathjen's OCF collapsing a [[Mahlo cardinal|weakly Mahlo cardinal]]<ref>Rathjen, Michael. "Ordinal Notations Based on a Weakly Mahlo Cardinal", Archive for Mathematical Logic 29 (1990) 249--263.</ref>, and Rathjen's OCF collapsing a [[weakly compact cardinal]].<ref>Rathjen, Michael. "Proof Theory of Reflection", Annals of Pure and Applied Logic 68, 181--224 (1994).</ref>
 
== Use of nonrecursive countable ordinals ==
It may seem circular to use an OCF whose definition presumes existence of uncountable or large cardinals in the ordinal analysis of a theory much weaker than ZFC. However all instances of uncountable cardinals in the definition of the OCF may be replaced with nonrecursive countable ordinals, at the expense of much difficulty in proving the relevant theorems about the OCF. For example, Rathjen has defined an OCF for analyzing KPM that uses [[Admissible ordinal|admissible ordinals]] in place of regular cardinals, and recursively Mahlo ordinals in place of Mahlo cardinals.<ref>Realm of Ordinal Analysis, near the end</ref>
 
The main technique for proving the relevant theorems about \( \psi_\pi(\alpha) \) (e.g. that \( \psi_\pi(\alpha)<\pi \)) becomes to use a \( \pi \)-recursive coding scheme to code the representable ordinals that are \( >\pi \) into members of \( L_\pi \). This coding must respect the ordering of the \( \psi_\kappa(\beta) \), which itself has not yet been verified.<ref name="Rathjen94">Possible citation? [https://www1.maths.leeds.ac.uk/~rathjen/WELL.pdf]</ref><sup>Maybe not? Look at things around p.11 more</sup><!--This citation is for previous sentence also--> This is in contrast to the cardinal-based definition of \( \psi \), in which case these can be proven by simple arguments like cardinality arguments.<ref>M. Rathjen, "How to develop proof-theoretic ordinal functions on the basis of admissible ordinals" (1998), MSC-1991 classification 03F13/03F35. Accessed 1 September 2023. Possibly in Mathematical Quarterly vol. 39 (1993)?</ref> In addition, some of the relations recursive definitions are performed along are well-founded but non-set-like.<ref name="Rathjen94" /><sup>p.5</sup>
 
== Quantifier complexity ==