in Jech's paper:
On Gödel's Second Incompleteness Theorem
http://www.math.psu.edu/jech/preprints/goedel.pdf
He proves:
Theorem if ZF proves there is a model of ZF, then ZF proves 0=1.
In the beginning of the proof he passes to a “big enough” finite subset S of ZF (that proves there is a model of ZF and defines formulas and their satisfaction etc.)
The proof goes by looking at a model M of S and models of S within M, which can be lifted to be a model in the ‘outside world’, and using some diagonal sentence G for a contradiction.
My question:
Why does passing to a finite subset needed for the proof?
Another question:
If once actually builds a model of set theory, the above theorem proves that ZF is inconsistent. But would that mean one could explicitly write down a list of inferences that will derive a contradiction? Could we be sure such a list exists?
Thanks,
Doron
Best Answer
There's a subtle point at the bottom of the first page and top of the second, to wit:
"For every sentence σ, $M\vDash\sigma$ iff $N\vDash(m\vDash\sigma)$. In particular, $N\vDash$ (m is a model)."
If "model" means "model of ZF", then one cannot conclude this. It is possible that N knows, for each particular σ ∈ ZF, that $m\vDash\sigma$, without knowing that m models ZF as a whole. This is because N 's grasp of what exactly is in ZF can be incorrect; if there are nonstandard integers, then there are also nonstandard (codes for) sentences, some of which will be in the "local copy" of ZF.
However, if "model" means "model of Σ" where Σ is an explicit finite list of axioms, all of which are in ZF (and with other nice properties as in the paper), then one can make the necessary leap. To model Σ is to model each σ in the explicit list; thus, if M does this, then N must know that m does this.