4 ms·

> You mean Γ ⊢ φ or Γ ⊢ ¬φ . In principle no, though it's possible that it's defined like that in certain places, since in first-order logic, that amounts to t

> You mean Γ ⊢ φ or Γ ⊢ ¬φ . In principle no, though it's possible that it's defined like that in certain places, since in first-order logic, that amounts to the same thing (given the completeness theorem). But "completeness" is a notion from model theory that doesn't care about proof systems. In a system where the completeness theorem is not true, such as second-order logic with standard semantics, we do have complete theories (such as second-order PA), where we always have Γ ⊨ φ or Γ ⊨ ¬φ, but that doesn't mean that every statement is either provable or disprovable. > The proof of Godel's theorem is to exhibit a φ for which "Γ ⊢ φ or Γ ⊢ ¬φ" is false. From that you conclude that "Γ ⊨ φ → Γ ⊢ φ" is false on the assumption that "Γ ⊨ φ" is true. But that last part is an informal argument. We believe that "Γ ⊨ G" is true for the Godel sentence G but we (obviously) can't prove it. I think that has it a bit backwards. It's not that we believe that PA ⊨ G - in fact, if we believed that, it would immediately imply PA ⊢ G, when that's exactly what we showed to be impossible. It's that we believe that G is true in the natural numbers, which is not the same thing as being true in PA, and that belief rests in our belief that PA is sound (which we can't prove, but seems reasonable). (There are some different "flavours" of the incompleteness theorems, some of them rely on soundness of PA and others only on it being consistent.) > But note that what you said is not mutually exclusive with what /u/Tainnor said, i.e. That's because that's me. ;)

lisper 4y ago
> That's because that's me. ;) Oh, sorry, I thought I was responding to the parent comment by /u/dvt Let's go back to basics. To begin with, let's make sure we're on the same page with regards to notation. "Γ ⊢ φ" means that the string φ is a theorem under Γ. This is a syntactic property of Γ. The claim that some sequence of strings P is a valid proof of φ (and that therefore Γ ⊢ φ is indeed true) can be verified mechanically. "Γ ⊨ φ" means that the string φ is true under some model of Γ. This is a semantic property of Γ and it cannot be checked mechanically. We want "Γ ⊨ φ → Γ ⊢ φ" to be true, that is, we would like it to be the case that for every statement φ that is true under some model of Γ, we can mechanically prove that φ is a theorem of Γ, i.e. we can show that there exists a P which is a proof of φ. 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. But we actually want more than that. We also want Γ to be "interesting" in some sense. There is no sport in coming up with uninteresting systems for which "Γ ⊨ φ → Γ ⊢ φ" is true. The obvious example is the empty system and a corresponding empty model where every φ is both false and not a theorem. So we impose some minimal structure on Γ, not because the rules of formal systems demand it, but because systems where, say, P and ¬P are both false are not very interesting. So we demand that e.g. there exist at least one true statement and at least one false statement in our model, not because there is any cosmic rule that requires this, but simply because the whole enterprise becomes a pointless exercise in navel-gazing if we don't. That raises the natural question: what is the minimal amount of structure we can impose on Γ to make it "interesting" and worthy of study. And there are many answers to this, because there are many possible things that are potentially "interesting". Propositional logic. Set theory. Yada yada yada. The surprise is that it turns out that with only a very small amount of structure we lose "Γ ⊨ φ → Γ ⊢ φ". As with the imposition of structure in general in order to make systems interesting and worthy of study, there are many different ways in which to impose enough structure to lose this desirable property. One way, the way which historically was the first to be discovered, is to impose enough structure that the system can be modeled by the natural numbers. But this is not the only way. Another way is to impose enough structure that the system can be modeled by a simple machine consisting of a tape and a lookup table. Yet another way is to impose a structure that the system can be modeled by two urns that contain stones, and the ability to add and remove stones from the urns, and look in an urn to see if it is empty or not. There are many many variations on the theme. All of these things turn out to be in some sense "equivalent", and because of that the details of the structure that we impose on the system are uninteresting. It doesn't matter if we use numbers or tapes or stones, there is a certain point beyond which we lose "Γ ⊨ φ → Γ ⊢ φ". And the big surprise is that the threshold is very, very low. It takes very little structure to cross the threshold. There are systems for which "Γ ⊨ φ → Γ ⊢ φ" does hold, but those are necessarily of very limited utility. The proof of the falseness of "Γ ⊨ φ → Γ ⊢ φ" for any given system depends on the details of the system, but the general procedure is always the same: you produce a mapping from proofs to elements of the model. You then use that mapping to produce an element of the model (called G) which is true under the model if and only if there does not exist an element of the model corresponding to a proof of G under your mapping. The key is the mapping from proofs to elements of the model, and Godel numbers were the first such map, but they are not the only such map, and there is nothing particularly special about them other than that they were the first to be discovered. They might have some advantages if you are actually writing out a detailed formal proof of Godel's theorem by hand, just as buggy whips can be useful if you are driving a horse and buggy. But there aren't many compelling reasons to do either one in today's world except as an exercise in nostalgia.
- Tainnor 4y ago
  > "Γ ⊨ φ" 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.

lisper 4y ago

> That's because that's me. ;) Oh, sorry, I thought I was responding to the parent comment by /u/dvt Let's go back to basics. To begin with, let's make sure we're on the same page with regards to notation. "Γ ⊢ φ" means that the string φ is a theorem under Γ. This is a syntactic property of Γ. The claim that some sequence of strings P is a valid proof of φ (and that therefore Γ ⊢ φ is indeed true) can be verified mechanically. "Γ ⊨ φ" means that the string φ is true under some model of Γ. This is a semantic property of Γ and it cannot be checked mechanically. We want "Γ ⊨ φ → Γ ⊢ φ" to be true, that is, we would like it to be the case that for every statement φ that is true under some model of Γ, we can mechanically prove that φ is a theorem of Γ, i.e. we can show that there exists a P which is a proof of φ. 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. But we actually want more than that. We also want Γ to be "interesting" in some sense. There is no sport in coming up with uninteresting systems for which "Γ ⊨ φ → Γ ⊢ φ" is true. The obvious example is the empty system and a corresponding empty model where every φ is both false and not a theorem. So we impose some minimal structure on Γ, not because the rules of formal systems demand it, but because systems where, say, P and ¬P are both false are not very interesting. So we demand that e.g. there exist at least one true statement and at least one false statement in our model, not because there is any cosmic rule that requires this, but simply because the whole enterprise becomes a pointless exercise in navel-gazing if we don't. That raises the natural question: what is the minimal amount of structure we can impose on Γ to make it "interesting" and worthy of study. And there are many answers to this, because there are many possible things that are potentially "interesting". Propositional logic. Set theory. Yada yada yada. The surprise is that it turns out that with only a very small amount of structure we lose "Γ ⊨ φ → Γ ⊢ φ". As with the imposition of structure in general in order to make systems interesting and worthy of study, there are many different ways in which to impose enough structure to lose this desirable property. One way, the way which historically was the first to be discovered, is to impose enough structure that the system can be modeled by the natural numbers. But this is not the only way. Another way is to impose enough structure that the system can be modeled by a simple machine consisting of a tape and a lookup table. Yet another way is to impose a structure that the system can be modeled by two urns that contain stones, and the ability to add and remove stones from the urns, and look in an urn to see if it is empty or not. There are many many variations on the theme. All of these things turn out to be in some sense "equivalent", and because of that the details of the structure that we impose on the system are uninteresting. It doesn't matter if we use numbers or tapes or stones, there is a certain point beyond which we lose "Γ ⊨ φ → Γ ⊢ φ". And the big surprise is that the threshold is very, very low. It takes very little structure to cross the threshold. There are systems for which "Γ ⊨ φ → Γ ⊢ φ" does hold, but those are necessarily of very limited utility. The proof of the falseness of "Γ ⊨ φ → Γ ⊢ φ" for any given system depends on the details of the system, but the general procedure is always the same: you produce a mapping from proofs to elements of the model. You then use that mapping to produce an element of the model (called G) which is true under the model if and only if there does not exist an element of the model corresponding to a proof of G under your mapping. The key is the mapping from proofs to elements of the model, and Godel numbers were the first such map, but they are not the only such map, and there is nothing particularly special about them other than that they were the first to be discovered. They might have some advantages if you are actually writing out a detailed formal proof of Godel's theorem by hand, just as buggy whips can be useful if you are driving a horse and buggy. But there aren't many compelling reasons to do either one in today's world except as an exercise in nostalgia.

Tainnor 4y ago
> "Γ ⊨ φ" 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.