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