4 ms·

The continuum hypothesis is an example of a statement that is independent of ZFC. About futility of theorem proving: I think a useful perspective on this is th

The continuum hypothesis is an example of a statement that is independent of ZFC. About futility of theorem proving: I think a useful perspective on this is that the context of formal logic with respect to "all mathematics" used to really mean "all of mathematics in one system" a hundred years ago. This is the logicist program started by Frege and Russell - make everything formal - and this was shattered. Now nothing stops us from formalizing some part of mathematics. Today, when people say "you can formalize all mathematics" post Gödel, it means you pick your area and formalize away, knowing that effectively proving consistency of your formal system (within the same system) is out of reach. So nobody tries to claim "all in one system" but many logics and sets of axioms coexist without there being any distinguished one that is better (in the sense of effectively proved consistent and strong enough to be "useful").

bjornsing 6y ago
Sure. And you can safely extend ZFC with either CH or ~CH. But that makes it clearly different than a theorem. In my mind mathematics is essentially the set of all theorems. So I think we’re back were we started: All of mathematics can in principle be deduced from ZFC. There are a few border cases that can be useful, and can be included by extending ZFC.
- dwohnitmok 6y ago
  I think that this is a reasonable response and I think the responses in this thread exaggerate the consequences of Godel's Incompleteness Theorems. But you perhaps may find it interesting to consider what could be meant when someone says "there are true statements that are not provable" in a way that doesn't exaggerate the results of the Incompleteness Theorems. I don't actually support this line of thinking, but I find it interesting to engage with. So here goes: Whatever you might say about more abstract mathematical structures, there seems to be something indelibly real about the natural numbers. I can verify simple facts about them by physically counting things. While definitionally perhaps it might make sense to create a formal system that says 5 + 6 = 8, I can go and count apples and realize that nope actually 5 + 6 = 11. Now luckily statements of this form, that don't use any quantification (i.e. the words "for all," "there exists," or their equivalents such as "always," or "eventually"), are entirely decided by our usual axioms about the natural numbers. But it seems like, while perhaps a tad less concrete than statements such as 1 + 1 = 2, there are other statements involving quantification that still have some "one-sided" concrete aspect to them. For example if I claim there exists a natural number with some arithmetical property and there indeed is such a number, simply by physically counting up I will eventually come across such a number. However, if I'm wrong, then I will never know (this is what is meant by one-sided). Likewise if I claim a property is true of every natural number, I will eventually have experimental proof if I'm wrong, but I will never know for certain if I'm right (at least by physically counting things). Godel's Incompleteness Theorem says there will always be such quantified statements that any given formal system cannot decide. Yet they seem to have definite truth values in our physical universe! Either my physical act of counting will come to an end or it won't. This seems like a very real consequence. So sure you can claim that these statements are different than theorems because either themselves or their negation can be added to our pre-existing axioms about the natural numbers without any conflict and that might be true in theory, but we would like to preserve the property that our axioms about the natural numbers correctly reflect how natural numbers act in our universe, and it seems, at least at a first glance, that Godel's Incompleteness Theorem disallows that, or at the very least that the act of trying to find these axioms requires extra-mathematical justification.
dwohnitmok 6y ago
> Today, when people say "you can formalize all mathematics" post Gödel, it means you pick your area and formalize away, knowing that effectively proving consistency of your formal system (within the same system) is out of reach. This isn't what I mean when I say "formalize all mathematics" at least. For example the diversity among the current crop of proof assistants has nothing to do with incompleteness and everything instead to do with with proof writing ergonomics. Assuming we perfectly solved the problem of the ergonomics of writing formal proofs, ZFC would be enough to do the overwhelming majority of modern mathematics. > effectively proving consistency of your formal system (within the same system) This isn't the significance of the Second Incompleteness Theorem though. Since an inconsistent formal system can prove anything, why would you ever trust a proof of consistency within the same system? To avoid repetition, I'll just link to a previous comment I made: https://news.ycombinator.com/item?id=25118038 https://news.ycombinator.com/item?id=25118038 > many logics and sets of axioms coexist without there being any distinguished one that is better (Syntactic) completeness has never really been a criteria for creating an end-all-be-all formal system in and of itself. We happily use many different mutually incompatible geometric systems (Euclidean, hyperbolic, etc.), in spite of the fact that many are complete. That being said, it is true a pre-Godel desirable property of a foundational system of mathematics would be completeness, but foundations has never really been all that important for the working mathematician.
- burakemir 6y ago
  Let me try to reconstruct what has been said. You seem to be reacting to points different from the one I tried to make. bjornsing: All of mathematics can in principle be derived from ZFC. morelisp: not all, there are independent statements. Mathematics is beyond formalization. bjornsing: like what? are you saying that formalization is futile? or not? me: CH is an example. formalizing is not futile, but affected by incompleteness theorems in the sense that all those proof assistants, when used for developing some theory, will require something else to prove the consistency of that theory. dwohnitmok: the point of incompleteness is not that it requires a stronger system, but that a weaker system cannot prove a stronger system, killing the idea of trusted computing base. See, I was not trying to expound the significance of the Second Incompleteness Theorem; I do not really care what mathematicians consider as in or out of "all mathematics," but I noticed that "being able to formalize all mathematics" has become a somewhat technical expression in logic. I like very much what you're writing in that comment. I have also seen Gentzen's consistency argument for PA and think the qualification that you include at the end about weaker systems sometimes being able to show the consistency of stronger ones is needed. I did not imply that proving consistency of X within X is desirable. However, I am intrigued by Artemov using a provability operator to prove consistency of PA in PA: https://arxiv.org/abs/1902.07404 https://arxiv.org/abs/1902.07404 Provability logic is interesting, a modal logic that adds Loeb's theorem as axiom (maybe Carl Hewitt would consider it a foundation of computer science? but I digress.) Now, the reason I feel compelled to comment back: I do not understand why you bring up completeness. What are you reacting to? Are you trying to imply that using incomplete foundations is the key to ignore the challenge of proving consistency? Saying "ZFC is enough for all mathematics" is a commitment to ZFC axioms and to first-order logic. First order logic is compact and complete. As such, it is very much affected by the First Incompleteness Theorem and also the Second, and there will also be non-standard models and the Skolem paradox. I don't have a horse in the foundation and formalization race, just curious what you mean. As far as I can tell (and I may well be off, not a mathematician), it seems quite desirable that foundations worthy of the name would let us prove all theorems of arithmetic and natural numbers.

bjornsing 6y ago

Sure. And you can safely extend ZFC with either CH or ~CH. But that makes it clearly different than a theorem. In my mind mathematics is essentially the set of all theorems. So I think we’re back were we started: All of mathematics can in principle be deduced from ZFC. There are a few border cases that can be useful, and can be included by extending ZFC.

dwohnitmok 6y ago
I think that this is a reasonable response and I think the responses in this thread exaggerate the consequences of Godel's Incompleteness Theorems. But you perhaps may find it interesting to consider what could be meant when someone says "there are true statements that are not provable" in a way that doesn't exaggerate the results of the Incompleteness Theorems. I don't actually support this line of thinking, but I find it interesting to engage with. So here goes: Whatever you might say about more abstract mathematical structures, there seems to be something indelibly real about the natural numbers. I can verify simple facts about them by physically counting things. While definitionally perhaps it might make sense to create a formal system that says 5 + 6 = 8, I can go and count apples and realize that nope actually 5 + 6 = 11. Now luckily statements of this form, that don't use any quantification (i.e. the words "for all," "there exists," or their equivalents such as "always," or "eventually"), are entirely decided by our usual axioms about the natural numbers. But it seems like, while perhaps a tad less concrete than statements such as 1 + 1 = 2, there are other statements involving quantification that still have some "one-sided" concrete aspect to them. For example if I claim there exists a natural number with some arithmetical property and there indeed is such a number, simply by physically counting up I will eventually come across such a number. However, if I'm wrong, then I will never know (this is what is meant by one-sided). Likewise if I claim a property is true of every natural number, I will eventually have experimental proof if I'm wrong, but I will never know for certain if I'm right (at least by physically counting things). Godel's Incompleteness Theorem says there will always be such quantified statements that any given formal system cannot decide. Yet they seem to have definite truth values in our physical universe! Either my physical act of counting will come to an end or it won't. This seems like a very real consequence. So sure you can claim that these statements are different than theorems because either themselves or their negation can be added to our pre-existing axioms about the natural numbers without any conflict and that might be true in theory, but we would like to preserve the property that our axioms about the natural numbers correctly reflect how natural numbers act in our universe, and it seems, at least at a first glance, that Godel's Incompleteness Theorem disallows that, or at the very least that the act of trying to find these axioms requires extra-mathematical justification.

dwohnitmok 6y ago

> Today, when people say "you can formalize all mathematics" post Gödel, it means you pick your area and formalize away, knowing that effectively proving consistency of your formal system (within the same system) is out of reach. This isn't what I mean when I say "formalize all mathematics" at least. For example the diversity among the current crop of proof assistants has nothing to do with incompleteness and everything instead to do with with proof writing ergonomics. Assuming we perfectly solved the problem of the ergonomics of writing formal proofs, ZFC would be enough to do the overwhelming majority of modern mathematics. > effectively proving consistency of your formal system (within the same system) This isn't the significance of the Second Incompleteness Theorem though. Since an inconsistent formal system can prove anything, why would you ever trust a proof of consistency within the same system? To avoid repetition, I'll just link to a previous comment I made: https://news.ycombinator.com/item?id=25118038 https://news.ycombinator.com/item?id=25118038 > many logics and sets of axioms coexist without there being any distinguished one that is better (Syntactic) completeness has never really been a criteria for creating an end-all-be-all formal system in and of itself. We happily use many different mutually incompatible geometric systems (Euclidean, hyperbolic, etc.), in spite of the fact that many are complete. That being said, it is true a pre-Godel desirable property of a foundational system of mathematics would be completeness, but foundations has never really been all that important for the working mathematician.

burakemir 6y ago
Let me try to reconstruct what has been said. You seem to be reacting to points different from the one I tried to make. bjornsing: All of mathematics can in principle be derived from ZFC. morelisp: not all, there are independent statements. Mathematics is beyond formalization. bjornsing: like what? are you saying that formalization is futile? or not? me: CH is an example. formalizing is not futile, but affected by incompleteness theorems in the sense that all those proof assistants, when used for developing some theory, will require something else to prove the consistency of that theory. dwohnitmok: the point of incompleteness is not that it requires a stronger system, but that a weaker system cannot prove a stronger system, killing the idea of trusted computing base. See, I was not trying to expound the significance of the Second Incompleteness Theorem; I do not really care what mathematicians consider as in or out of "all mathematics," but I noticed that "being able to formalize all mathematics" has become a somewhat technical expression in logic. I like very much what you're writing in that comment. I have also seen Gentzen's consistency argument for PA and think the qualification that you include at the end about weaker systems sometimes being able to show the consistency of stronger ones is needed. I did not imply that proving consistency of X within X is desirable. However, I am intrigued by Artemov using a provability operator to prove consistency of PA in PA: https://arxiv.org/abs/1902.07404 https://arxiv.org/abs/1902.07404 Provability logic is interesting, a modal logic that adds Loeb's theorem as axiom (maybe Carl Hewitt would consider it a foundation of computer science? but I digress.) Now, the reason I feel compelled to comment back: I do not understand why you bring up completeness. What are you reacting to? Are you trying to imply that using incomplete foundations is the key to ignore the challenge of proving consistency? Saying "ZFC is enough for all mathematics" is a commitment to ZFC axioms and to first-order logic. First order logic is compact and complete. As such, it is very much affected by the First Incompleteness Theorem and also the Second, and there will also be non-standard models and the Skolem paradox. I don't have a horse in the foundation and formalization race, just curious what you mean. As far as I can tell (and I may well be off, not a mathematician), it seems quite desirable that foundations worthy of the name would let us prove all theorems of arithmetic and natural numbers.