in Jech's paper: On Gödel's Second Incompleteness Theorem


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


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.


One place in the proof where Jech uses the finiteness of $S$ is the point where he passes from "$M \vDash \sigma$ if and only if $N \vDash (m \vDash \sigma)$" to $N \vDash (m$ is a model$)$". To make this inference, you just list all the sentences $\sigma_1, \ldots, \sigma_n$ in $S$, and since $N\vDash (m\vDash \sigma_i)$ for every $i$, we have $$N\vDash [(m\vDash \sigma_1) \wedge (m \vDash \sigma_2) \wedge \cdots \wedge (m \vDash \sigma_n)],$$ which is what we want. If you had an infinite number of $\sigma_i$ then you could not do this because sentences in first-order languages have to be finite in length.

As for your second question, I think that there is some vagueness in your hypothesis "if one actually builds a model of set theory." If I interpret this to mean, "if we are explicitly given a proof in ZF of `there is a model of ZF'" then yes, given such a proof, we can algorithmically convert it into a ZF proof of 0=1. Without looking at Jech's proof more carefully I'm not sure if it is "finitistic" enough to yield such an algorithm, but certainly there are other proofs of Goedel's second theorem that show you how to do this.


I think reading:


is going to help you.

Jech's proof is rewritten a bit more explicitly (see section "III. SHORT PROOFS"), and then used in the next section to prove Gödel's second incompleteness theorem for weaker theories than ZF.


OK, if there's a model M of ZF which can be embedded in another model N via m, we cannot conclude that N thinks m is a model.

However, it seems to me the same proof can be carried without it, only using the following reverse implication for the infinite set of axioms ZF:

(*) if N is a model of ZF and m is any inside model of ZF, it can be lifted to an 'outside' model M, which moreover satisfies A iff N thinks m does

A is the diagonal sentence, saying there's a model which does not satisfy A

Now we can prove: (1) if ZF is consistent, then A.

Proof: by the completeness Theorem ZF has a model M. if M is negative we're done. otherwise M has a negative sub-model which can be lifted by (*) to a negative model in the 'real world'. so again A is true.

(2) ( the inside version of (1) - for any theorem we can prove it has a valid proof - just write it down explicitly) ZF proves that : if ZF is consistent, then A.

Now, if ZF is consistent, and it proves its consistency, then using modus ponens on (1) and 'inside' modus ponens of (2) we get: (1') A (2') ZF proves A. (Thus, any model satisfies A)

which is a contradiction: A is true iff there's a model that does not satisfy A.

Am I still missing something?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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