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

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)$$.

• What is P here? Power set axiom? Jun 10, 2020 at 23:41
• Yes, P is Power Set axiom. Jun 11, 2020 at 0:11
• What's the meaning of ZFC $\Rightarrow$ Con(X) (where X is a set of axioms)? I don't understand "ZFC" as an assertion (while "$M$ is a model of ZFC" or "Con(ZFC)") are logical assertions). (Oh, it's just been edited, thanks)
– YCor
Jun 12, 2020 at 12:53

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.
• I agree with the part that if $n \in X_{ZFC-P}$ represents some real axiom of $ZFC-P$, then $H_{\omega_1} \models n$. However, $ZFC$ allows nonstandard models which have nonstandard natural numbers. Such natural numbers have infinite predecessors looking from outside but are regarded as finite numbers inside the model. When we define $X_{ZFC-P}$, we are using some formula $\phi$ such that $X_{ZFC-P}=\{ n : \phi (n) \}$. It is not clear if $X_{ZFC-P}$ contains nonstandard naturals. If $n_0 \in X_{ZFC-P}$ is nonstandard, we don't have a corresponding axiom in ZFC-P to $n_0$. - Jun 11, 2020 at 0:01
• -In this case it is not clear if $H_{\omega_1} \models n_0$. Jun 11, 2020 at 0:02
• @FengLiang In any model of ZFC that has nonstandard natural numbers, some of them will be in $X_{ZFC-P}$, but that makes no difference. It is a theorem of ZFC (and therefore true in all models of ZFC, even nonstandard ones) that $H_{\omega_1}$ satisfies all axioms of ZFC-P (and "all" here means all in the sense of the model, including nonstandard axioms). Jun 11, 2020 at 2:29
• Do you know where I can find a proof of it? To be clear, we need to show: $ZFC \vdash H_{\omega_1} \models X_{ZFC-P}$, which is stronger than the statement: assuming $ZFC$, $H_{\omega_1}$ is a model of $ZFC-P$. For the latter one, it is proved as Theorem 6.5 in Chapter IV of Kunen's book. I agree with that proof, but all it proved is only all standard axioms of $ZFC-P$ are true in $H(\omega_1)$. Besides that, I don't know a proof of $ZFC \vdash H_{\omega_1} \models X_{ZFC-P}$. Jun 11, 2020 at 2:51