4 ms·

>>His proof is fairly difficult to understand - it involves prime numbers, factorization, all this number theory. >Actually, the textbook proof itself is not v

>>His proof is fairly difficult to understand - it involves prime numbers, factorization, all this number theory. >Actually, the textbook proof itself is not very different from the presentation in this article, so not hard at all. The difficult part is in formalizing that you can write "a program that proves a program halts". To do so you have to encode it into the language of mathematics, and that is the painful part. I think the difficulty of understanding Gödel's proof has changed with the rise of computers. For him the difficult part of the proof was showing that you can represent text as numbers and manipulate it using arithmetic operations. These days we all do that for our day jobs. So you can skip over the part that Gödel thought was difficult in one line, and focus your attention on the clever use of self-reference. Also these days we would probably use a binary encoding instead of Gödel's encoding via prime factorisation, so even if you did want to explain the details of the encoding the amount of number theory would be reduced.

knome 5y ago
The prime factorization ensures that every combination of terms creates a unique value. How does binary do so?
- Strilanc 5y ago
  Typically either with length prefixing (what binary protocols do) or with escaping/quoting (what text protocols do). For example, JSON assigns a unique bit sequence to every possible list of strings by using '"' and ',' as separators and '\' as an escape signal to disable the special meaning of the next character.
woolion 5y ago
Gödel's method starting with encoding parentheses, and bound variables, i.e. purely syntactical artifacts. It's a good example where you could do away with this, using e.g. de Bruijn indices -- exactly as you'd suggest switching encoding to binary. It is another layer of (mostly incidental) complexity yet in the end this complexity has to be addressed -- one choice of base does not change the number. When you write programs, you don't prove them correct, and you go down to assembly instructions, which is essentially what Gödel did.
lacker 5y ago
For him the difficult part of the proof was showing that you can represent text as numbers and manipulate it using arithmetic operations. These days we all do that for our day jobs. Yes - this is a great way of putting it.

knome 5y ago

The prime factorization ensures that every combination of terms creates a unique value. How does binary do so?

Strilanc 5y ago
Typically either with length prefixing (what binary protocols do) or with escaping/quoting (what text protocols do). For example, JSON assigns a unique bit sequence to every possible list of strings by using '"' and ',' as separators and '\' as an escape signal to disable the special meaning of the next character.

woolion 5y ago

Gödel's method starting with encoding parentheses, and bound variables, i.e. purely syntactical artifacts. It's a good example where you could do away with this, using e.g. de Bruijn indices -- exactly as you'd suggest switching encoding to binary. It is another layer of (mostly incidental) complexity yet in the end this complexity has to be addressed -- one choice of base does not change the number. When you write programs, you don't prove them correct, and you go down to assembly instructions, which is essentially what Gödel did.

lacker 5y ago

For him the difficult part of the proof was showing that you can represent text as numbers and manipulate it using arithmetic operations. These days we all do that for our day jobs. Yes - this is a great way of putting it.