# Proof-theoretic ordinals and the Axioms of Replacement

According to this Wiki article, ZFC-R (ZFC without the Axioms of Replacement) cannot construct $\omega \cdot 2$. It also claims that $V_{\omega\cdot 2}$ is a model of ZFC-R and is sufficient to do basically all of second-order arithmetic.

(It also seems to refer to ZFC-R as Z, which isn't clear to me that they're equivalent.)

However, in this article it says that the proof-theoretic ordinal of a theory is the smallest recursive ordinal that the theory can't prove to be well-founded. It then further claims that the proof-theoretical ordinal of second-order arithmetic is (currently) undescribably large--far larger than $\omega \cdot 2$. Since ZFC-R can do second-order arithmetic, its proof-theoretical ordinal must be at least as large.

So how is it that ZFC-R can prove that $\omega\cdot 2$ is well-founded, but apparently cannot prove it exists?

## 1 Answer

You need to distinguish between well ordered sets and von Neumann ordinals. While $\sf ZFC-R$ cannot prove the existence of von Neumann ordinals $\geq\omega+\omega$, it can prove the existence of many well ordered sets. In fact, in $V_{\omega+\omega}$ any order type below $\beth_\omega$.

The term proof theoretic ordinal has a technical meaning to it, and it is in fact a countable ordinal. It is not the term for the largest von Neumann ordinal that a theory can prove to exist, though.

(To wit, if $M$ is any countable transitive model of $\sf ZFC-R$, then it contains only countably many ordinals, and countably many sets. So only countably many order types exist there. And we could ask what is the least order type of a set that provably exists in a transitive model of $\sf ZFC-R$. This has to be a countable ordinal.)

• +1. For the OP: elaborating on the first sentence of this answer's second paragraph, the proof-theoretic ordinal is defined in terms of computable linear orders which the theory in question can prove are well-founded; this is a very different thing from definable ordinals which the theory can prove exist. There are lots of ways to ask, "How large are the ordinals that this theory can 'get'?", and they're not equivalent. For yet a third, look at this paper by Arai. – Noah Schweber Jan 11 '17 at 19:01
• @NoahSchweber So, if I understand you correctly, ZFC-R can prove that sets with the order type $\omega\cdot 2$ exist, but not that the specific set $\{\omega + n: n\in N\}$ exists? – eyeballfrog Jan 11 '17 at 20:50
• @eyeballfrog Exactly. For instance, the set $$\{(m, n): \mbox{m is even and n is odd, or m and n have the same parity and m<n}\}$$ is a linear order with ordertype $\omega+\omega$, and ZFC-R proves that it exists. – Noah Schweber Jan 11 '17 at 21:06
• @eyeballfrog: Yes. – Asaf Karagila Jan 11 '17 at 21:06
• And I guess one final question, which might seem obvious given the above, but I want to be sure I understand. There exists some ordinal (though we don't know what it is yet) that ZFC-R cannot prove any sets with that order type exist, right? – eyeballfrog Jan 11 '17 at 21:14