4 ms·

> The double turnstyle symbol has multiple uses Ah. TIL. > This is true. OK, it's good that we agree on that, but it doesn't really matter. What matters is

by lisper 4y ago

> The double turnstyle symbol has multiple uses Ah. TIL. > This is true. OK, it's good that we agree on that, but it doesn't really matter. What matters is whether or not the english statement "G cannot be proven" (or some variation on that theme) is true or false. More to the point, what matters is what it takes to persuade a human being that it is true or false. The double-turnstyle symbol may be useful, but it is not the main event. > That is basically true, assuming that the theory is also sound OK, so we are basically in agreement on the things that actually matter. (Ironically, AFAICT Leary & Kristiansen don't actually define the term "sound". But again, whatever. It doesn't really matter for the substance of the point I am trying to make.) The point I am trying to make is this: the reason Godel's theorem matters is that it is a negative result on the quest to reduce all of mathematics to a mechanical process. Implicit in this goal is that the process yield results that are in some sense "reasonable", i.e. if a putative mechanical process for doing math ever yields the result that 2+2=5 then we can be pretty sure that something has gone wrong even without knowing anything about double-turnstyles or soundness or validity or consistency or any of the other myriad things that logicians concern themselves with. These are all just ways of battening down various hatches, but none of them actually matter. What matters, the reason Godel's theorem is a thing, is that it is what informs us that it is impossible to mechanize all of mathematics, and that attempting to do so is a fool's errand. Finding the weakest possible conditions under which this result holds is of secondary importance, of interest only to logicians. If you can add 1 and check for equality -- or any of a myriad other combinations of trivial operations that allow you to enumerate proofs -- you've lost. That is what matters. And that can be proven without Godel numbers.

Tainnor 4y ago
"Soundness" is a term that AFAIK comes from philosophy. An argument is correct if it follows logically from the premises, a sound argument is one in which the premises are also "true". In the context of theories, theories are sound if they are not merely consistent but also "true", i.e. correct with respect to reality. You quickly see that this gets us into murky territory where you have to argue, outside of logic itself, whether or not certain things are "true". That's why soundness is not necessarily talked about much in an introductory mathematical logic text such as L&K. The reason why this matters in the context of Gödel's theorems, though, besides a purely philosophical point of view, is that "PA is sound" can not be expressed in the language of arithmetic, but "PA is consistent" can be expressed in that language, and therefore Gödel's first theorem itself can be expressed in arithmetic. That is the key that establishes the link between the first and the second incompleteness theorem, the latter of which expresses that a theory of sufficient strength can't prove itself consistent.[0] A naïve proof via Turing Machines, to my understanding, gives you something equivalent to Godel's theorem provided PA is sound, but not just simply provided PA is consistent. Otherwise, I agree with your conclusions about the meaning of Gödel's theorems,[1] and I even agree that knowing all the technical conditions under which they apply shouldn't be of importance to non-logicians. I don't object to teaching CS students a version of Gödel's first incompleteness theorem via Turing Machines or even to some hand-waving where necessary. But that's not the same thing as claiming that Turing Machines make the original proof ideas obsolete. > And that can be proven without Godel numbers. I've said it before but Gödel numbers are a trivial technical detail. What matters is that an encoding scheme exists, not which one it is. You can take Gödel's original proof and just replace Gödel numbering with your favourite encoding scheme and nothing substantial about the proof structure will change (except that you will want to substitute the "factoring primes" routine with a corresponding decoding routine for your preferred scheme).[2] It just so happens that mathematicians actually like Gödel numbering because primes are very simple objects and every maths major learns about unique factorisation and the infinity of primes very early on. If as a computer scientist, you disagree, no big deal: just substitute your favourite encoding scheme. That's an entirely different discussion though as the one whether you want to prove Gödel's theorems via Turing machines or via purely logical means and the theory of primitive recursion. [0]: That, by itself, is not terribly interesting - if the theory was inconsistent, its own consistency proof wouldn't matter (since an inconsistent theory proves everything). The reason it becomes interesting is because that also implies that a theory can't be proven consistent by a weaker theory either (since every proof in the weaker theory is a proof in the original theory). This is what essentially kills the Hilbert program: We can't, say, agree that PA is sound and consistent (which seems easy enough to believe) and use that in order to prove ZFC consistent, or some such. [1]: Although I'm not sure they're necessarily "practically" relevant. Had it turned out that model checking of PA is "only" NP-complete, instead of uncomputable, it wouldn't practically have made it much better. [2]: This is, for example, briefly discussed in section 19.2 of this textbook about Gödel's theorems, which I highly recommend to anyone who does care about the technical details: https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf https://www.logicmatters.net/resources/pdfs/godelbook/GodelB...
- lisper 4y ago
  > I've said it before but Gödel numbers are a trivial technical detail. Actually, you seemed to be saying the exact opposite before when you wrote: > Your point about ASCII codes ignores that we don't just want individual symbols to be numbers, we want entire formulas to be numbers too. And at this point I'm still not sure if you really understand this or not because: > you will want to substitute the "factoring primes" routine with a corresponding decoding routine for your preferred scheme Well, yeah, obviously, but translating between strings of symbols and numbers is trivial when your alphabet is ASCII (or LATIN1 or UTF8 or whatever). You don't need to factor, all you need to do is divide/modulo by powers of 2. This is just obvious to anyone who has even the most elementary knowledge of modern computers. > A naïve proof via Turing Machines, to my understanding, gives you something equivalent to Godel's theorem provided PA is sound, but not just simply provided PA is consistent. No, it is vastly simpler than that. All you need is a computable mapping between programs and numbers. Once you have that, any claim about a program can be translated into a claim about a number (and vice versa). "P is a program that halts when run on input I" has a corresponding "N is a number that describes a program that halts when run on input I". From that, Godel's theorem is an elementary proof by reductio: if arithmetic were decidable, you could solve the halting problem by translating the question of whether or not a program P halts into the question of whether a number N describes a program that halts. Note that you essentially get soundness "for free" because the halting theorem is not grounded in axioms, it is grounded in physics. We don't have to wonder if our models of Turing Machines are "true". We can simply build a TM and observe that it behaves according to the model. And so the details of your axiomatization of math don't matter at all. Whatever axiomatization you can come up with, as long as you can use it to do arithmetic, and as long as someone can write a proof-checker for it, then Godel's theorem pops out as an elementary result. > mathematicians actually like Gödel numbering because primes are very simple objects Yes, I get that. But Turing machines are pretty simple too. The thing that makes TMs better than primes is that we can actually build a physical artifact whose behavior corresponds to the mathematical model of a TM. You can't do the same thing for primes because primes are not models of physical systems.
  - Tainnor 4y ago
    I really don't wish to belabour the primes vs. ASCII discussion because: it really is but a trivial implementation detail. You want to have a bijection between formulas and the natural numbers (such that certain operations on formulas, such as composition and extraction of subformulas can be computed). Primes do that, as do ASCII sequences. > From that, Godel's theorem is an elementary proof by reductio: if arithmetic were decidable, you could solve the halting problem by translating the question of whether or not a program P halts into the question of whether a number N describes a program that halts. I think you again misunderstand the full implications of Gödel's first theorem. Gödel's first theorem: > Any theory of arithmetic that is sufficiently strong and consistent is incomplete. What you have just proven is a corollary of that theorem, but actually a weaker result: > Arithmetic truth is not decidable Gödel's theorem works even if PA is not sound, but merely consistent. And it also works for potential other, unsound theories of arithmetic, as long as they're strong enough and consistent. Your proof via Turing machines does not: if PA is unsound, and if from PA you derive that the "impossible" program halts (or does not halt), it doesn't tell you anything, because the conclusions of PA can't be trusted. Therefore you can't derive the necessary contradiction. Again, this matters not only philosophically, but also technically because "If PA is sound, it is incomplete* can't be written as a statement of arithmetic, but "If PA is consistent, it is incomplete" can, and this is the necessary link between the first and the second theorem. --- I think there's a consistent thread in your comments where you think things are "obvious" and "true" because we can observe them somehow physically (e.g. your assertion that the Halting Problem is "not grounded in axioms, but in physics" - to which I would again object, but let's not go into that), but this is not how mathematics (and logic) work. It's fine if you don't care about it personally, but Gödel's theorems have deep mathematical and philosophical implications about systems of reasoning which are not dependent on our physical world. But I don't think this discussion will go anywhere.

by lisper 4y ago

Tainnor 4y ago

"Soundness" is a term that AFAIK comes from philosophy. An argument is correct if it follows logically from the premises, a sound argument is one in which the premises are also "true". In the context of theories, theories are sound if they are not merely consistent but also "true", i.e. correct with respect to reality. You quickly see that this gets us into murky territory where you have to argue, outside of logic itself, whether or not certain things are "true". That's why soundness is not necessarily talked about much in an introductory mathematical logic text such as L&K. The reason why this matters in the context of Gödel's theorems, though, besides a purely philosophical point of view, is that "PA is sound" can not be expressed in the language of arithmetic, but "PA is consistent" can be expressed in that language, and therefore Gödel's first theorem itself can be expressed in arithmetic. That is the key that establishes the link between the first and the second incompleteness theorem, the latter of which expresses that a theory of sufficient strength can't prove itself consistent.[0] A naïve proof via Turing Machines, to my understanding, gives you something equivalent to Godel's theorem provided PA is sound, but not just simply provided PA is consistent. Otherwise, I agree with your conclusions about the meaning of Gödel's theorems,[1] and I even agree that knowing all the technical conditions under which they apply shouldn't be of importance to non-logicians. I don't object to teaching CS students a version of Gödel's first incompleteness theorem via Turing Machines or even to some hand-waving where necessary. But that's not the same thing as claiming that Turing Machines make the original proof ideas obsolete. > And that can be proven without Godel numbers. I've said it before but Gödel numbers are a trivial technical detail. What matters is that an encoding scheme exists, not which one it is. You can take Gödel's original proof and just replace Gödel numbering with your favourite encoding scheme and nothing substantial about the proof structure will change (except that you will want to substitute the "factoring primes" routine with a corresponding decoding routine for your preferred scheme).[2] It just so happens that mathematicians actually like Gödel numbering because primes are very simple objects and every maths major learns about unique factorisation and the infinity of primes very early on. If as a computer scientist, you disagree, no big deal: just substitute your favourite encoding scheme. That's an entirely different discussion though as the one whether you want to prove Gödel's theorems via Turing machines or via purely logical means and the theory of primitive recursion. [0]: That, by itself, is not terribly interesting - if the theory was inconsistent, its own consistency proof wouldn't matter (since an inconsistent theory proves everything). The reason it becomes interesting is because that also implies that a theory can't be proven consistent by a weaker theory either (since every proof in the weaker theory is a proof in the original theory). This is what essentially kills the Hilbert program: We can't, say, agree that PA is sound and consistent (which seems easy enough to believe) and use that in order to prove ZFC consistent, or some such. [1]: Although I'm not sure they're necessarily "practically" relevant. Had it turned out that model checking of PA is "only" NP-complete, instead of uncomputable, it wouldn't practically have made it much better. [2]: This is, for example, briefly discussed in section 19.2 of this textbook about Gödel's theorems, which I highly recommend to anyone who does care about the technical details: https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf https://www.logicmatters.net/resources/pdfs/godelbook/GodelB...

lisper 4y ago
> I've said it before but Gödel numbers are a trivial technical detail. Actually, you seemed to be saying the exact opposite before when you wrote: > Your point about ASCII codes ignores that we don't just want individual symbols to be numbers, we want entire formulas to be numbers too. And at this point I'm still not sure if you really understand this or not because: > you will want to substitute the "factoring primes" routine with a corresponding decoding routine for your preferred scheme Well, yeah, obviously, but translating between strings of symbols and numbers is trivial when your alphabet is ASCII (or LATIN1 or UTF8 or whatever). You don't need to factor, all you need to do is divide/modulo by powers of 2. This is just obvious to anyone who has even the most elementary knowledge of modern computers. > A naïve proof via Turing Machines, to my understanding, gives you something equivalent to Godel's theorem provided PA is sound, but not just simply provided PA is consistent. No, it is vastly simpler than that. All you need is a computable mapping between programs and numbers. Once you have that, any claim about a program can be translated into a claim about a number (and vice versa). "P is a program that halts when run on input I" has a corresponding "N is a number that describes a program that halts when run on input I". From that, Godel's theorem is an elementary proof by reductio: if arithmetic were decidable, you could solve the halting problem by translating the question of whether or not a program P halts into the question of whether a number N describes a program that halts. Note that you essentially get soundness "for free" because the halting theorem is not grounded in axioms, it is grounded in physics. We don't have to wonder if our models of Turing Machines are "true". We can simply build a TM and observe that it behaves according to the model. And so the details of your axiomatization of math don't matter at all. Whatever axiomatization you can come up with, as long as you can use it to do arithmetic, and as long as someone can write a proof-checker for it, then Godel's theorem pops out as an elementary result. > mathematicians actually like Gödel numbering because primes are very simple objects Yes, I get that. But Turing machines are pretty simple too. The thing that makes TMs better than primes is that we can actually build a physical artifact whose behavior corresponds to the mathematical model of a TM. You can't do the same thing for primes because primes are not models of physical systems.
- Tainnor 4y ago
  I really don't wish to belabour the primes vs. ASCII discussion because: it really is but a trivial implementation detail. You want to have a bijection between formulas and the natural numbers (such that certain operations on formulas, such as composition and extraction of subformulas can be computed). Primes do that, as do ASCII sequences. > From that, Godel's theorem is an elementary proof by reductio: if arithmetic were decidable, you could solve the halting problem by translating the question of whether or not a program P halts into the question of whether a number N describes a program that halts. I think you again misunderstand the full implications of Gödel's first theorem. Gödel's first theorem: > Any theory of arithmetic that is sufficiently strong and consistent is incomplete. What you have just proven is a corollary of that theorem, but actually a weaker result: > Arithmetic truth is not decidable Gödel's theorem works even if PA is not sound, but merely consistent. And it also works for potential other, unsound theories of arithmetic, as long as they're strong enough and consistent. Your proof via Turing machines does not: if PA is unsound, and if from PA you derive that the "impossible" program halts (or does not halt), it doesn't tell you anything, because the conclusions of PA can't be trusted. Therefore you can't derive the necessary contradiction. Again, this matters not only philosophically, but also technically because "If PA is sound, it is incomplete* can't be written as a statement of arithmetic, but "If PA is consistent, it is incomplete" can, and this is the necessary link between the first and the second theorem. --- I think there's a consistent thread in your comments where you think things are "obvious" and "true" because we can observe them somehow physically (e.g. your assertion that the Halting Problem is "not grounded in axioms, but in physics" - to which I would again object, but let's not go into that), but this is not how mathematics (and logic) work. It's fine if you don't care about it personally, but Gödel's theorems have deep mathematical and philosophical implications about systems of reasoning which are not dependent on our physical world. But I don't think this discussion will go anywhere.