Questions tagged [ordinal-analysis]
The ordinal-analysis tag has no usage guidance.
11
questions with no upvoted or accepted answers
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) | \...
