# Tag Info

Accepted

### Is there a computable ordinal encoding the proof strength of ZF? Is it knowable?

Rom Maimon is describing the program of proof-theoretic ordinal analysis. First, as you observed in your addendum, it isn't interesting to find some encoding of an ordinal whose well-foundedness ...
• 6,965
Accepted

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

The axioms of first-order arithmetic include the induction schema, which says that, for every formula $A(x)$ with free variable $x$, the conjunction of $A(0)$ and $\forall x\,(A(x)\to A(x+1))$ implies ...
• 68.1k
Accepted

• 14.5k
Accepted

### Which ordinals are proof-theoretic ordinals?

If $\alpha$ is a reasonable presentation of a computable ordinal then the proof-theoretic ordinal of $ACA_0+\alpha$ is well-ordered is the smallest $\epsilon$ number $>\alpha$. (There's a proof of ...
• 6,965
Accepted

### Models of PRA/EFA with induction on $X$ but not $\omega^X$

I suspect the paper you want is Avigad and Sommer, A Model-Theoretic Approach to Ordinal Analysis. As the name suggests, they give an ordinal analysis rooted in the structure of models of arithmetic. ...
• 6,965

### How can any theory prove well-foundedness of ordinals above $\omega_1^{\text{CK}}$?

This is a difference between internal and external quantification. Proof-theoretic ordinal analysis involves an external quantification over (external, recursive) ordinals. What is provable in ZFC ...
Accepted

### A question about ordinal analysis

First of all, note that we don't (yet) have ordinal analyses of subsystems of second order arithmetic beyond $\Pi^1_2$-CA$_0$. Still, we can say something about the pattern you indicate using known ...
• 1,340
Accepted

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

Let me show that for extensions $T\supseteq\mathsf{ACA}_0$ the usual proof-theoretic ordinal $|T|_{WO}$ coincide with $|T|_{WPO}$ that is the suprema of $\mathsf{o}(X)$, for recursive wpo $X$, for ...
• 3,458

### What does "can almost be proven in PA" mean regarding Theorem 2 of Timothy Chow's expository article, "The Consistency of Arithmetic"?

I believe you're overthinking what Chow means by "almost provable." We have an arithmetic statement of the form $$(*)\quad\forall x\varphi(x),$$ which while not provable in PA has the property that ...
• 21.7k

### Going beyond the strength of Peano arithmetic "without sets"

A lot of work has been done on (1) various systems of ordinal notations ranging from very weak to very strong and (2) calibrating the proof theoretic strength of various formal systems, say in terms ...
• 37.2k

### Iterated Gentzen: or, a Sith objection to the proof of consistency of PA

Mathobi is making a different argument in the comments on this post than in the question itself: in the post Mathobi is considering how far we need to justify transfinite induction to prove $G(i)$ ...
• 293

### Models of PRA/EFA with induction on $X$ but not $\omega^X$

The easiest way to construct a model $M$ of PRA where the Ackermann function is not total is to take a nonstandard model $M_0$ of, say, PA, fix a nonstandard element $a\in M_0$, and define $M$ as the ...
• 38.8k

• 4,061
Accepted

### Does this restriction on powersets in ZF have a proof theoretic ordinal?

Your theory interprets $\mathsf{ZF}^-$. In fact, $\mathsf{ZF}-$ (namely, $\mathsf{ZF}$ without Powerset) interprets $\mathsf{ZF}^-+(V=L)$. It answers your questions negatively since the proof-...
• 1,577

### Regarding Gentzen's note regarding 'Godel-points' (i.e., "Where is the Godel-point hiding?")

Gentzen's remark has some bite in the case the standard first-order arithmetic PA, because we plausibly know a bit more arithmetically. But he apparently did not understand the generality of the ...
Let $\mathsf{KPh}$ denote the theory $\mathsf{KP}+\textrm{The recursively inaccessibles are unbounded}\! "$. I haven't found an explicit analysis of $\mathsf{KPh}$ in Rathjen's preprints, but there ...