How can ZF prove relative consistency for itself?

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

-

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