Formal proof of $ZFC \vdash CON(\ulcorner ZFC-P\urcorner)$

Question

I am wondering that if one can show $ZFC \vdash CON(\ulcorner ZFC-P \urcorner)$. There is an argument in Set Theory, An Introduction to Independence Proofs by Kunen (page 145), but I am confused about the proof.

Let $\phi$ be the formula for the coding of $ZFC-P$ in natural numbers, and $X_{ZFC-P}=\{n\in \omega :\phi(n)\}$.

By Godel Completeness Theorem as the formal sentence $\forall X (CON(X) \leftrightarrow \exists \mathfrak{M}(\mathfrak{M} \models X) )$, it is enough to prove that: $ZFC \vdash H(\omega_1) \models X_{ZFC-P} $, or say $ZFC \vdash \forall x \in X_{ZFC-P} (H(\omega_1) \models x)$. By Completeness and Soundness Theorems, it is enough to show that whenever $M$ is model of $ZFC$, $M$ models $\forall x \in X_{ZFC-P} (H(\omega_1) \models x)$. This amounts to showing for all $x \in X_{ZFC-P}$, $H(\omega_1) \models x$ is true in $M$.

However, if $M$ is a nonstandard model which has nonstandard natural numbers, $X_{ZFC-P}$ may be strictly larger than the actual collection of codings of $ZFC-P$. Let $x_0$ be the coding of a nonstandard axiom $\psi$ which has infinite length looking from outside while we have $\phi(x_0)$. In Kunen's book, they showed $H(\omega_1) \models x$ for actual axioms of $ZFC-P$, but not for infinite sentences like $\psi$.

In fact, $CON(\ulcorner ZFC-P \urcorner)$ as a formal sentence also includes possible nonstandard axioms. I am wondering that if there is a way to deal with these nonstandard axioms, or if one can show $ZFC \vdash CON(\ulcorner ZFC-P \urcorner)$.

Answer 1

You can directly show from $ZFC$ that $\forall n \in X_{ZFC-P}\, \colon \, ( H(\omega_1) \vDash n)$. To see this remind yourself that $ \vDash$ is expressible by a single formula $\psi$, so that $H(\omega_1) \vDash \varphi(z_1,...,z_m)$ iff $\psi(H(\omega_1), \ulcorner \varphi \urcorner, \vec{z},1)$. Now for $n \in X_{ZFC-P}$ you have a finite case distincition what kind of axiom $n$ is. E.g. if $n$ is ` $\forall A \, \forall \vec{z} $ replacement for the formula $\varphi_n(x,y, \vec{z})$ with respect to $A$ holds ', let $A \in H(\omega_1)$ and $\vec{z} \in H(\omega_1)^{<\omega}$ be arbitrary and define the set $$B:=\{y \in H(\omega_1) \, \colon \, \exists x \in A \, \, H(\omega_1) \vDash \varphi_n(x,y, \vec{z})\}.$$ Finally prove that $B \in H(\omega_1)$, and so $H(\omega_1) \vDash n$. The subtlety here is that you are only using replacement with respect to $\psi$. Therefore, this is a finite proof.

On the meta-level, for every finite $\Delta \subseteq ZFC$ you can prove $CON(\Delta)$. But $ZFC$ does not prove $\forall \Delta \subseteq ZFC \, \text{finite}\, \colon CON(\Delta)$ as this would contradict Gödel's second Incompleteness Theorem.