Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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)$?
share|cite|improve this question
@user10811: If Andres' answer cleared up your question please mark it as the accepted answer (the transparent check mark under the answer's reputation). – Asaf Karagila May 16 '11 at 8:38
up vote 12 down vote accepted

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

share|cite|improve this answer
Amazing answer! Thank you very much. – user10811 May 12 '11 at 16:51
Looking at the model-theoretical point of view, I have two questions: 1.completeness theorem is proved in ZF-P-Reg and the fact that $ WF^M $ satisfies ZF depends only from the fact that M models ZF-Reg so is it correct to write $ ZF-P-Reg \vdash con(ZF-Reg)\implies con(ZF)$? 2. we have two proofs (model-theoretic and syntactical) and for each of them we have a finitistic metatheoretic proof and a formalized proof.Is it true that the metatheoretic model-theoretical proof, that is substantially the same as the formalised cited above, use a sort of completeness theorem but thought in metatheory? – eagle Jun 27 '15 at 3:29
@eagle On question 1, yes. In fact, much weaker theories suffice to formalize this implication. – Andrés E. Caicedo Jun 28 '15 at 17:37

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.