We changed our privacy policy. Read more.

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
3
votes
0answers
70 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 ...
0
votes
0answers
85 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 ...
1
vote
1answer
78 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 ...
6
votes
1answer
119 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).
0
votes
0answers
55 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 ...
0
votes
0answers
38 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 ...
3
votes
0answers
87 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 ...
1
vote
0answers
63 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 ...
2
votes
1answer
94 views

Proof-theoric ordinal of ETCS

What is the proof-theoric ordinal of Lawvere's elementary theory of the category of sets?
2
votes
0answers
53 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 ...
2
votes
0answers
37 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_{\...
-2
votes
1answer
128 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 ...
0
votes
1answer
100 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 ...
4
votes
0answers
68 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 ...
3
votes
1answer
104 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$. ...
8
votes
1answer
236 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 ...
6
votes
2answers
249 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 ...
1
vote
1answer
298 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 ...
0
votes
0answers
80 views

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

Let be $PA_0 =PA$, Let be ,for every ordinal $\alpha$ , $PA_{\alpha+1} =PA_\alpha + Con(PA_\alpha )$ and if $\alpha$ is limit ordinal let be $PA_\alpha = \cup_{\beta<\alpha} PA_\beta$. 1) Is ...
13
votes
1answer
344 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 ...
1
vote
1answer
130 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 ...
7
votes
2answers
396 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?