> 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? :)
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.
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?
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).
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
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.
Mathematical papers are seldom written fully formally. This is in no small part because the most commonly accepted foundation of mathematics (ZFC atop first-order logic) was only designed to make formalization possible “in principle”. It's precisely because of this that researchers in formal verification are looking for systems that make formalization actually possible in practice, such as various flavors of type theory.
I think you should almost replace "spoken language" in that quote with "natural language". As opposed to a formal syntax like used by Russel and Walllace -- or indeed any programming language.
I say "almost replace" because even natural languages can be restricted into formal versions good enough for proofs. People have been playing that game since Aristotle and his sylogisms.
its a pedantic point but most proofs are handwavy in the sense that they don't show which rule of inference allows them to claim a particular intermediary result. Proving anything but the most trivial thing where every single deduction is made is quite tedious, but the sentiment is correct.
To me, a proof would have to be a Turing complete procedure for verifying a theorematic result. Often times, proofs, however, only amount to convincing arguments (convincing to adepts, that is, who have not yet discovered a flaw in the proof). Furthermore, yes, I truly believe that proofs provided through computational analysis are perfectly legitimate, even if mere humans can hardly cope with them.
After Gentzen introduced the idea of a the sequent calculus and the idea of a Turing Machine was shown to be a complete answer to the idea of what a "computable function" is, I think the answer to the question "what is a proof" is really something along the lines of: a proof is a kind of computable function. Trying to spell out what kind of computable functions they are is a big part of one of the main outstanding problems of mathematics known as the P v NP problem. In other words, you recognize these drawings as "proofs" when you are trained to see them but nobody really knows how to define a general procedure that will output all of the correct drawings correctly (using whatever symbolism or notation you prefer). Hence the digression on proof assistants. I mean: you encounter the overall idea of producing logical drawings that demonstrate mathematical truths in elementary school geometry and then try to make those concepts more precise (as David Hilbert did) all the way through to research level mathematical logic and even then, after learning concepts that take years to master, you will still never quite know how to answer the question posed in the title of the blog post.
It's weird to me to identify proofs with a computable function that generates the steps in a sequent calculus proof. Why would this be more fundamental than the steps themselves? Even in mathematical foundations where computable functions are very important (e.g. intensional type theories like CoC) we have proof terms that are not functions (e.g. existence proofs are of sigma type, not pi type).
> Trying to spell out what kind of computable functions they are is a big part of one of the main outstanding problems of mathematics known as the P v NP problem. In other words, you recognize these drawings as "proofs" when you are trained to see them but nobody really knows how to define a general procedure that will output all of the correct drawings correctly (using whatever symbolism or notation you prefer).
P vs NP has little to do with what computable functions we consider to be proofs, if we decide to go that route at all. All proposed general mathematical foundations (ZFC, ETCS, MLTT, various HoTTs) have polynomial proof checking[1], so yes a P=NP result will mean we can check the truth of a mathematical statement in polynomial time (in the size of the proof at least), but this magic algorithm will just spit out the same form of proof that the NP verifier takes as input. This has nothing to do with what we decide to consider the format of a proof to be.
> I mean: you encounter the overall idea of producing logical drawings that demonstrate mathematical truths in elementary school geometry and then try to make those concepts more precise (as David Hilbert did) all the way through to research level mathematical logic and even then, after learning concepts that take years to master, you will still never quite know how to answer the question posed in the title of the blog post.
For particular mathematical systems, this is very much a solved problem since we have verifiers for a variety of mathematical foundations including ZFC. If you mean "what does a proof for any suitable logical system look like", we would generally require that it be some class of input that can be put into a particular computable function that is the verifier, but there is no reason to require the proof itself to be a computable function.
[1]: Yes, there are type theories with undecidable type checking but at the proof-theoretic level we would generally require the evidence that our proof term type checks to be part of the proof of a statement so this doesn't make much of a difference here.
Alan Perlas, Dick Lipton, and Richard De Millo addressed this question in their POPL3 paper, Social Processes and Proof of Theorems and Programs,
https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf. It is still a good read.
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? :)