Talk: Stegert's Psi functions

Superficial complexity

Stegert's OCF uses 6 pages to define the notion of reflection instances, and Rathjen's OCF from "An Ordinal Analysis of Stability" uses around 8 pages. What causes OCFs of this strength that are used for proof theory to have such enormous technical complexity, while ordinal notations like Taranovsky's C conjectured to encapsulate even stronger theories (such as Z₂) are far simpler? It seems to be in Stegert's and Rathjen's best interest to keep the definition as simple as possible, so theorems are easier to prove, in which case this is as simple as OCFs can get on this level? (While being used for analysis with proofs) C7X (talk) 02:12, 8 June 2021 (UTC)

Edit: From reading a bit more of Stegert's paper, from what I guess much of the ordinal notation system comes from recursive implementation of corollary 2.3.12 (for a standardness predicate on terms) not sure about that, and theorem 2.3.14 (for a binary relation on terms). And it's the OCF whose definition is extremely complicated, not so much the ordinal notation. But even then, this notation seems quite a bit more complex than Taranovsky's C C7X (talk) 02:18, 8 June 2021 (UTC)

Taranovsky does not actually collapse ordinals, and hence the well-foundedness might not hold. What we need is an ordinal notation, which is required to be well-founded. Say, (a reasonable formalisation of) BM1 is much simpler than ordinal notations, but is not well-founded.

​On the other hand, ordinals are well-founded by definition. Therefore if a notation precisely imitate the ordering of ordinals, then it is automatically well-founded. The point is that imitating actual ordinals in a precise manner is very difficult, and the definition will be long. For example, you can see that Denis's ordinal notation based on M is sufficiently long, and Rathjen's ordinal notation based on M is longer. Even a simpler ordinal notation e.g. Jager-Buchholz's ordinal notation is sufficiently complicated.

p-adic 02:26, 8 June 2021 (UTC)

Repetitive citations and ill-definedness

Two things:

1. How do I cite the same paper less repetitively if the citations are for different page numbers?
2. In definition 7.2.1 of Stegert's paper, it seems that a map \(\textrm N\) is given without a domain, but its domain is clarified later in lemma 7.2.2. Is clarifying the domain of a function after it's defined in the paper bad writing practice? Or does it mean \(\textrm N\) is completely ill-defined, since the lemma would have to be proven about \(\textrm N\), a function that doesn't yet exist? C7X (talk) 04:57, 10 June 2021 (UTC)

1. I usually cite a source in this way^{[1] p.40} unlike you. This allows us to easily know the coincidence of the reference.

2. Since α is quantified so that it runs through T(Ξ), "N(α) = min ..." is a definable function formula. Given a definable funtion formula F(x,y) with domain X (= {x|∃y,F(x,y)}), we can regard it as a function, which is commonly denoted by a symbol f introduced by a sentence like "f(x) = ... " in the definition of F(x,y). (In the case of the function formula N(α) = min ..., it is N.) In that case, we say "f is defined on X".

I note that introducing a definable partial function is a common method in mathematics. For example, Rathjen's χ is defined by a function formula, and the domain is determined after the introduction of the function formula.

​The lack of the domain is a critical problem when googologists write "f(α) = ..." without quantifying α by writing "for any ordinal α", "for any set α", "for any integer α larger than -10", or something like that. If we can uniquely guess the domain, then it does not cause a problem even though it is ill-defined to some extent and should be fixed. On the other hand, definitions written by googologists usually have serious ambiguity, due to multiple errors unlike defintiions in mathematical papers. In that case, they can be completely ill-defined. (I wrote a little about a function formula in the second last paragraph of "General Setting" section in my guideline, but it might be better to add a similar explanation to my common lists.)

p-adic 05:54, 10 June 2021 (UTC)