# Questions tagged [ordinal-analysis]

The tag has no usage guidance.

39 questions
Filter by
Sorted by
Tagged with
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
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 ...
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
969 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
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
291 views

### What is the proof-theoretic ordinal of bare $\mathsf{NFU}$?

On the Stanford Encyclopedia of Philosophy article on alternative axiomatic set theories, it is stated without reference that bare $\mathsf{NFU}$ (i.e., $\mathsf{NFU}$ without the axiom of infinity) ...
• 6,394
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
210 views

### Is there a relation between type (maximum linearization) of a computable WQO and the ordinal strength of a theory needed to prove it?

Background: Given a well partial order $X$ (more commonly studied with antisymmetry dropped as well-quasi-orders, but I'm going to say well partial order to make this definition simpler, obviously ...
• 2,385
300 views

### Complexity of induction formulas in proof theoretic ordinals

According to The Art of Ordinal Analysis, the proof theoretic ordinal of a theory $T$ is the least ordinal $\alpha$ such that: $${\bf ERA}+TI(\alpha,ECP)\vdash Con(T)$$ In above definition, $ECP$ ...
• 1,659
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
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 ...
• 1,108
784 views

### Ordinal Analysis of Peano Arithmetic with Restricted Induction

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, ...
• 1,379
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
562 views

### Gentzen's result on PA

The Wikipedia states that Gentzen proved that "in modern terms, the proof-theoretic ordinal of PA is $\varepsilon_0$." Further down, the article defines what the "proof theoretic ordinal" of a theory ...
• 1,002
785 views

### ERA, PRA, PA, transfinite induction and equivalences

I'm quite sure I don't understand very well the links between proof theoretical ordinals of theories, the axioms of transfinite induction and the objects a theory can prove to exist. For instance I'm ...
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
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,091
420 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 ...
415 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 (...
• 7,129
271 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$. ...
• 178
334 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$): ...
622 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
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
146 views

Consider the theory ${\rm PA}^{\mathbb{T}}$ obtained by adding a truth predicate to Peano arithmetic, applicable to sentences of the unaugmented language and satisfying the compositionality axioms $\... • 37.4k 5 votes 0 answers 187 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 ... • 161 5 votes 0 answers 188 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,091 4 votes 1 answer 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.5k 4 votes 0 answers 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,091 3 votes 2 answers 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 3 votes 1 answer 636 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 3 votes 0 answers 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,091 3 votes 0 answers 773 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 3 votes 0 answers 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 2 votes 1 answer 441 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) | \... 1 vote 3 answers 873 views ### Regarding Gentzen's note regarding 'Godel-points' (i.e., "Where is the Godel-point hiding?") Consider the following note written by Gerhard Gentzen in early 1932, on the onset of his work on a consistency proof for arithmetic: The axioms of arithmetic are obviously correct, and the ... • 5,792 1 vote 1 answer 343 views ### What does "can almost be proven in PA" mean regarding Theorem 2 of Timothy Chow's expository article, "The Consistency of Arithmetic"? In his expository article, "The Consistency of Arithmetic" (MSN), Prof. Chow has the following theorems: Theorem 1. If$a_1, a_2, a_3,\dotsc$is a sequence of ordinals and$a_i \ge a_j$whenever$...
• 5,792
1 vote
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 ...