Skip to main content

All Questions

Filter by
Sorted by
Tagged with
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 ...
Imperishable Night's user avatar
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
2 votes
0 answers
194 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 ...
C7X's user avatar
  • 2,031
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
365 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 ...
Simon Henry's user avatar
  • 42.4k
5 votes
1 answer
310 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, ...
C7X's user avatar
  • 2,031
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
5 votes
0 answers
262 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 ...
user115415's user avatar
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
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
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
8 votes
0 answers
287 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 ...
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
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
5 votes
1 answer
411 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$): ...
Julian Barathieu's user avatar
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 ...
Keith Millar's user avatar
  • 1,252
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
6 votes
1 answer
474 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 ...
David Roberts's user avatar
  • 35.4k
5 votes
1 answer
409 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 ...
John Baez's user avatar
  • 22.3k
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
27 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 ...
Scott Aaronson's user avatar
19 votes
0 answers
590 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 ...
Scott Aaronson's user avatar
40 votes
2 answers
4k 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 ...
Scott Aaronson'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
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
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