All Questions
Tagged with ordinal-analysis theories-of-arithmetic
12 questions
39
votes
3
answers
3k
views
Why do stacked quantifiers in PA correspond to ordinals up to $\epsilon_0$?
I am trying to understand why induction up to exactly $\epsilon_0$ is necessary to prove the cut-elimination theorem for first-order Peano Arithmetic; or, as I understand, equivalently, why the length ...
13
votes
3
answers
1k
views
Which ordinals can be proof-theoretic ordinals of a reasonable theory?
When talking to a friend recently he asked a question - are there any reasonable first-order theories which have proof theoretic ordinal equal to small or large Veblen ordinal? I have then extended ...
- 28.2k
13
votes
1
answer
437
views
What is the proof-theoretic ordinal of bare $\mathsf{NFU}$?
On the Stanford Encyclopedia of Philosophy article on alternative axiomatic set theories, it is stated without reference that bare $\mathsf{NFU}$ (i.e., $\mathsf{NFU}$ without the axiom of infinity) ...
- 12.4k
11
votes
2
answers
1k
views
Why is there a need for ordinal analysis?
Consider the Peano axioms. There exists a model for them (namely, the natural numbers with a ordering relation $<$, binary function $+$, and constant term $0$). Therefore, by the model existence ...
- 139
9
votes
1
answer
643
views
Gentzen's result on PA
The Wikipedia states that Gentzen proved that "in modern terms, the proof-theoretic ordinal of PA is $\varepsilon_0$." Further down, the article defines what the "proof theoretic ordinal" of a theory ...
- 1,174
9
votes
1
answer
1k
views
ERA, PRA, PA, transfinite induction and equivalences
I'm quite sure I don't understand very well the links between proof theoretical ordinals of theories, the axioms of transfinite induction and the objects a theory can prove to exist.
For instance I'm ...
8
votes
2
answers
560
views
Models of PRA/EFA with induction on $X$ but not $\omega^X$
As I currently understand it, induction on formulas containing $N+1$ first-order quantifiers is required to prove the well-ordering of the ordinal $(\omega \uparrow\uparrow N) < \epsilon_0$, that ...
8
votes
1
answer
574
views
Iterated Gentzen: or, a Sith objection to the proof of consistency of PA
$\DeclareMathOperator\PRA{PRA}\DeclareMathOperator\WF{WF}\DeclareMathOperator\Con{Con}\DeclareMathOperator\PA{PA}$Preamble: In the year … in a galaxy far far away, a nasty Sith named Darth Dubious (...
- 7,853
6
votes
0
answers
421
views
What is proof-theoretic ordinal of weak first-order arithmetic?
According to Wikipedia(https://en.wikipedia.org/wiki/Ordinal_analysis) and nlab(https://ncatlab.org/nlab/show/ordinal+analysis), a proof-theoretic ordinal of $\mathsf{PRA}$ is $\omega^\omega$.
...
- 178
4
votes
1
answer
269
views
Does Peano's axioms prove $\alpha$-induction for primitive recursive sequences for every concrete $\alpha < \varepsilon_0$?
It is well-known that Peano's axioms (PA) cannot prove $\varepsilon_0$-induction for primitive recursive sequences (PRWO($\varepsilon_0$)), because PA + PRWO($\varepsilon_0$) proves the consistency of ...
1
vote
1
answer
466
views
What does "can almost be proven in PA" mean regarding Theorem 2 of Timothy Chow's expository article, "The Consistency of Arithmetic"?
In his expository article, "The Consistency of Arithmetic" (MSN), Prof. Chow has the following theorems:
Theorem 1. If $a_1, a_2, a_3,\dotsc$ is a sequence of ordinals and $a_i \ge a_j$ whenever $...
- 6,132
0
votes
3
answers
1k
views
Regarding Gentzen's note regarding 'Godel-points' (i.e., "Where is the Godel-point hiding?")
Consider the following note written by Gerhard Gentzen in early 1932, on the onset of his work on a consistency proof for arithmetic:
The axioms of arithmetic are obviously correct, and the ...
- 6,132