3 ms·

> Near the turn of the 20th century, some important advancements were made in mathematical logic. Principia Mathematica was an attempt to report the axioms and

> Near the turn of the 20th century, some important advancements were made in mathematical logic. Principia Mathematica was an attempt to report the axioms and inference rules needed to prove any mathematical truth. 20 years later, Gödel’s incompleteness theorem proved that such a goal could never be accomplished. This part fascinates me. As I understand it Gödel's incompleteness theorem states essentially that "in any formal axiomatic system large enough to contain arithmetic there will be true statements that cannot be proven". But doesn't that apply to the less formal "natural language" proofs of mathematicians as well...? When I read sections like the above (in many different places) I sometimes get the feeling that the authors think that "Gödel proved that formal proofs cannot prove all mathematical truths, so we mathematicians switched to informal proofs instead (to get around Gödel's incompleteness theorem and continue on our quest to prove all mathematical truths)". Can someone confirm that this is not the intended meaning? :P As I see it, let there be sets of mathematical statements A, B and C such that A are all true statements, B are all statements that can be formally proven and C are all statements that have a beautiful proof (from "The Book"); then C must be a (possibly equal) subset of B, which must in turn be a (possibly equal) subset of A. Right? :)

bjornsing 10y ago
> B, which must in turn be a (possibly equal) subset of A Correction: Gödel has proven that B is a proper subset of A :) so that last "(possibly equal)" should have been "proper". :P No comments, anybody? I really want to know... :)
- deleted 10y ago
  [deleted]
johncolanduoni 10y ago
This is not the meaning of the incompleteness theorem. We still ostensibly work within the formal framework of a theory (usually Zermelo-Fraenkel set theory with axiom of choice a.k.a. ZFC) that cannot be proved consistent. We usually call these theories a "foundation" for mathematics. The (relatively) informal nature of mathematical proofs is not an attempt to run away from this, since truly informal reasoning is even more susceptible to contradiction (e.g. Naive set theory and russel's paradox). What Godel's theorem actually restricts is proving "absolute" statements. Whenever we prove X in most mathematics today what we know to be incontrovertible is that "within ZFC X is provable" (assuming there aren't any immediate errors within the proof). Since we can't prove that ZFC is consistent, this might turn out to be a very boring statement indeed (since if it is inconsistent we'll have 2+2=5 too). Godel won't let us sneak off and find some super-foundation that can be proved consistent inside itself and then find out the "absolute truth" of mathematical statements, so we're stuck with this state of affairs. Mathematicians generally look at the consistency of foundational systems a bit like a physicist looks at a physical law. It's possible that we're working within an inconsistent system and all our proofs are meaningless, but we've been looking really hard for a long time, and a lot of the axioms we were once worried about (e.g. Excluded middle and choice) can be conclusively shown to not lead to a contradiction (via independence proofs) so we're probably okay. Also virtually none of mathematics is tightly bound to our particular choice of foundations, so few believe that even in the case of such a crisis that we'd have to throw out all mathematics. We would likely just need to rebase it a bit. As a result, we've mostly continued on as we did before Godel's result, except we've developed the meta-theory of our mathematical foundations to try and root out any problems. We've also stopped talking about axioms being "true", and just started looking at them as rules in a game.
- bjornsing 10y ago
  Thanks so much for the answer! :D But are you absolutely sure that my brief characterization of Gödel's incompleteness theorem is so off...? Wikipedia phrases it "no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of the natural numbers. For any such formal system, there will always be statements about the natural numbers that are true, but that are unprovable within the system." [1] In what way is that (materially) different from my characterization? On Gödel's second incompleteness theorem, that "the system [as defined above] can not demonstrate its own consistency", I think we agree. The logical consequences of that which you bring up all seem very reasonable to me. But the real question as I see it is why you guys have abandoned Russel's ambitions to formalize all of mathematics. Why is his efforts so often described as more or less hopeless, in light of Gödel's results? As I see it (and as I interpret your answer) all of mathematics can be formally proven within ZFC, in machine readable/checkable form. Why not do it...? Or, perhaps, rather, why characterize it as "hopeless" in any sense? 1. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
  - johncolanduoni 10y ago
    Sorry I wasn't clear, but Godel's theorems have not made the formalization (in the sense of writing machine-checkable, or at least fully explicit proofs) impossible or undesirable. The reason we don't write up the proofs in mathematical papers as Coq files or something equivalent is purely practical: doing so for most mathematics is exceedingly tedious with our existing tools. In addition, proof assistants have a steep learning curve even for mathematicians, as they are designed by mathematical logicians who have a very specific kind of mathematics in mind. What these theorems made hopeless is the formalization of the concept of "the" natural numbers. Previously, it was taken for granted that our definitions of the natural numbers entirely fixed the truth of all of the statements you could make about them. However Godel showed that we have to pick a particular formalization, which will necessarily leave some facts about the natural numbers undetermined. Even simple theories which formalize the natural numbers and nothing else (e.g. Peano arithmetic) suffer from this problem. This results in things like non-standard arithmetic[1], which no axiomatization of the natural numbers can possibly avoid entirely. Most of mathematics is not about the natural numbers directly, but virtually all mathematical structures can be used to model the natural numbers with addition and multiplication in some way (e.g. Dimensionality of vector spaces) so similar restrictions apply here too. But none of this gives us any reason to avoid formal proofs; if a mathematician feels that an informal proof truly omits an important step or is missing full justification of a statement then they would regard the proof as incomplete (at least until the issue is clarified). [1]: https://en.m.wikipedia.org/wiki/Non-standard_model_of_arithmetic https://en.m.wikipedia.org/wiki/Non-standard_model_of_arithm...

bjornsing 10y ago

> B, which must in turn be a (possibly equal) subset of A Correction: Gödel has proven that B is a proper subset of A :) so that last "(possibly equal)" should have been "proper". :P No comments, anybody? I really want to know... :)

deleted 10y ago
[deleted]

johncolanduoni 10y ago

This is not the meaning of the incompleteness theorem. We still ostensibly work within the formal framework of a theory (usually Zermelo-Fraenkel set theory with axiom of choice a.k.a. ZFC) that cannot be proved consistent. We usually call these theories a "foundation" for mathematics. The (relatively) informal nature of mathematical proofs is not an attempt to run away from this, since truly informal reasoning is even more susceptible to contradiction (e.g. Naive set theory and russel's paradox). What Godel's theorem actually restricts is proving "absolute" statements. Whenever we prove X in most mathematics today what we know to be incontrovertible is that "within ZFC X is provable" (assuming there aren't any immediate errors within the proof). Since we can't prove that ZFC is consistent, this might turn out to be a very boring statement indeed (since if it is inconsistent we'll have 2+2=5 too). Godel won't let us sneak off and find some super-foundation that can be proved consistent inside itself and then find out the "absolute truth" of mathematical statements, so we're stuck with this state of affairs. Mathematicians generally look at the consistency of foundational systems a bit like a physicist looks at a physical law. It's possible that we're working within an inconsistent system and all our proofs are meaningless, but we've been looking really hard for a long time, and a lot of the axioms we were once worried about (e.g. Excluded middle and choice) can be conclusively shown to not lead to a contradiction (via independence proofs) so we're probably okay. Also virtually none of mathematics is tightly bound to our particular choice of foundations, so few believe that even in the case of such a crisis that we'd have to throw out all mathematics. We would likely just need to rebase it a bit. As a result, we've mostly continued on as we did before Godel's result, except we've developed the meta-theory of our mathematical foundations to try and root out any problems. We've also stopped talking about axioms being "true", and just started looking at them as rules in a game.

bjornsing 10y ago
Thanks so much for the answer! :D But are you absolutely sure that my brief characterization of Gödel's incompleteness theorem is so off...? Wikipedia phrases it "no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of the natural numbers. For any such formal system, there will always be statements about the natural numbers that are true, but that are unprovable within the system." [1] In what way is that (materially) different from my characterization? On Gödel's second incompleteness theorem, that "the system [as defined above] can not demonstrate its own consistency", I think we agree. The logical consequences of that which you bring up all seem very reasonable to me. But the real question as I see it is why you guys have abandoned Russel's ambitions to formalize all of mathematics. Why is his efforts so often described as more or less hopeless, in light of Gödel's results? As I see it (and as I interpret your answer) all of mathematics can be formally proven within ZFC, in machine readable/checkable form. Why not do it...? Or, perhaps, rather, why characterize it as "hopeless" in any sense? 1. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
- johncolanduoni 10y ago
  Sorry I wasn't clear, but Godel's theorems have not made the formalization (in the sense of writing machine-checkable, or at least fully explicit proofs) impossible or undesirable. The reason we don't write up the proofs in mathematical papers as Coq files or something equivalent is purely practical: doing so for most mathematics is exceedingly tedious with our existing tools. In addition, proof assistants have a steep learning curve even for mathematicians, as they are designed by mathematical logicians who have a very specific kind of mathematics in mind. What these theorems made hopeless is the formalization of the concept of "the" natural numbers. Previously, it was taken for granted that our definitions of the natural numbers entirely fixed the truth of all of the statements you could make about them. However Godel showed that we have to pick a particular formalization, which will necessarily leave some facts about the natural numbers undetermined. Even simple theories which formalize the natural numbers and nothing else (e.g. Peano arithmetic) suffer from this problem. This results in things like non-standard arithmetic[1], which no axiomatization of the natural numbers can possibly avoid entirely. Most of mathematics is not about the natural numbers directly, but virtually all mathematical structures can be used to model the natural numbers with addition and multiplication in some way (e.g. Dimensionality of vector spaces) so similar restrictions apply here too. But none of this gives us any reason to avoid formal proofs; if a mathematician feels that an informal proof truly omits an important step or is missing full justification of a statement then they would regard the proof as incomplete (at least until the issue is clarified). [1]: https://en.m.wikipedia.org/wiki/Non-standard_model_of_arithmetic https://en.m.wikipedia.org/wiki/Non-standard_model_of_arithm...