3 ms·

> "Γ ⊨ φ" means that the string φ is true under some model of Γ. It means that φ is true in every model of Γ.[0] > If we have such a P in hand we can always c

> "Γ ⊨ φ" means that the string φ is true under some model of Γ. It means that φ is true in every model of Γ.[0] > If we have such a P in hand we can always check it, but if we don't have a P the question of whether or not one exists is generally an open one. > The surprise is that it turns out that with only a very small amount of structure we lose "Γ ⊨ φ → Γ ⊢ φ". That is not true for first-order logic. In first order logic Γ ⊨ φ → Γ ⊢ φ is always true. That's the completeness theorem.[1] This really only starts to become false when you go to e.g. second-order logic, but first-order logic is really the most commonly used type of logic and plenty sufficient for almost all of mathematics (though that becomes a philosophical debate to some extent). Gödel's theorem is really about first-order logic, and it says that even though completeness of FOL is a nice thing, it doesn't help us with the goal of finding an effective theory of the natural numbers (effective in the sense that proofs are mechanically verifiable). [0]: That's the standard definition, as it can be found e.g. in https://milneopentextbooks.org/download/friendly-intro-2e-update19-pdf/ https://milneopentextbooks.org/download/friendly-intro-2e-up... (Definition 1.9.1) or https://books.google.it/books?id=u0wlXPHATDcC&pg=PA67#v=onepage&q&f=false https://books.google.it/books?id=u0wlXPHATDcC&pg=PA67#v=onep... (Definition 3.4.4 (iv)) and many other textbooks on logic. [1]: See e.g. https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th... - and every introductory textbook about about mathematical logic, including the ones referenced above.

lisper 4y ago
> It means that φ is true in every model of Γ.[0] > (Definition 1.9.1) That is not a definition of ⊨, that is a definition of logical implicature. Not the same thing. The ⊨ symbol is defined in definition 1.7.4, and it is used in a different sense than we are using it here. The left-hand argument to the ⊨ operator in that book is a model (an "L-structure" using the book's terminology), not a theory. But Γ is a theory. So writing Γ ⊨ φ is fundamentally incompatible with the definition of ⊨ given in that book. 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. > That is not true for first-order logic. In first order logic Γ ⊨ φ → Γ ⊢ φ is always true. Only if you restrict what you mean by "first-order logic". Under some definition it is manifestly not true: any (first order) theory that includes arithmetic is incomplete. > first-order logic is really the most commonly used type of logic and plenty sufficient for almost all of mathematics Yes, and when you include arithmetic (or any of the other variants on that theme) it becomes incomplete.
- Tainnor 4y ago
  > 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.

lisper 4y ago

> It means that φ is true in every model of Γ.[0] > (Definition 1.9.1) That is not a definition of ⊨, that is a definition of logical implicature. Not the same thing. The ⊨ symbol is defined in definition 1.7.4, and it is used in a different sense than we are using it here. The left-hand argument to the ⊨ operator in that book is a model (an "L-structure" using the book's terminology), not a theory. But Γ is a theory. So writing Γ ⊨ φ is fundamentally incompatible with the definition of ⊨ given in that book. 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. > That is not true for first-order logic. In first order logic Γ ⊨ φ → Γ ⊢ φ is always true. Only if you restrict what you mean by "first-order logic". Under some definition it is manifestly not true: any (first order) theory that includes arithmetic is incomplete. > first-order logic is really the most commonly used type of logic and plenty sufficient for almost all of mathematics Yes, and when you include arithmetic (or any of the other variants on that theme) it becomes incomplete.

Tainnor 4y ago
> 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.