6 ms·

> nowadays Turing Machines are a dime a dozen, and the idea of a "program" is common place I think you may have misconstrued what I meant. From a metamathemati

by dvt 4y ago

> nowadays Turing Machines are a dime a dozen, and the idea of a "program" is common place I think you may have misconstrued what I meant. From a metamathematical standpoint, leveraging the Halting Problem gives you a lot of stuff for free. Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians. Specifically, Godel numbering really originally made this entire thing work. And that sausage was not very intuitively-made.

lisper 4y ago
> leveraging the Halting Problem gives you a lot of stuff for free. Not exactly for free. You still have to prove the non-computability of the halting problem. But I get your meaning. > Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians. Sure, but that is no different from any technological advance. Arabic numerals were a major breakthrough when they were first invented. Nowadays it is pretty safe to take them for granted in most cases. > Godel numbering really originally made this entire thing work. Sure, but that was only necessary because Godel didn't know about ASCII. Proving Godel's theorem using Godel numbers is kind of like writing a C compiler as a state table for a Turing Machine. You could do it, but no one in their right mind would except perhaps as an intellectual exercise. The history of how technological innovations came about is very different, and usually much more difficult, than the way one can re-invent those innovations with the benefit of hindsight.
- Tainnor 4y ago
  Gödel numbering is chosen because numbers are very easy to reason about and mathematicians like that things are provable from simple principles like arithmetic, and because for Gödel's theorem to actually work on theories of arithmetic the encodings of formulas have to be numbers. Of course, you can choose some other encoding scheme - one that is easier for humans to read, such as the binary encoding of a nicely formatted string - but that's not as directly amenable to a rigorous mathematical proof. In particular, you technically have to prove that that encoding scheme doesn't lead to ambiguities, i.e. every string has (at most) a unique parsing. That may seem (and is) obvious, but technically does require a proof, something you can avoid when you just use Gödel numbering via the fundamental theorem of arithmetic instead But Gödel numbering is not really the bread and butter of the proof. The more technically relevant part about Gödel's proofs that doesn't just readily follow from the halting problem is the fact that incompleteness of first-order theories has only very weak conditions - Robinson arithmetic is already sufficient. You have to prove that Robinson arithmetic is strong enough to express every primitive recursive function and that requires some mathematical tricks.
  - lisper 4y ago
    > because for Gödel's theorem to actually work on theories of arithmetic the encodings of formulas have to be numbers ASCII codes are numbers. > but that's not as directly amenable to a rigorous mathematical proof Why not? > you technically have to prove that that encoding scheme doesn't lead to ambiguities, ASCII is unambiguous. In fact, the only difference between ASCII and Godel numbers is that ASCII encodes strings as powers of 256 whereas Godel numbers encode strings as powers of prime numbers. > i.e. every string has (at most) a unique parsing Huh? That makes no sense. Did you mean that every number has a unique mapping to a string? Because ASCII certainly meets that requirement. > The more technically relevant part about Gödel's proofs that doesn't just readily follow from the halting problem is the fact that incompleteness of first-order theories has only very weak conditions - Robinson arithmetic is already sufficient. Why does that matter? This seems to me like an interesting bit of trivia about Robinson arithmetic, but I don't see why this matters to the main point. Any system less powerful than PA is trivially incomplete.
    - lmm 4y ago
      > Why does that matter? This seems to me like an interesting bit of trivia about Robinson arithmetic, but I don't see why this matters to the main point. Any system less powerful than PA is trivially incomplete. Isn't this backwards? Systems that are simple enough (e.g. Presburger arithmetic) are complete, which is what we'd expect.
      - lisper 4y ago
        I guess I should have been more precise: trivially incomplete with respect to truths about numbers, which is the thing we actually care about. It is trivial to construct a complete system that is completely (!) uninteresting. The empty system is complete with respect to its own theorems, of which there are none, but that is about as uninteresting as it gets. The interesting thing is that as soon as you get a system that is sufficiently expressive to capture even an elementary subset of what we would consider "truths about numbers" that system is necessarily incomplete, and it cannot be made complete by making it more powerful. That is the interesting thing, and proving it does not depend (AFAICT) on the details of any particular encoding of truths about numbers as long as it is well defined.

by dvt 4y ago

lisper 4y ago

> leveraging the Halting Problem gives you a lot of stuff for free. Not exactly for free. You still have to prove the non-computability of the halting problem. But I get your meaning. > Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians. Sure, but that is no different from any technological advance. Arabic numerals were a major breakthrough when they were first invented. Nowadays it is pretty safe to take them for granted in most cases. > Godel numbering really originally made this entire thing work. Sure, but that was only necessary because Godel didn't know about ASCII. Proving Godel's theorem using Godel numbers is kind of like writing a C compiler as a state table for a Turing Machine. You could do it, but no one in their right mind would except perhaps as an intellectual exercise. The history of how technological innovations came about is very different, and usually much more difficult, than the way one can re-invent those innovations with the benefit of hindsight.

Tainnor 4y ago
Gödel numbering is chosen because numbers are very easy to reason about and mathematicians like that things are provable from simple principles like arithmetic, and because for Gödel's theorem to actually work on theories of arithmetic the encodings of formulas have to be numbers. Of course, you can choose some other encoding scheme - one that is easier for humans to read, such as the binary encoding of a nicely formatted string - but that's not as directly amenable to a rigorous mathematical proof. In particular, you technically have to prove that that encoding scheme doesn't lead to ambiguities, i.e. every string has (at most) a unique parsing. That may seem (and is) obvious, but technically does require a proof, something you can avoid when you just use Gödel numbering via the fundamental theorem of arithmetic instead But Gödel numbering is not really the bread and butter of the proof. The more technically relevant part about Gödel's proofs that doesn't just readily follow from the halting problem is the fact that incompleteness of first-order theories has only very weak conditions - Robinson arithmetic is already sufficient. You have to prove that Robinson arithmetic is strong enough to express every primitive recursive function and that requires some mathematical tricks.
- lisper 4y ago
  > because for Gödel's theorem to actually work on theories of arithmetic the encodings of formulas have to be numbers ASCII codes are numbers. > but that's not as directly amenable to a rigorous mathematical proof Why not? > you technically have to prove that that encoding scheme doesn't lead to ambiguities, ASCII is unambiguous. In fact, the only difference between ASCII and Godel numbers is that ASCII encodes strings as powers of 256 whereas Godel numbers encode strings as powers of prime numbers. > i.e. every string has (at most) a unique parsing Huh? That makes no sense. Did you mean that every number has a unique mapping to a string? Because ASCII certainly meets that requirement. > The more technically relevant part about Gödel's proofs that doesn't just readily follow from the halting problem is the fact that incompleteness of first-order theories has only very weak conditions - Robinson arithmetic is already sufficient. Why does that matter? This seems to me like an interesting bit of trivia about Robinson arithmetic, but I don't see why this matters to the main point. Any system less powerful than PA is trivially incomplete.
  - lmm 4y ago
    > Why does that matter? This seems to me like an interesting bit of trivia about Robinson arithmetic, but I don't see why this matters to the main point. Any system less powerful than PA is trivially incomplete. Isn't this backwards? Systems that are simple enough (e.g. Presburger arithmetic) are complete, which is what we'd expect.
    - lisper 4y ago
      I guess I should have been more precise: trivially incomplete with respect to truths about numbers, which is the thing we actually care about. It is trivial to construct a complete system that is completely (!) uninteresting. The empty system is complete with respect to its own theorems, of which there are none, but that is about as uninteresting as it gets. The interesting thing is that as soon as you get a system that is sufficiently expressive to capture even an elementary subset of what we would consider "truths about numbers" that system is necessarily incomplete, and it cannot be made complete by making it more powerful. That is the interesting thing, and proving it does not depend (AFAICT) on the details of any particular encoding of truths about numbers as long as it is well defined.