2
$\begingroup$

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

  • 0
    See also: http://math.stackexchange.com/a/1368646/758672016-12-10

1 Answers 1

2

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

  • 0
    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)$ ?2011-03-23