3 ms·

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

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
  Ok, thanks, that makes sense. So I can sleep well at night knowing that at least my (purely assumed) understanding of Russel's dream is alive and well: we have found a formal system with axioms and inference rules (ZFC) within which all mainstream mathematics can (hopefully and in principle) be formally proven. Gödel however tells us 1) that there are mathematical "truths" (statements that always hold) which cannot be proven within ZFC, and 2) that ZFC could be inconsistent. The practical consequences of that are however limited. :) Is that a reasonable summary? :P
  - johncolanduoni 10y ago
    Yep! It's even rosier than that actually; we have quite a few foundational theories that appear to be able to handle the vast majority of mathematics pretty well.

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
Ok, thanks, that makes sense. So I can sleep well at night knowing that at least my (purely assumed) understanding of Russel's dream is alive and well: we have found a formal system with axioms and inference rules (ZFC) within which all mainstream mathematics can (hopefully and in principle) be formally proven. Gödel however tells us 1) that there are mathematical "truths" (statements that always hold) which cannot be proven within ZFC, and 2) that ZFC could be inconsistent. The practical consequences of that are however limited. :) Is that a reasonable summary? :P
- johncolanduoni 10y ago
  Yep! It's even rosier than that actually; we have quite a few foundational theories that appear to be able to handle the vast majority of mathematics pretty well.