# Re: Jech's proof of Gödel's second incompleteness theorem

Patrik Eklund peklund at cs.umu.se
Mon Sep 12 01:45:18 EDT 2022

```I  look at formula (1) in Jech's proof of Gödel's 2nd incompleteness
theorem

M |= sigma if and only if N |= (M' |= sigma)

Clearly, M and N are syntactically built by the same rules, so M and N
are of the "same type", however we define 'type' in this context. But
the type possessed by "sigma" is NOT the type possessed by "M' |=
sigma"! That is, syntactically speaking.

Yet, the relation |= is  applied to both "M |= sigma" and "N |= (M' |=
sigma)".

Or in other words, the first "|=" in "N |= (M' |= sigma)" is NOT the
same as the second one.

Am I wrong or am I wrong?

In the history of FOM, types were not treated. Church tried a bit on
simple types with his o and iota. Later type theory does not fix this.

So basically this is something that has been ignored over the last
century.

Best,

Patrik

On 2022-09-11 19:54, Vaughan Pratt wrote:

> In response to Adriano Palma's request, Thomas Jech submitted his proof
> of Gödel's second incompleteness theorem to arXiv on April 15, 1992.