9 ms·

What is a Proof?

68 points by CarolineW 10y ago

danvayn 10y ago
Terrible title for a great blog about proof assistants imo
- johncolanduoni 10y ago
  Care to explain?
  - tgarma1234 10y ago
    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.
    - johncolanduoni 10y ago
      > a proof is a kind of computable function 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.
jonnybgood 10y ago
> Technically, a proof communicated in spoken language is an informal proof, and this is how nearly all proofs in mathematics are conveyed. 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?
- zeroxfe 10y ago
  This is not that uncommon -- e.g., most proofs of the undecidability of the halting problem.
- ambulancechaser 10y ago
  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.
- adrianratnapala 10y ago
  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.
- cscurmudgeon 10y ago
  Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Formal here is not "Mathy and jargony and with a lot of greek symbols" as is understood normally.
  - jonnybgood 10y ago
    > Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Right. That's the formal I'm also referring to.
bjornsing 10y ago
> 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.
superobserver 10y ago
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.
drallison 10y ago
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 https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf. It is still a good read.

What is a Proof?

68 points by CarolineW 10y ago

danvayn 10y ago

Terrible title for a great blog about proof assistants imo

johncolanduoni 10y ago
Care to explain?
- tgarma1234 10y ago
  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.
  - johncolanduoni 10y ago
    > a proof is a kind of computable function 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.

jonnybgood 10y ago

> Technically, a proof communicated in spoken language is an informal proof, and this is how nearly all proofs in mathematics are conveyed. 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?

zeroxfe 10y ago
This is not that uncommon -- e.g., most proofs of the undecidability of the halting problem.
ambulancechaser 10y ago
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.
adrianratnapala 10y ago
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.
cscurmudgeon 10y ago
Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Formal here is not "Mathy and jargony and with a lot of greek symbols" as is understood normally.
- jonnybgood 10y ago
  > Formal == Machine verifiable, and means the proof is written in a language with a well-defined syntax and semantics. Right. That's the formal I'm also referring to.

bjornsing 10y ago

> 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.

superobserver 10y ago

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.

drallison 10y ago

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 https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf. It is still a good read.