Does consistency of second order arithmetic prove existence of omega models?

Question

Is the following a theorem of second order arithmetic $Z^2$?

$Con(Z^2) \to \exists M (M \text { is an } \omega \text {-model of } Z^2)$

Answer 1

Hopefully not!

(Specifically: the implication in question is provable in $Z_2$ iff the theory $Z_2+Con(Z_2)$ is inconsistent, and in that case it's provable for silly reasons.)

---

Assuming $Z_2+Con(Z_2)$ is consistent:

Consider the theory $T=Z_2$ + $Con(Z_2)$ + $\neg Con(Z_2+Con(Z_2))$. By Godel, this is consistent since $Z_2+Con(Z_2)$ is, and $T$ trivially proves $Con(Z_2)$.

However, $T$ also proves that $Z_2$ has no $\omega$-model as follows:

• If $M$ were an $\omega$-model of $Z_2$, then $M$ would satisfy $Con(Z_2)$ since $Con(Z_2)$ is arithmetic and true.

• But then $M$ would be a witness to the consistency of $Z_2+ Con(Z_2)$, and that's not consistent.

So $T$ disproves the implication in question, and so $Z_2$ can't prove the implication in question since $T$ is a consistent extension of $Z_2$.

---

Assuming $Z_2+Con(Z_2)$ is inconsistent:

This winds up being boring: if $Z_2+Con(Z_2)$ is inconsistent, then $Z_2$ proves $\neg Con(Z_2)$ and so proves the implication in the question vacuously.

---

Finally,note that basically nothing about $Z_2$ was used here; really the only subtlety is the issue of how exactly we talk about satisfaction of a sentence in a structure. The issue is that the natural definition of "$M\models\varphi$" is $\Sigma^1_1$ ("There is a family of Skolem functions for $\varphi$ over $M$"), but:

• If we want to be able to prove for each $\varphi$ the sentence $$\forall M(M\models\varphi\vee M\models\neg\varphi),$$ then we need ACA$_0$.

• If we want to be able to prove the sentence $$\forall M,\varphi(M\models\varphi\vee M\models\neg\varphi),$$ then we need the slightly-stronger theory ACA$_0^*$ (which is ACA$_0$ + "For all $n,X$, the $n$th jump of $X$ exists"); this is equivalent to ACA$_0$ for $\omega$-models, but has slightly stronger first-order part.

• Finally, if we want to be able to prove the sentence $$\forall M(Th(M)\mbox{ exists}),$$ we need ACA$_0^+$ (which is ACA$_0$ + "For all $X$ the $\omega$th jump of $X$ exists").

The general idea is that "obvious" model-theoretic arguments can be blithely skipped over at the level of ACA$_0^+$. (Ironically, the really deep model-theoretic fact - compactness - is quite weak in this context, being only at the level of WKL$_0$! This is a good example of how in reverse math we sometimes get surprising strength from "trivialities," in this case the bivalence of truth.)

If we want to go lower - say, to RCA$_0$ - the key is to define "($\omega$-)model" correctly: here it will suffice to have a model of a theory $T$ be a structure together with an appropriate indexed collection of Skolem functions (and an isomorphism between the first-order part and $\omega$).