What is a Proof?
samidavies.wordpress.com
samidavies.wordpress.com
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? :)
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?
1. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
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_arithm...
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... :)
That doesn't sound right. Nearly all proofs are communicated in a written formal language. That's completely different than spoken language.
Am I missing something?
Formal here is not "Mathy and jargony and with a lot of greek symbols" as is understood normally.
Right. That's the formal I'm also referring to.
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.
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.