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

This is related to my first question. In order to get what I don't get, I ll go with something much more specific here.

It is well known that $ZF \vdash Con(ZF) \longrightarrow Con(ZF + AF)$. The way I know to proove it uses :

Lemma 1 : If $T$ and $S$ are two theories in set theory language, $M$ is a class (i.e. a formula $\phi(x)$ tell if $x$ is in $M$ or not) and $T \vdash \mbox{"}M$ is a model for $S$", then $Con(T) \vdash Con(S)$

So we have to build a class, say $V=\cup_{\alpha \in ORD} V_{\alpha}$ and then $ZF$ is suppose to demonstrate, for instance, that $V$ satisfies comprehension axiom scheme.

We can use :

Lemma 2 : $(\forall x \in M$, $P(x) \subset M) \longrightarrow$ comprehension scheme is true in $M$

With Lemma 2, the proof is straightforward. My problem is that I do not know why lemma 2 would be a ZF theorem. I don't even know how it could be written in ZF language, since there is an infinite number of axiom to write, and since $V$ is a class, there is no formula $\theta(\ulcorner f \urcorner)$ saying $V \vDash f$

Of course, for all formulas $F$ of the comprehension scheme, we can write

$ZF \vdash (\forall x \in M$, $P(x) \subset M) \longrightarrow F^M$

but if we do that for all formulas, the proof will be infinite...

share|cite|improve this question
up vote 2 down vote accepted

(In what follows, I am assuming that ZF consists of Extensionality, Pairing, Union, Comprehension, Replacement, Infinity and Power Set, and that AF is the Axiom of Foundation.)

I think that the somewhat formal way of looking at all of this is to basically work by contrapositive. Working in ZF, assume $\neg \mathrm{Con} ( \text{ZF+AF} )$. Then there is a proof of some obvious contradiction, say $( \forall x ) ( x = x ) \wedge \neg ( \forall x ) ( x = x )$, in ZF+AF. Furthermore, ZF is able to code proofs/formulas as sets/natural numbers in a standard manner. This proof can only consist of finitely many axioms from ZF+AF, say $\phi_1 , \ldots , \phi_n$. Also in ZF we can construct the class of well-founded sets, denoted (as in Kunen) by $\mathbf{WF}$, and in ZF we can prove that $\mathbf{WF} \models \phi_1 \wedge \cdots \wedge \phi_n$, and therefore it must be that ''$\mathbf{WF} \models ( \forall x ) ( x = x ) \wedge \neg ( \forall x ) ( x = x )$'' is a theorem of $\text{ZF} + \neg \mathrm{Con} ( \text{ZF+ AF} )$. Formally, using relativisation, we have that $$\text{ZF} + \neg \mathrm{Con} ( \text{ZF+AF} ) \vdash ( \forall x \in \mathbf{WF} ) ( x = x ) \wedge \neg ( \forall x \in \mathbf{WF} ) ( x = x ),$$ and thus $\text{ZF} \vdash \neg \mathrm{Con} ( \text{ZF+AF} ) \rightarrow \neg \mathrm{Con} ( \text{ZF} )$.

share|cite|improve this answer
Awesome ! This answers everything I was wondering. thx a lot. So despite the fact that this is wrong to say $ZF \vdash \mbox{"}WF \vDash ZF\mbox{"}$, this is true to say $ZF \vdash Con(ZF) \rightarrow Con(ZF+AF)$ – Archimondain Mar 22 '11 at 17:54
Actually, $\neg Con(ZF + AF)$ says there is a proof of some obvios contradiction, but why would this proof be standard ? If it is not, how to proove $\neg Con(ZF)$ ? – Archimondain Mar 23 '11 at 9:47

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.