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

[Patrik Eklund]

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