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 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.
I’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?