Skip to main content

Questions tagged [ordinal-analysis]

In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

Filter by
Sorted by
Tagged with
1 vote
0 answers
81 views

Are finitist systems the ones with a proof-theoretic ordinal of at most $\omega^\omega$?

The proof-theoretic ordinal of $\mathsf{EFA}$ and $\mathsf{RCA}_0^*$ are $\omega^3$ and the one of $\mathsf{PRA}$, $\mathsf{I\Sigma1}$, $\mathsf{RCA}_0$, etc. is $\omega^\omega$. See https://ncatlab....
user avatar
1 vote
0 answers
61 views

How large is $f_{\Gamma_{0}}(2)$ in the Fast-Growing Hierarchy?

If my ordinal arithmetic is correct, $f_{\Gamma_{0}}(2)=f_{\epsilon_{\epsilon_0}}(2)$ so $$f_{\epsilon_{\omega}}(2)\ll f_{\Gamma_{0}}(2)\ll f_{\epsilon_{\epsilon_1}}(2),$$ but that doesn't show ...
Michael Toth's user avatar
3 votes
1 answer
124 views

Why do we define the proof-theoretic ordinal of a theory the way we do when there are unnatural well-orderings out there?

The proof-theoretic ordinal of first-order arithmetic ($\mathsf{PA}$) is $\varepsilon_{0}$. However, in pages 3 and 4 of Andreas Weiermann's Analytic combinatorics, proof-theoretic ordinals, and phase ...
John's user avatar
  • 4,362
3 votes
1 answer
72 views

Is there a model of KP with no $\emptyset'$ ordinal notation for the Bachmann-Howard ordinal?

The Bachmann-Howard ordinal (BHO) is a large recursive ordinal defined using ordinal collapsing functions. Kripke-Platek set theory (KP) is a fragment of ZF obtained by removing powerset, swapping ...
C7X's user avatar
  • 1,207
1 vote
0 answers
268 views

What is the least upper bound ordinal of my linear n-symbol partition ordinal (ordinal that contain all finite string of finite different symbol)?

Note: The "partition" here isn't relate to the partition at all. Note: For the detail of "ordinal that contain all finite string of finite different symbols", see the "Edit&...
Just a man in the world's user avatar
6 votes
2 answers
265 views

What, precisely, does it mean to represent an ordinal on a computer?

Two closely related questions about ordinals that I found quite confusing at first and couldn't find a satisfactory answer online (self-answering): I've heard sentences like "$\omega^{CK}$ is ...
Abhimanyu Pallavi Sudhir's user avatar
1 vote
1 answer
109 views

What is the proof theoretic ordinal of $\mathsf{B\Sigma}_{2}^{0}$?

The proof-theoretic strength of a theory is measured by the $\mathsf{\Pi}_{1}^{1}$-ordinal of the theory and it is called the proof-theoretic ordinal (PTO) of the theory (there are other ordinal ...
John's user avatar
  • 4,362
5 votes
1 answer
200 views

What are the proof-theoretic strengths of Ramsey's theorems?

The proof-theoretic strength of a theory is measured by the $\mathsf{\Pi}_{1}^{1}$-ordinal of the theory (indeed, there are other ordinal analyses, like the $\Pi_{2}^{0}$-ordinal of the theory). ...
John's user avatar
  • 4,362
5 votes
0 answers
85 views

When should one use transfinite induction?

I've come across it multiple times now in proof theory papers that authors use (sometimes quite elaborate) inductions in order to prove easy results. The most striking example is the following, where ...
10012511's user avatar
  • 682
2 votes
1 answer
276 views

What is an example of a statement equivalent to $\omega^{\omega}$-induction?

If $\alpha$ is a countable ordinal and $A$ is the set of natural numbers having well-ordering of type $\alpha$, does this mean that $\alpha$-induction (transfinite induction up to $\alpha$) is ...
John's user avatar
  • 4,362
3 votes
1 answer
222 views

What is the proof-theoretic ordinal of true arithmetic?

The proof theoretic ordinal of $PA$ is $\epsilon_0$. My question is, what is the proof-theoretic ordinal of true arithmetic, i.e. $Th(\mathbb{N})$? I’m assuming you get something bigger than $\...
Keshav Srinivasan's user avatar
1 vote
0 answers
43 views

Does "predicativitness" of class comprehension in $\sf MK$ affects the value of the class of all ordinals?

If we take $\sf MK$ and $\sf PMK$, the latter is just a weakening of the former by restricting the formulas in class comprehension to be relativised to sets which is by the way a mono-sorted version ...
Zuhair's user avatar
  • 4,555
2 votes
1 answer
155 views

Link between a theory’s proof-theoretic ordinal and the fastest-growing function it can prove total

When I’ve tried to read up on proof-theory I’ve come across this point multiple times - that given a well-founded fast-growing hierarchy, the index of the fastest-growing function f that T can prove ...
Ablation_nation's user avatar
3 votes
0 answers
182 views

Iterated $\Pi^1_1$-reflection and non-Gandiness underrepresented in ordinal analyses?

Edit: I now feel this question is more appropriate for MathOverflow, I will leave this copy for posterity. Note on terminology: "admissible", "$(^+)$-stable", and "$\Pi^1_1$-...
C7X's user avatar
  • 1,207
2 votes
1 answer
147 views

What is the relevance of the fast-growing hierarchy in the definition of Yudkowsky’s number?

I’m struggling with a certain connection the author draws in defining a certain “huge” number. The number is defined as follows: Let T be the first-order theory of Zermelo-Fraenkel set theory plus the ...
Ablation_nation's user avatar
4 votes
1 answer
202 views

Why do we need ordinal representation systems?

Trying to learn about ordinal analysis and I keep seeing the concept of the natural ordinal representation system, for representing ordinals as relations on N. In particular the definition of an ...
Ablation_nation's user avatar
0 votes
0 answers
221 views

Higher order arithmetic, hierarchies and proof theoretic ordinals

I would like to consider a generalization of the notation $\Pi$ and $\Sigma$ used for the arithmetical hierarchy $(\Pi^0_n$, $\Sigma^0_n)$ and the analytical hierarchy $(\Pi^1_n$, $\Sigma^1_n)$ to ...
holmes's user avatar
  • 413
1 vote
1 answer
236 views

Is there a sequence of extensions of ZFC where the corresponding sequence of proof theoretic ordinals has $\omega_1^{CK}$ as least upper-bound

I was reading this question on MO where they define an infinite sequence of extensions of ZF by creating iteratively a new theory which includes the consistency of the previous ones. The definition ...
holmes's user avatar
  • 413
6 votes
1 answer
150 views

Is Goodstein's theorem equivalent to $\varepsilon_0$-induction over weak base theories (e.g. PRA)?

Is Goodstein's theorem equivalent to $\varepsilon_0$-induction over a weak base theory like PRA? I'm surprised this hasn't been asked here before (as far as I can tell).
Jori's user avatar
  • 1,698
0 votes
0 answers
125 views

Turing degrees of subsets of Kleene $\mathcal{O}$ which are ordinal notations of subsets of the set of recursive ordinals

An ordinal $\alpha$ is said to be recursive if there is a recursive well-ordering of a subset of the natural numbers having the order type $\alpha$. The smallest ordinal that is not recursive is ...
holmes's user avatar
  • 413
4 votes
1 answer
507 views

What is the proof theoretic ordinal of Homotopy Type theory?

The proof theoretic ordinal of Martin-Löf type theory is $\Gamma_0$. What about HoTT and what about other flavors of type theory (the ones related to the lambda cube for instance)?
holmes's user avatar
  • 413
0 votes
0 answers
60 views

Equation to Specify Lexicographical Ordering?

I am not a mathematician, but I need to specify, precisely, a special way to sort an arbitrary list of ASCII strings1, with the addition of some special rules for a small set of specific characters. I ...
Jim L.'s user avatar
  • 123
3 votes
0 answers
107 views

Optimal bound for cost of cut elimination in infinitary logic with transfinite cut-rank in terms of Veblen's $\varphi$ function

The theorem I am referring to is Tait's sharpening of Gentzen's Cut Elimination Theorem in [1], which Schütte [2, p. 204, Theorem 22.8] also calls the ``second cut elimination theorem'' (here written ...
10012511's user avatar
  • 682
1 vote
0 answers
91 views

Infinite ordinals in proof theory

I've been trying to get acquainted with proof theory (particularly ordinal analysis) as part of a school project, and am trying to tease out the story behind the appearance of infinite ordinals in a ...
Malice Vidrine's user avatar
2 votes
1 answer
121 views

Proof-theoric ordinal of ETCS

What is the proof-theoric ordinal of Lawvere's elementary theory of the category of sets?
1103_base_6's user avatar
2 votes
0 answers
95 views

At which ordinal this "counting" ordinal language would fail?

The language $FOL(=, \in , <, C)$ is mono-sorted first order predicate language with extra-logical primitives of equality (and its axioms), set membership, strict smaller than binary relation, and ...
Zuhair's user avatar
  • 4,555
2 votes
0 answers
52 views

What is the proof-theoretic ordinal of $ \mathsf{PA}+\mathsf{TI}(\prec_{\varepsilon_0})$?

$ \mathsf{TI}(\prec_{\varepsilon_0}) $ is transfinite induction on $\varepsilon_0$ ordinal notation by Cantor normal form. I think that proof-theoretic ordinal of $\mathsf{PA}+\mathsf{TI}(\prec_{\...
Alwe's user avatar
  • 21
-2 votes
1 answer
159 views

Question on An Explicit Enumeration of Ordinals

Question: What is the first countable ordinal that doesn't appear in the sequence $T$ defined below and is that ordinal equal to $\{ t_i : t_i \in T\}$? Introduction: Making a Sequence $T$ based on ...
AplanisTophet's user avatar
0 votes
1 answer
166 views

What is the lowest layer of the Constructible Universe which is a model of $ZFC-P$?

This answer says that the smallest ordinal $\lambda$ such that $L_\lambda$ is a model of $ZFC$ isn’t easy to describe, other than to say that $\omega_1^{CK}<\lambda<\omega_1$. But my question ...
Keshav Srinivasan's user avatar
5 votes
0 answers
111 views

Does there exist a notion of "growth rate", big-O notation, etc for ordinal (normal) functions?

Given some $f: \Bbb N \to \Bbb N$, we have various ways to talk about how fast it's growing: big-O notation, little-o notation, and so on. These are a good way to compare growth rates, so we can talk ...
Mike Battaglia's user avatar
4 votes
1 answer
163 views

Modifying the "base" of Veblen's hierarchy to exceed $\Gamma_0$

The Veblen hierarchy is usually defined with $\varphi_0(x) = \omega^x$. As a result, we can define the Feferman–Schütte ordinal as the first fixed point of the function $\varphi_\alpha(0) = \alpha$. ...
Mike Battaglia's user avatar
8 votes
1 answer
460 views

How do we know PA is incomparable with PRA + $\epsilon_0$?

Gödel 2 says that no subtheory of PA can prove Con$_{PA}$, and even though most natural theories $T$ extending PA can prove Con$_{PA}$, this is relatively uninteresting since anyone doubting the ...
Morgan Sinclaire's user avatar
6 votes
2 answers
397 views

Is there a "solution" to the ordinal game?

Even though I have almost no background in logic, I find the idea of ordinal notation quite interesting. It seems that the idea is to come up with notation to define larger and larger numbers, until ...
zoidberg's user avatar
  • 1,305
1 vote
1 answer
488 views

Conway Notation for Large Countable Ordinals

I have not previously seen anything online that dives deeply into On: In Conway's notation On denotes the ordinal numbers (and No denotes the set of all surreal Numbers). Basically the elements of ...
user820789's user avatar
0 votes
0 answers
111 views

How is the minimum ordinal to reach TRUE ARITHMETIC starting from PA?

Let $PA_0$ be $PA$, for every ordinal $\alpha$, let $PA_{\alpha+1} $ be $PA_\alpha + Con(PA_\alpha )$ and if $\alpha$ is limit ordinal let $PA_\alpha$ be $\cup_{\beta<\alpha} PA_\beta$. Is every $...
Stefano.A's user avatar
14 votes
1 answer
563 views

Small proof-theoretic ordinals

Where to find proofs of the following: 1) proof-theoretic ordinal of $I\Sigma_0$, which is Robinson's Q arithmetic with induction on $\Sigma_0$ formulas, is $\omega^2$? 2) proof-theoretic ordinal of ...
George Levsky's user avatar
1 vote
1 answer
198 views

Has the proof theoretic ordinal of $MLTT + M$ been studied?

By $MLTT + M$ I mean basic Martin Lof type theory with general $M$-types. It well known that the proof-theoretic ordinal of $MLW$ (MLTT with W-types) is the Bachmann-Howard ordinal, but is the proof ...
Nathan BeDell's user avatar
7 votes
2 answers
510 views

proof theoretic ordinal for Robinson's arithmetic

Does a theory like Robinson's arithmetic have a proof-theoretic ordinal? If so, what is it?
Cecilia Burrow's user avatar