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

Patrik Eklund peklund at
Mon Sep 12 01:45:18 EDT 2022

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

   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' |= 

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 



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.  
> It can be downloaded from .  
> Hopefully that's what Adriano wanted.
> Vaughan Pratt
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220912/71a9460a/attachment-0001.html>

More information about the FOM mailing list