5 ms·

”He also helped to edit the papers of Kurt Gödel, known for his famous (and famously difficult) Incompleteness Theorems, which establish that there can be no co

”He also helped to edit the papers of Kurt Gödel, known for his famous (and famously difficult) Incompleteness Theorems, which establish that there can be no consistent axiomatic theory of logic from which the whole of mathematics can be derived, a man who has been called the most important logician since Aristotle.” Gödel’s work is characterized like this all the time, like if he proved that there is something magical about mathematics, as if it’s above and beyond logic. But that’s not what Gödel proved, right? My understanding is: All of mathematics can in principle be derived from ZFC. Gödel proved that there are mathematical statements (conjectures) that are true but cannot be proven (in ZFC). They are however, by definition, not theorems (in ZFC) and not part of mathematics in any reasonable sense.

morelisp 6y ago
> All of mathematics can in principle be derived from ZFC. Even this isn't true; many useful (as in often-used) statements are independent of ZFC, and not even in the semantically funny way a Gödel sentence is. Or maybe ZFC is inconsistent, in which case all of mathematics surely can be derived from it - but so can all mathematical lies. Gödel also proves we can't know if it is or isn't (at least by the standards mathematical formalists seek). > not part of mathematics in any reasonable sense. This is an aesthetic claim about what theorems get to count as "real mathematics", and one both Gödel (who believed in the literal existence of mathematical objects and therefore actual truth of his sentences) and contemporary hardcore formalists (whose goal was to find some extension of PA both complete and consistent) would disagree with. Gödel quite literally proved mathematics is "beyond" (as in its truths cannot be wholly captured by) and "above" (as in mathematical rules seem to be able to characterize the whole of) mathematical logic. Whether that makes it "magical" or not is something we will probably debate for another century.
- bjornsing 6y ago
  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.
- dwohnitmok 6y ago
  > Gödel quite literally proved mathematics is "beyond" (as in its truths cannot be wholly captured by) and "above" (as in mathematical rules seem to be able to characterize the whole of) mathematical logic. Godel's Incompletness Theorems do not by themselves address truth, but instead require additional theorems and/or philosophical commitments to decide either way.
  - morelisp 6y ago
    > Godel's Incompletness Theorems do not by themselves address truth This is itself a sort of philosophical commitment - and again, not one shared by Gödel or the logicist program.
    - dwohnitmok 6y ago
      I mean yes, in so far as any statement about philosophy is a philosophical commitment, but that kind of feels like nitpicking no? In very real ways Godel's Incompleteness Theorems do not address truth. Their proofs are purely syntactic rather than semantic. > and again, not one shared by Gödel or the logicist program. The logicist program is a bit tricky to pin down; the major figures associated with it either were no longer active in mathematical logic by the time of Godel's result (e.g. Russell) or were but never made any response to them (e.g. Hilbert). However, we know Godel's take on the matter. In particular I don't think this is an accurate account of Godel's own viewpoint. It is clear Godel clearly believed that there were mathematical truths that could not be expressed by formal systems. However, it is also clear that Godel acknowledges this to be an additional philosophical commitment. Godel himself cleanly states this in his 1951 Gibbs Lecture. > Does it [his incompleteness theorems, in particular his second one] mean that no well-defined system of mathematics can contain all of mathematics proper? It does, if by mathematics proper is understood the system of all true mathematical propositions; it does not, however, if one understands by it the system of all demonstrable mathematical propositions. I shall distinguish between these two meanings of mathematics as mathematics in the objective and in the subjective sense. Godel is pointing out that his incompleteness theorems require an additional philosophical commitment to "objective" or "subjective" mathematics in order to make a statement on truth (what he refers to as "true" in his comment already demonstrates his own predilection towards "objective" mathematics being the correct philosophical commitment, but the important point here is that he is making the distinction). As a footnote, Godel's notion of mathematical truth is an extremely strong Platonist position that I don't think most HN commentators would agree with (at least at the beginning; they may be swayed to come around to it). Godel believed there were no truly independent mathematical statements, only ones temporarily independent of our limited set of axioms. Every mathematical statement is either true or false. For example, the continuum hypothesis will be definitively decided one way or the other (if I recall Godel ultimately estimated the continuum hypothesis to be false).

morelisp 6y ago

> All of mathematics can in principle be derived from ZFC. Even this isn't true; many useful (as in often-used) statements are independent of ZFC, and not even in the semantically funny way a Gödel sentence is. Or maybe ZFC is inconsistent, in which case all of mathematics surely can be derived from it - but so can all mathematical lies. Gödel also proves we can't know if it is or isn't (at least by the standards mathematical formalists seek). > not part of mathematics in any reasonable sense. This is an aesthetic claim about what theorems get to count as "real mathematics", and one both Gödel (who believed in the literal existence of mathematical objects and therefore actual truth of his sentences) and contemporary hardcore formalists (whose goal was to find some extension of PA both complete and consistent) would disagree with. Gödel quite literally proved mathematics is "beyond" (as in its truths cannot be wholly captured by) and "above" (as in mathematical rules seem to be able to characterize the whole of) mathematical logic. Whether that makes it "magical" or not is something we will probably debate for another century.

bjornsing 6y ago
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.
dwohnitmok 6y ago
> Gödel quite literally proved mathematics is "beyond" (as in its truths cannot be wholly captured by) and "above" (as in mathematical rules seem to be able to characterize the whole of) mathematical logic. Godel's Incompletness Theorems do not by themselves address truth, but instead require additional theorems and/or philosophical commitments to decide either way.
- morelisp 6y ago
  > Godel's Incompletness Theorems do not by themselves address truth This is itself a sort of philosophical commitment - and again, not one shared by Gödel or the logicist program.
  - dwohnitmok 6y ago
    I mean yes, in so far as any statement about philosophy is a philosophical commitment, but that kind of feels like nitpicking no? In very real ways Godel's Incompleteness Theorems do not address truth. Their proofs are purely syntactic rather than semantic. > and again, not one shared by Gödel or the logicist program. The logicist program is a bit tricky to pin down; the major figures associated with it either were no longer active in mathematical logic by the time of Godel's result (e.g. Russell) or were but never made any response to them (e.g. Hilbert). However, we know Godel's take on the matter. In particular I don't think this is an accurate account of Godel's own viewpoint. It is clear Godel clearly believed that there were mathematical truths that could not be expressed by formal systems. However, it is also clear that Godel acknowledges this to be an additional philosophical commitment. Godel himself cleanly states this in his 1951 Gibbs Lecture. > Does it [his incompleteness theorems, in particular his second one] mean that no well-defined system of mathematics can contain all of mathematics proper? It does, if by mathematics proper is understood the system of all true mathematical propositions; it does not, however, if one understands by it the system of all demonstrable mathematical propositions. I shall distinguish between these two meanings of mathematics as mathematics in the objective and in the subjective sense. Godel is pointing out that his incompleteness theorems require an additional philosophical commitment to "objective" or "subjective" mathematics in order to make a statement on truth (what he refers to as "true" in his comment already demonstrates his own predilection towards "objective" mathematics being the correct philosophical commitment, but the important point here is that he is making the distinction). As a footnote, Godel's notion of mathematical truth is an extremely strong Platonist position that I don't think most HN commentators would agree with (at least at the beginning; they may be swayed to come around to it). Godel believed there were no truly independent mathematical statements, only ones temporarily independent of our limited set of axioms. Every mathematical statement is either true or false. For example, the continuum hypothesis will be definitively decided one way or the other (if I recall Godel ultimately estimated the continuum hypothesis to be false).