13 ms·

> That is not a definition of ⊨, that is a definition of logical implicature. Not the same thing. You should read that definition again. It's really hard to ha

> That is not a definition of ⊨, that is a definition of logical implicature. Not the same thing. You should read that definition again. It's really hard to have a discussion if we can't agree on standard notation. The double turnstyle symbol has multiple uses (sad as it is), and when there is a structure on the LHS it means something different than when there is a set of formulas on the LHS. The second sense is defined in 1.9.1 and is based on the first sense. > And our disagreement turns on this, at least in part, because one of the consequences of the incompleteness theorem is that there are models of PA (or RA or whatever your favorite axiomization of arithmetic happens to be) where G is true, and there are models where G is false. This is true. > any (first order) theory that includes arithmetic is incomplete. That is basically true, assuming that the theory is also sound (because we can construct unsound complete theories of arithmetic), and if by "arithmetic" we mean "addition and multiplication" (otherwise, see Presburger Arithmetic). Gödel's First Incompleteness theorem does give you a bit more than that though (at least in its strongest variants): it doesn't make any assumptions about the theory being sound (mainly because that's very hard to prove), it just needs the theory to be "strong enough" and to be consistent (i.e. not leading to a contradiction). So even if we were willing to accept some false statements we can't get a complete theory (technically, that's the Gödel-Rosser proof, Gödel's original proof had a slightly different condition). It also gives you a concrete example of a Gödel sentence that can be construed, which leads rather directly to the second theorem.

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

> 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...