Timeline for SAT problem in Gödel numbering
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 31, 2017 at 8:52 | comment | added | Andrej Bauer | I think it's about propaganda, namely that mathematicians (and more specifically logicians) laid the ground for the digital era. Gödel had the idea that data which has nothing to do with arithmetic can be represented with numbers. Then Turing took one step closer by thinking of more concrete representations of such "numbers". And of course they also asked the question "what is computable?" | |
| May 31, 2017 at 1:01 | comment | added | Robert Israel | OK, so the question is whether an encoding qualifies as "Gödel" if it uses bit sequences. I personally wouldn't use that adjective, but I won't argue the point. | |
| May 30, 2017 at 18:19 | comment | added | Andrej Bauer | My remark is much more trivial than than that. All computers use all Gödel numberings for the simple reason that they use sequences of bits, which are just numbers in binary. | |
| May 30, 2017 at 16:27 | comment | added | Robert Israel | By "this way" I meant "using Gödel numbers". Proof assistants use much more efficient representations of mathematical structures. | |
| May 30, 2017 at 6:00 | comment | added | Andrej Bauer | Actually, all proof assistants do this all the time, and even youtube videos are just numbers, and so is music, and what you're reading on the the screen at the moment. It's just that the basic operations aren't $+$ and $\times$ but $NAND$. | |
| May 29, 2017 at 20:20 | history | answered | Robert Israel | CC BY-SA 3.0 |