Questions tagged [ordinal-analysis]

The tag has no usage guidance.

11 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
19
votes
0answers
480 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 ...
7
votes
0answers
200 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 ...
6
votes
0answers
234 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$. ...
5
votes
0answers
150 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 ...
5
votes
0answers
148 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 ...
4
votes
0answers
275 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 (...
4
votes
0answers
237 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. ...
3
votes
0answers
129 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 ...
3
votes
0answers
739 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 ...
3
votes
0answers
561 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 ...
2
votes
0answers
281 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) | \...