Skip to main content

All Questions

Filter by
Sorted by
Tagged with
9 votes
0 answers
264 views

Consequences of recent claims of Ordinal Analysis of $Z_2$

Recently Toshiyasu Arai submitted "An ordinal analysis of $\Pi_{N}$-Collection" and Henry Towsner submitted "Proofs that Modify Proofs", both of which claim ordinal analysis of ...
solatia's user avatar
  • 161
6 votes
0 answers
181 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. Note on terminology: "admissible", "$(^+)$-stable", and "$\Pi^1_1$-...
C7X's user avatar
  • 2,031
1 vote
0 answers
122 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 ...
Reflecting_Ordinal's user avatar
5 votes
1 answer
360 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 \...
Victor's user avatar
  • 2,136
6 votes
1 answer
292 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 ...
Keshav Srinivasan's user avatar
0 votes
0 answers
157 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 ...
Reflecting_Ordinal's user avatar
6 votes
0 answers
183 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 $\...
Nik Weaver's user avatar
  • 42.8k
5 votes
0 answers
265 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 ...
Dmytro Taranovsky's user avatar
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 ...
Gabriel Nivasch's user avatar
10 votes
1 answer
258 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 ...
Harry Altman's user avatar
  • 2,585
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$. ...
Alwe's user avatar
  • 178
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 $...
Thomas Benjamin's user avatar
3 votes
0 answers
144 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 ...
Dmytro Taranovsky's user avatar
4 votes
0 answers
367 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. ...
Dmytro Taranovsky's user avatar
4 votes
1 answer
887 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 ...
Robin Saunders's user avatar
8 votes
1 answer
295 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 ...
Łukasz Lew's user avatar
2 votes
1 answer
542 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) | \...
Boris Dimitrov's user avatar
10 votes
1 answer
358 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 ...
Dmytro Taranovsky's user avatar
10 votes
1 answer
373 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$ ...
Erfan Khaniki's user avatar
8 votes
1 answer
706 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 ...
Wojowu's user avatar
  • 28.2k
14 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 ...
Wojowu's user avatar
  • 28.2k
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 ...
Wojowu's user avatar
  • 28.2k
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 ...
Eliezer Yudkowsky's user avatar
15 votes
1 answer
605 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 ...
Noah Schweber's user avatar
13 votes
1 answer
982 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}$, ...
Benya's user avatar
  • 151
3 votes
0 answers
853 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 ...
Keshav Srinivasan's user avatar
3 votes
2 answers
814 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 ...
Keshav Srinivasan's user avatar
5 votes
1 answer
720 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 ...
Keshav Srinivasan's user avatar
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 ...
Primitive Recursive Fab's user avatar
10 votes
1 answer
735 views

Arithmetic strength of Peano + the Howard ordinal

Consider the theory $\mathrm{PA}+\mathrm{BHO}$ consisting of first-order Peano arithmetic ($\mathrm{PA}$) enriched by an axiom scheme which allows well-founded induction up to any ordinal less than [a ...
Gro-Tsen's user avatar
  • 32.5k
8 votes
2 answers
824 views

Ordinal Analysis of Peano Arithmetic with Restricted Induction

If we take Peano Arithmetic and restrict induction to formulas over various fragments of the arithmetic hierarchy, say to the $\Sigma^0_n$ formulas for various $n$ or some other interesting fragments, ...
Russell O'Connor's user avatar
16 votes
1 answer
2k views

Proof theoretic ordinal

In Ordinal Analysis, Proof-theoretic Ordinal of a theory is thought as measure of a consistency strength and computational power. Is it always the case? I. e. are there some general results about ...
SNd's user avatar
  • 161