# Questions tagged [ordinal-analysis]

The tag has no usage guidance.

39 questions
Filter by
Sorted by
Tagged with
87 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$-...
• 470
78 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 ...
1 vote
198 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 ...
• 5,268
145 views

• 5,782
417 views

### What system suffices to show the strength of PRA is $\omega^\omega$?

Russell O'Connor wrote in 2009 (link): PRA has consistency strength equivalent to the well-foundness of $\omega^\omega$, which can be stated again as the termination of some other program on all ...
• 31.2k
135 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 ...
• 4,071
221 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 ...
• 4,071
268 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. ...
• 4,071
635 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 ...
• 3,148
237 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 ...
• 255
439 views

• 1,659
331 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 ...
• 19.4k
968 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 ...
• 857
1k views

### Why is there a need for ordinal analysis?

Consider the Peano axioms. There exists a model for them (namely, the natural numbers with a ordering relation $<$, binary function $+$, and constant term $0$). Therefore, by the model existence ...
• 119
594 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 ...
• 23.7k
419 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 ...
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 ...
• 9,465
533 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 ...
• 9,465
3k 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 ...
• 9,465
751 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}$, ...
• 141
772 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,979
661 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 ...
• 3,979
621 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 ...
• 3,979
602 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 ...
• 3,979
3k views

### Why do stacked quantifiers in PA correspond to ordinals up to $\epsilon_0$?

I am trying to understand why induction up to exactly $\epsilon_0$ is necessary to prove the cut-elimination theorem for first-order Peano Arithmetic; or, as I understand, equivalently, why the length ...
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, ...