3 ms·

Interesting. Can you give an example of a statement that is independent of ZFC yet useful/often-used? I struggle to make any sense of this claim though... What

Interesting. Can you give an example of a statement that is independent of ZFC yet useful/often-used? I struggle to make any sense of this claim though... What is a proof if not an explanation of how a statement can be deduced from other statements (which in turn... all the way back to axioms)? And are you saying formal proof assistants like coq and isabelle are fools errands, in the sense that mathematics is in principal beyond formalization? If not, then why not?

sn41 6y ago
The consistency of ZFC cannot be proven in ZFC - this follows from the second incompleteness theorem. The consistency of ZFC is a very useful theorem. There are also very easy to understand number-theoretic and combinatorial results, like the Paris-Harrington Theorem [1] and Goodstein's Theorem [2] which are provably independent of Peano Arithmetic. The latter has an interpretation as a "hydra" game: there is a rooted tree (hydra), and you can cut off a number of heads in one shot. The hydra grows back a finite number of heads according to a specified rule. The question is, is there a strategy to slay the hydra? The surprising answer is that any strategy will work(!), but you cannot prove this fact inside Peano arithmetic. [1] https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor... [2] https://en.wikipedia.org/wiki/Goodstein%27s_theorem https://en.wikipedia.org/wiki/Goodstein%27s_theorem
- dwohnitmok 6y ago
  > The consistency of ZFC cannot be proven in ZFC - this follows from the second incompleteness theorem. The consistency of ZFC is a very useful theorem. Perhaps less useful than one might think. Given that an inconsistent system can prove anything, if you weren't convinced of ZFC's consistency to begin with I hardly think you'd be convinced by a proof of its consistency in itself. Godel's Second Incompleteness Theorem is important "in the other direction," that is its consequence for systems bigger than ZFC (or indeed PA)/larger statements that imply the consistency of your formal system in question. (A previous comment I made on this in greater detail https://news.ycombinator.com/item?id=25118038 https://news.ycombinator.com/item?id=25118038)
- oh_sigh 6y ago
  The answer is surprising only if you believe the specified rule can be any rule. But really, the specified rule may have enough complexity in it that makes it difficult to intuitively reason about the problem at all, at which point it isn't really a counter-intuitive result, merely a counter-intuitive rule.
dwohnitmok 6y ago
I feel like some weird hawk that swoops in for a lot of these Godel comments. No Godel's incompleteness theorems prove nothing about truth by themselves. They are only statements about proofs and can be independently paired with other statements (as well as their negation), both philosophical and mathematical, about truth. That is the incompleteness theorems are silent on the matter of truth as a direct consequence, but require other theorems or philosophies to further mold statements on truth (the incompleteness theorems do have important indirect impact on those statements). For example there is Godel's Completeness Theorem , which in a vague sense proves that "all true things are provable" (I can explain in greater detail if so desired). Godel's Completeness Theorem holds independently of Godel's Incompleteness Theorems (that is all four possible pairings of holding/not holding can apply to different formal systems). Notably Godel's Completeness Theorem holds for first order logic, the most common formalization of mathematical foundations (which includes ZFC and Peano Arithmetic). > Can you give an example of a statement that is independent of ZFC yet useful/often-used? Very briefly, the proof of Fermat's Last Theorem used an axiom that is independent of ZFC (it used a large cardinal axiom). It was later found that the proof did not require this axiom and could be fully formalized within ZFC. There are separately simple-sounding and useful-sounding, but not actually used, statements which are independent of ZFC (such as if the set X is smaller than the set Y by cardinality then X has fewer subsets than Y). But almost all of mainstream mathematics is perfectly happy to remain in ZFC. There is separately an interesting empirical/philosophical question of whether there might still be a "practically complete" set of axioms to do mathematics which is not definitively settled by Godel's Incompleteness Theorems. > And are you saying formal proof assistants like coq and isabelle are fools errands, in the sense that mathematics is in principal beyond formalization? If not, then why not? Ugh this is why associating Godel's Incompleteness Theorems with truth can be so misleading. Godel's Incompleteness Theorems, in contexts where Godel's Completeness Theorem holds, has little overall consequence for formal proof assistants. Whether the conception of abstraction in a human mind in principle is beyond formalization is a deep philosophical question (but this is not specific to mathematics, this is really just the age old philosophical question of whether qualia and the human consciousness are reducible). However mathematics as practiced by working mathematicians and laid out in theorems and proofs is formalizable essentially by definition.
burakemir 6y ago
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.
morelisp 6y ago
> And are you saying formal proof assistants like coq and isabelle are fools errands[?] No, and I have no clue how you could get that from what I wrote. To move back into a more familiar domain, Rice's theorem puts a frustrating limit on what we can accomplish via static analysis of programs, and yet the static analysis we can do remains extremely helpful in programming.

sn41 6y ago

The consistency of ZFC cannot be proven in ZFC - this follows from the second incompleteness theorem. The consistency of ZFC is a very useful theorem. There are also very easy to understand number-theoretic and combinatorial results, like the Paris-Harrington Theorem [1] and Goodstein's Theorem [2] which are provably independent of Peano Arithmetic. The latter has an interpretation as a "hydra" game: there is a rooted tree (hydra), and you can cut off a number of heads in one shot. The hydra grows back a finite number of heads according to a specified rule. The question is, is there a strategy to slay the hydra? The surprising answer is that any strategy will work(!), but you cannot prove this fact inside Peano arithmetic. [1] https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor... [2] https://en.wikipedia.org/wiki/Goodstein%27s_theorem https://en.wikipedia.org/wiki/Goodstein%27s_theorem

dwohnitmok 6y ago
> The consistency of ZFC cannot be proven in ZFC - this follows from the second incompleteness theorem. The consistency of ZFC is a very useful theorem. Perhaps less useful than one might think. Given that an inconsistent system can prove anything, if you weren't convinced of ZFC's consistency to begin with I hardly think you'd be convinced by a proof of its consistency in itself. Godel's Second Incompleteness Theorem is important "in the other direction," that is its consequence for systems bigger than ZFC (or indeed PA)/larger statements that imply the consistency of your formal system in question. (A previous comment I made on this in greater detail https://news.ycombinator.com/item?id=25118038 https://news.ycombinator.com/item?id=25118038)
oh_sigh 6y ago
The answer is surprising only if you believe the specified rule can be any rule. But really, the specified rule may have enough complexity in it that makes it difficult to intuitively reason about the problem at all, at which point it isn't really a counter-intuitive result, merely a counter-intuitive rule.

dwohnitmok 6y ago

I feel like some weird hawk that swoops in for a lot of these Godel comments. No Godel's incompleteness theorems prove nothing about truth by themselves. They are only statements about proofs and can be independently paired with other statements (as well as their negation), both philosophical and mathematical, about truth. That is the incompleteness theorems are silent on the matter of truth as a direct consequence, but require other theorems or philosophies to further mold statements on truth (the incompleteness theorems do have important indirect impact on those statements). For example there is Godel's Completeness Theorem , which in a vague sense proves that "all true things are provable" (I can explain in greater detail if so desired). Godel's Completeness Theorem holds independently of Godel's Incompleteness Theorems (that is all four possible pairings of holding/not holding can apply to different formal systems). Notably Godel's Completeness Theorem holds for first order logic, the most common formalization of mathematical foundations (which includes ZFC and Peano Arithmetic). > Can you give an example of a statement that is independent of ZFC yet useful/often-used? Very briefly, the proof of Fermat's Last Theorem used an axiom that is independent of ZFC (it used a large cardinal axiom). It was later found that the proof did not require this axiom and could be fully formalized within ZFC. There are separately simple-sounding and useful-sounding, but not actually used, statements which are independent of ZFC (such as if the set X is smaller than the set Y by cardinality then X has fewer subsets than Y). But almost all of mainstream mathematics is perfectly happy to remain in ZFC. There is separately an interesting empirical/philosophical question of whether there might still be a "practically complete" set of axioms to do mathematics which is not definitively settled by Godel's Incompleteness Theorems. > And are you saying formal proof assistants like coq and isabelle are fools errands, in the sense that mathematics is in principal beyond formalization? If not, then why not? Ugh this is why associating Godel's Incompleteness Theorems with truth can be so misleading. Godel's Incompleteness Theorems, in contexts where Godel's Completeness Theorem holds, has little overall consequence for formal proof assistants. Whether the conception of abstraction in a human mind in principle is beyond formalization is a deep philosophical question (but this is not specific to mathematics, this is really just the age old philosophical question of whether qualia and the human consciousness are reducible). However mathematics as practiced by working mathematicians and laid out in theorems and proofs is formalizable essentially by definition.

burakemir 6y ago

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.

morelisp 6y ago

> And are you saying formal proof assistants like coq and isabelle are fools errands[?] No, and I have no clue how you could get that from what I wrote. To move back into a more familiar domain, Rice's theorem puts a frustrating limit on what we can accomplish via static analysis of programs, and yet the static analysis we can do remains extremely helpful in programming.