show/hide this revision's text 2 Punctuation, unicode

proof Proof of goedel Gödel incompleteness

in Jech's paper: On Goedel's 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'world’, and using some diagonal sentence G for a contradiction.

My question:

Why does passing to a finite subset needed for the proof?

another

Another question: If once actually builds a model of set theory, the above theorem proves that ZF is incosistentinconsistent. 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

show/hide this revision's text 1

proof of goedel incompleteness

in Jech's paper: On Goedel'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 incosistent. 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