Understanding an Easy Relative Consistency Proof

When proving that $(ZF-Reg)\vdash CON(ZF - Reg)\rightarrow CON(ZF)$ we start by defining the class $WF=\cup_{\alpha \in ORD} V_{\alpha}$. Then we prove with $ZF-Reg$ that actually $WF$ is a model for $ZF$ using several absoluteness results. So my questions are:

• Where in this proof are we using $CON(ZF-Reg)$?
• If the answer to my first question is we are using the fact that the class of all hereditary sets $V$ is a model for $ZF-Reg$ isn't this a lot stronger than just asuming $CON(ZFC)$?

Solution 1:

What you are doing is describing a procedure that, within $V$, isolates the class $WF$. So far, we are not using $CON(ZF-Reg)$. But note that so far we have not concluded $CON(ZF)$ either.

Now, assume $CON(ZF-Reg)$. This means (by the completeness theorem) that there is a (set) model $M$ of $ZF-Reg$. But then your procedure shows how you can identify a subcollection $WF^M$ of $M$ that is a model of $ZF$. So, now, you have $CON(ZF)$.

There is also a way of arguing syntactically that avoids the completeness theorem: Assume $CON(ZF)$ fails. This means that there is a proof of a contradiction $\psi\land\lnot\psi$ from the axioms of ZF. This proof uses only finitely many axioms, say $\phi_1,\dots,\phi_n$. The proof that the class $WF$ is a model of $ZF$ is actually a metatheorem: For each axiom $\phi$ of $ZF$ you can identify a finite collection $T_\phi$ of axioms of $ZF-Reg$ that imply that $WF$ is a model of $\phi$ or more precisely, $T_\phi$ proves the relativized formula $\phi^{WF}$. Using basic properties of relativizations such as $(\psi\to\rho)^{WF}$ being $\psi^{WF}\to\rho^{WF}$ and $(\lnot\psi)^{WF}$ being $\lnot(\psi^{WF})$, it follows that from the finitely many formulas $\phi_i^{WF}$ you can prove the contradiction $\psi^{WF}\land\lnot(\psi^{WF})$.

But this implies that the finite family $\bigcup_i T_{\phi_i}$ of axioms of $ZF-Reg$ is inconsistent, and therefore so is $ZF-Reg$, i.e., $CON(ZF-Reg)$ fails.

Note that the two arguments I sketched have nothing to do with the specifics of $ZF-Reg$ or $ZF$. They show how, once you know that there is a procedure that gives you the class model of one theory, you can conclude the implication between consistencies you were actually interested in. This is why many consistency results in set theory simply tell you how to produce a class model. Then the same argument as above gives you the actual consistency result.

There is a subtle point that I feel I need to address. There is no truth predicate for proper classes, this is Tarski's theorem on undefinability of truth. This means that it is not a theorem of $ZF-Reg$ that $WF$ is a model of $ZF$. Above, I called this a metatheorem. The point is that proofs use only finitely many axioms, while what we have is a recursive procedure that for each axiom $\phi$ of $ZF$ isolates a finite set $T_\phi$ of axioms of $ZF-Reg$ that imply $\phi^{WF}$. But then, the actual "proof" that $ZF$ holds in $WF$ would require infinitely many axioms, namely, those in $\bigcup_\phi T_\phi$.

This is not as strange as it may first sound. Note that there is no proof in $ZF$ that $ZF$ holds in $V$, for exactly the same reason.

On the other hand, if $M$ is a set model, then truth in $M$ is definable. In fact, there are formulas $\phi(x,y,z)$ and $\psi(x,y,z)$ that are $\Sigma_1$ and $\Pi_1$, respectively, such that (a weak fragment of) $ZF-Reg$ proves are equivalent and, for any sets $A,B,C$, we have that $$\phi(A,B,C)$$ holds iff $A=(M,E)$ is a structure in the language of set theory, $B$ codes a formula $\rho(\vec w)$, $C$ is a finite tuple of elements of $M$ (of the same length as $\vec w$, and $$ (M,E)\models\rho(C).$$ This means that, in contrast to the situation above, we can prove (as a theorem of $ZF-Reg$) that if $M$ is a set model of $ZF-Reg$, then $WF^M$ is a model of $ZF$. This is because we can readily formalize our metatehorem, once we can uniformly talk about satisfiability of formulas (which is what the truth predicate $\phi$ buys us).