The latest episode of Gödel Without Tears — on the Arithmetization of Syntax — is now available here.

2 thoughts on “Gödel Without Tears — 7”

a.c.

A curious feature of this, looked at today, is that when we decode n, as in the proof of theorem 28, and then ask whether the resulting expression is a term, what we would actually get, in a computer, is another encoding: a sequence of Unicode characters, perhaps.

So in a way we haven’t gotten anywhere — unless the difficulty in seeing that theorem 28 is true is a difficulty in seeing how it would work for the particular encoding Godel chose.

a.c.A curious feature of this, looked at today, is that when we decode n, as in the proof of theorem 28, and then ask whether the resulting expression is a term, what we would actually get, in a computer, is another encoding: a sequence of Unicode characters, perhaps.

So in a way we haven’t gotten anywhere — unless the difficulty in seeing that theorem 28 is true is a difficulty in seeing how it would work for the particular encoding Godel chose.

Peter SmithI’m not sure I’m grasping the point being made: is it being said that the quick-and-dirty reasoning for Theorem 28 is TOO quick and dirty?