#ordinal analysis

[ciandoesstuff]

would the set of all infinite ordinals less than why did it delete the epsilon εbut anyway it's epsilon-0 be considered the omegavers- NO NO NEVERMIND POST CANCELLED POST CANCELLED NEVER FUCKING MIND

[voiceless-lateral-fricative]

a conlang with an ordinal base number system, like base ω

technically this would be distinct from having no base at all, and instead you can represent higher and higher ordinals using only a couple symbols

e.g:

ω²+ω•25+41 =[1][25][41], each digit is represented using square brackets

[lilith-hazel-mathematics]

You two seem to know a lot about logic. I am currently very lost attempting to study proof theoretic ordinals on my own. Do you know any good sources to study them from or have any advice?

While I have several vague senses of what things do and how they work and their proofs and what they are in some cases, it has swaths of handwavy bits and attempts to formalise it continually elude and confound me.

Despite being very knowledgeable about both ordinals and proof theory, I unfortunately have basically no clue how proof theoretic ordinals work. As general advice, it could be useful to just retrace the steps of the mathematicians who pioneered the subject, since that might give some motivation to why they defined things the way they have. With the benefit of hindsight of course, about what works and what doesn't.

At the risk of 2501-ing myself (or vice versa, depending on how much you already know), I only know the absolute basics about ordinal analysis, like that the proof theoretic ordinal of Peano Arithmetic is ε0. This was proved by Gentzen back in 1936, by proving PA is consistent using a transfinite induction of length ε0. In combination with Godel's Incompleteness Theorem, it follows that PA cannot perform transfinite induction of length ε0. My understanding is that this was the origin of ordinal analysis, so reading Gentzen's proof may be enlightening if you haven't already. I personally haven't read it, so I have no clue how it works, nor how difficult the proof is.

On the other hand, establishing a proof theoretic ordinal also involves showing that the theory can do transfinite induction of any strictly smaller length. That is, it's not enough to know that PA cannot do induction of length ε0, but you must also show that it can do inductions of length ω^ω and ω^ω^ω and so on. I've personally done this, and it's not horribly complicated. Basically for any ordinal α, the ordinal ω^α is isomorphic to the set of finite non-increasing sequences in α, using a form of lexicographical ordering. This isomorphism is definable in terms of the Cantor Normal Form. Reasoning in this way, you can show that if PA can do transfinite induction to length α, then it can also do induction to length ω^α. Of course induction to length ω is free, as that's literally just induction along ℕ.

Through the grapevine I've also heard that the Feferman-schütte ordinal is of great relevance to predicative arithmetic, but that's just me gossiping. I don't really know anything about it.