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.
> 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>
More information about the FOM
mailing list