Questions tagged [ordinal-analysis]
The ordinal-analysis tag has no usage guidance.
55
questions
5
votes
0
answers
79
views
Iterated $\Pi^1_1$-reflection and non-Gandiness underrepresented in ordinal analyses?
This is a copy of Math StackExchange question #4395977, which I felt was more appropriate for MathOverflow.
The admissible ordinals $\alpha$ s.t. the supremum of $\alpha$-recursive well-orderings is ...
- 804
2
votes
0
answers
101
views
How closely do ordinal collapsing functions relate to Skolem hulls?
Ordinal collapsing functions appear in proof theory, and they are used to name large countable ordinals by using uncountable ordinals. Previously I posted a question about why $\psi(\alpha)$ is ...
- 804
1
vote
0
answers
92
views
Is there an error in W. Buchholz's paper "A simplified version of local predicativity"?
I want to self-learn proof theory. It seems that the operator controlled derivation method is important in this field, and the paper in the title is the first paper that uses this method.
So I'm ...
- 1,276
5
votes
1
answer
341
views
A possible flaw in Theorem 14.17 in Kurt Schütte's -Proof Theory-
Reading Chapter V, pages (73-97) in Proof Theory (Springer, 1977), by Kurt Schütte, I have encountered a peculiar problem which puzzles me.
On page 96, a map $\rm{Nr}:\overline{\rm{OT}}\rightarrow \...
- 2,036
7
votes
1
answer
187
views
Does $\text{ACA}_0$ + True Arithmetic prove the well-foundedness of every recursive ordinal?
As discussed in Noah Schweber's answer to What is the proof-theoretic ordinal of true arithmetic?, it is somewhat ambiguous what “the proof-theoretic ordinal of True Arithmetic” might mean. In one ...
- 4,471
5
votes
1
answer
210
views
How to build large recursive ordinals using Dillator and/or Ptykes?
I've only recently learned about Girard's theory of Dilators and Ptykes, and I find this theory very elegant, but it is not clear at all to me whether/how it can be used to produce ordinal notations ...
- 38.7k
1
vote
0
answers
104
views
Is $\sf \Gamma_0$ the proof theoretic ordinal of this kind of predicative class theory?
Adopting the approach of Mono-sorted $\sf NBG$, define sets as elements of classes, then axiomatize:
Extensionality, Predicative Class comprehension, emptyset, in the usual manner along mono-sorted $\...
- 7,901
1
vote
0
answers
119
views
What is the proof theoretic ordinal of this kind of predicative type-set theory?
The following is a kind of Predicative Type Set Theory.
The question is about what is exactly the proof theoretic ordinal of this theory? Is it lower than the one expected for predicative theories, i....
- 7,901
5
votes
1
answer
195
views
How closely do ordinal collapsing functions relate to Mostowski collapse?
Ordinal collapsing functions (such as Rathjen's $\psi_\pi$-functions, not the Levy collapse function) name large countable ordinals by mapping larger ordinals below some "large" ordinal, ...
- 804
5
votes
0
answers
105
views
What's the purpose of $\mathsf M\text-\mathsf P$-expressions?
In ordinal notations such as Stegert's (Ordinal Proof Theory of Kripke–Platek Set Theory Augmented by Strong Reflection Principles) and Rathjen's (An Ordinal Analysis of parameter free $\Pi_2^1$-...
- 580
0
votes
0
answers
113
views
How to define BHO alternatives below admissible ordinals?
Bachmann-Howard ordinal is a recursive ordinal. It's not that large compared to those proof-theoretic ordinals of stronger theories, but the definition of BHO is sufficient to illustrate how ...
- 1,276
1
vote
1
answer
240
views
Does this restriction on powersets in ZF have a proof theoretic ordinal?
If we add to the language of set theory a total one place function symbol $\mathcal P$ standing for powerset operator, and then add to ZF-Power the following axioms:
Power: if $\phi$ is a formula in ...
- 7,901
6
votes
0
answers
172
views
Ordinal strength of iterated truth theories
Consider the theory ${\rm PA}^{\mathbb{T}}$ obtained by adding a truth predicate to Peano arithmetic, applicable to sentences of the unaugmented language and satisfying the compositionality axioms $\...
- 40.9k
12
votes
1
answer
346
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) ...
- 9,099
5
votes
0
answers
220
views
Higher order arithmetic, hierarchies and proof theoretic ordinals
I asked this question on MSE some days ago but I have not received any answer so I have decided to post it here.
I would like to consider a generalization of the notation $\Pi$ and $\Sigma$ used for ...
- 161
7
votes
1
answer
505
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,457
5
votes
0
answers
226
views
$Π_2$ strength of KP
I am looking for a characterization of the $Π_2$ statements provable in KP.
Here, KP (often denoted KPω) is the Kripke-Platek set theory, including infinity and full induction on ordinals. Here is ...
- 5,742
8
votes
1
answer
606
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,014
10
votes
1
answer
234
views
Is there a relation between type (maximum linearization) of a computable WQO and the ordinal strength of a theory needed to prove it?
Background:
Given a well partial order $X$ (more commonly studied with antisymmetry dropped as well-quasi-orders, but I'm going to say well partial order to make this definition simpler, obviously ...
- 2,495
6
votes
0
answers
335
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
0
votes
3
answers
953
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 ...
- 5,944
1
vote
1
answer
381
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 $...
- 5,944
11
votes
1
answer
460
views
What system suffices to show the strength of PRA is $\omega^\omega$?
Russell O'Connor wrote in 2009 (link):
PRA has consistency strength equivalent to the well-foundness of $\omega^\omega$, which can be stated again as the termination of some other program on all ...
- 32.9k
3
votes
0
answers
136
views
Partial well-ordering of formulas
Given a theory $T$, for arbitrary formulas $φ$ and $ψ$ that provably in $T$ denote an ordinal, set $[φ]_T < [ψ]_T$ iff provably in $T$, the ordinal denoted by $φ$ is less than the ordinal denoted ...
- 5,742
8
votes
0
answers
252
views
Natural examples of recursive pseudowellorderings
Question: What are some natural examples of recursive pseudowellorderings?
By natural, I mean in the style of reasonable ordinal notation systems as opposed to dependent on a Gödel numbering or an ...
- 5,742
4
votes
0
answers
309
views
Ordinal analysis and nonrecursive ordinals
Ordinal analysis is typically described as characterizing recursive ordinals in a theory $T$, but there is a sense in which it can characterize all $T$-ordinals, even those that are nonrecursive.
...
- 5,742
4
votes
1
answer
725
views
Going beyond the strength of Peano arithmetic "without sets"
First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set ...
- 3,388
8
votes
1
answer
257
views
Correspondence between proof-theoretic ordinals and fast growing functions?
For theories with well known proof-theoretic-ordinals, (what) is there a correspondence between their proof-theoretic-ordinal and (ordinal indexed families of?) fast growing functions provable total ...
- 225
2
votes
1
answer
506
views
What is the proof-theoretic ordinal of KPh?
If we work in this notation:
$$C_0 (\alpha, \beta) = \beta \cup \lbrace 0 \rbrace$$
$$C_{n+1} (\alpha, \beta) = \lbrace \gamma + \delta, \omega^\gamma, \Omega_{\gamma}, I_{\gamma}, \psi_\pi(\eta) | \...
- 482
5
votes
1
answer
371
views
A question about ordinal analysis
I have several questions related to ordinal analysis.
According to [1], here are the proof-theoretic ordinal of some well-known theories (using $|T|$ do denotate the proof-theoretic ordinal of $T$):
...
- 615
8
votes
4
answers
1k
views
Formalizations of The Matchstick Diagram Representation of Ordinals
The matchstick diagram is a really interesting and intuitive method of representing countable ordinals. However, because of how difficult it is to graphically represent ordinals with it, I started ...
- 1,224
9
votes
1
answer
286
views
$Π^0_1$ Proof Ordinals
Natural theories extending EFA (exponential/elementary function arithmetic) are well-ordered by $Π^0_1$ provability, and we would like a formal definition of the well-ordering that is robust yet as ...
- 5,742
10
votes
1
answer
349
views
Complexity of induction formulas in proof theoretic ordinals
According to The Art of Ordinal Analysis, the proof theoretic ordinal of a theory $T$ is the least ordinal $\alpha$ such that:
$${\bf ERA}+TI(\alpha,ECP)\vdash Con(T)$$
In above definition, $ECP$ ...
- 1,699
6
votes
1
answer
407
views
Existence of well-ordering of epsilon_0 in weak theories
In a discussion on a youtube video on the hydra game I jokingly mentioned how everyone was assuming that $\varepsilon_0$ was well-ordered. This lead to a bit of disagreement (in a nice way!) about the ...
- 32.9k
4
votes
1
answer
364
views
What countable ordinals are called $\kappa_\alpha$?
Jervell has a notation for countable ordinals up to the small Veblen ordinal using trees:
• Herman Ruge Jervell, How to wellorder finite trees
and get good ordinal notations, Berkeley Logic ...
- 20.9k
13
votes
2
answers
1k
views
How can any theory prove well-foundedness of ordinals above $\omega_1^{\text{CK}}$?
$\newcommand{\omegaoneck}{\omega_1^{\text{CK}}}$
Pardon the extremely basic question - this isn't quite my area - but I'm confused about the definition of proof theoretic ordinals.
The proof ...
- 877
10
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 ...
- 129
8
votes
1
answer
649
views
Which ordinals are proof-theoretic ordinals?
Few months ago I have posted this question on MO, but I must admit that at the time, admittedly, I had no idea on how technical proof-theoretic considerations can be. I have decided to revise this ...
- 26.2k
13
votes
1
answer
1k
views
Peano arithmetic vs. fast-growing hierarchy with pathological fundamental sequences
Fundamental sequence for a countable limit ordinal $\alpha$ is an increasing sequence $\{\alpha[i]\}$ of ordinals of length $\omega$ such that $\lim_{i\rightarrow\omega}\alpha[i]=\alpha$. There are ...
- 26.2k
12
votes
1
answer
706
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 ...
- 26.2k
7
votes
2
answers
455
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 ...
28
votes
1
answer
2k
views
Why isn't this a computable description of the ordinal of ZF?
In a previous MO question, I was told by several commenters that
(a) it's known that there exists a computable ordinal $\alpha_{ZF}$ that "encodes the strength of ZF set theory" (i.e., a least ...
- 9,623
19
votes
0
answers
561
views
Can Gentzen-style proofs give omega-consistency and beyond?
In 1936, Gentzen famously showed that Primitive Recursive Arithmetic, plus the assumption that the ordinal $\epsilon_0$ is well-founded, is able to prove Con(PA). But of course, Con(PA) doesn't yet ...
- 9,623
39
votes
2
answers
3k
views
Is there a computable ordinal encoding the proof strength of ZF? Is it knowable?
In comments on Quora (see, for example, here, here, here), Ron Maimon has repeatedly expressed the strong opinion that Hilbert's program was not killed by Gödel's results in the way typically ...
- 9,623
16
votes
1
answer
544
views
Nontrivial upper bounds on proof-theoretic ordinals of strong theories: do we have any?
Motivated by Consistency of Analysis (second order arithmetic) and Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?, I have the following question:
Are there any examples of strong ...
- 18.2k
12
votes
1
answer
828
views
What is the proof-theoretic ordinal of PA + Con(PA), PA + Con(PA + Con(PA)) etc., and why?
I seem to remember having read that the proof-theoretic ordinal (sup of ordinals the theory can prove well-ordered) of $\mathsf{PA} + \mathsf{Con}(\mathsf{PA})$ is the same as that of $\mathsf{PA}$, ...
- 141
3
votes
0
answers
805
views
What is the role of the (formalized) omega rule in Ramified Analysis?
In the 1960's, Feferman and Schutte did groundbreaking proof-theoretic work to find out the strength of predicative systems of second-order arithmetic. They used the ramified theory of types, a ...
- 4,471
3
votes
2
answers
732
views
What is the proof-theoretic ordinal of Hyperarithmetical Comprehension?
As I discuss in my answer here, it seems to me that Solomon Feferman shows, on pages 10-11 of his seminal 1964 paper "Systems of Predicative Analysis", that if you consider predicative second-order ...
- 4,471
5
votes
1
answer
668
views
Can the Burgess-Hazen analysis of Predicative Arithmetic be extended to Transfinite Types?
Around page 300 of his book "Mathematical Thought and its Objects", Charles Parsons discusses the work of Edward Nelson, who believes that mathematical induction is impredicative, because it can be ...
- 4,471
4
votes
0
answers
642
views
Is there a notion of "predicative given the real numbers"?
A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...
- 4,471