Skip to main content

All Questions

Filter by
Sorted by
Tagged with
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
1 vote
0 answers
123 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 $\...
Zuhair Al-Johar's user avatar
1 vote
0 answers
127 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....
Zuhair Al-Johar's user avatar
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
5 votes
0 answers
115 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$-...
Binary198's user avatar
  • 704
1 vote
1 answer
251 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 ...
Zuhair Al-Johar'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
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
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
14 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 ...
John Gowers's user avatar
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
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