The scene is a familiar one. The brightest student in the mathematics class (who, naturally enough, intends to double-major in philosophy and business administration) has cornered the professor at the end of the third week.
Student: I'm not sure exactly what a proof is?End of scenario. But not, of course, the end of the debate. And it is a debate that has achieved increasing significance in recent years, with the arrival on the scene of computer proofs, the development and use of automatic theorem provers, and the attempts to provide verification of computer systems. Just what do we mean by a 'proof'?
Professor: It's exactly what I said in class. A proof is a sound, logical argument that establishes the truth of the statement in question.
S: But how do you know an argument is sound and logical? What do those words mean?
P: Good heavens, surely you can recognize a logical argument when you see one, can't you? Weren't you convinced by any of the examples I did in class?
S: Well, I was convinced that your examples of false proofs were indeed false. In each case, once you pointed out the logical error, I could see why that particular argument was not a proof. But I'm not so sure about the examples you gave that you said were valid proofs. I admit I could't see any logical errors, and the arguments did seem pretty convincing. But how can we know for sure that the argument was sound, and that there was not some hidden error that we all missed.
P: Well, you know, those proofs have all been around for hundreds of years, and lots of very clever mathematicians have examined them, and no one has found any errors. Surely, we can't all be wrong, can we?
S: Probably not. But doesn't that mean that the notion of a valid proof is a socially defined one; that what makes a proof valid is that the majority of mathematicians agree it is valid?
P: Good Lord, no. To be valid, a proof has to follow the laws of logic. You make a series of statements, each of which follows from the previous ones by the laws of logic.
S: What rules of logic? You never told us what they were. It seemed to me that for each of your examples, you presented a series of statements in which each one sure seemed reasonable, given the previous ones. But where were the rules of logic? How is what you did different from a clever political argument?
P: Well, of course, to make it easy for you to follow the proof, I did not write down every step. But it could be done. Logicians sorted all this out early this century. They developed a formal language for expressing proofs, 'predicate calculus' they call it, figured out the basic axioms of logic, specified the rules of deduction--I think one of them is called 'modus ponens' or something like that--and then you get a total rigorous notion of a proof. In fact, it is so rigorous that in some areas of mathematics--not mine, I hasten to add--you can program a computer to do it for you, to generate proofs or to check them.
S: So what you are saying is that any one of the ordinary, everyday proofs mathematicians deal with in their work can be re-written in a formal way that fits into this framework the logicians have axiomatized.
S: So why didn't you do that in class? Why not tell us what the axioms and rules of logic are and do it that way?
P: Good grief, that would be hopeless. If I tried to make even the simplest proof that precise, it would be incredibly long, and quite unreadable. You would never be able to follow it. It would be far less convincing than the version I gave.
S: You mean that no one ever does write a proof down in formal logic?
P: Yes, now you're getting it. In principle it could be done. Any valid proof could be written out in full in formal logic, and then it would satisfy the logician's definition of a proof.
S: Only, it would be so long that no one could actually read it and check that it was right.
S: So let me see if I have got this right. What you are saying is that, strictly speaking, a proof is valid if it is written out in predicate calculus and has the right structure according to the rules of logic. But such proofs are far too long and complicated for anyone to read, so no one ever does it. What happens in practice is that a proof is declared to be valid if it could, in principle, be written out in this formal way.
P: Yes, that's about it.
S: But how do you know that your proof, the one you write on the board, could be written out as a formal proof if you never actually do it?
P: Well, you just look at it. The irrationality of root-two for example. The argument I gave is quite obviously valid, so you know it could be translated into a valid predicate calculus proof.
S: But how do you know, if no one has ever done it?
P: ( Impatiently). Well, you know, those logicians were clever folk, and we know from their work that any valid proof could be written out in that way, at least in principle.
S: But how do you know your proof is valid in the first place?
P: Look, I really don't have time for this. You're just going round in circles. You clearly haven't really understood what is involved in proving something. Maybe mathematics is not your subject. Have you thought about taking a philosophy course instead?
It seems that mathematicians--and to avoid generating too many letters of complaint, let me hasten to rephrase that as 'we mathematicians'--are somewhat schizophrenic when it comes to answering this question. When pressured by the persistent student, we fall back on the logician's definition and the 'translatable in principle' defense. But in practice, we work happily with what is quite clearly a socially determined notion of proof. Though we might harbor doubts about particularly long and novel proofs, we generally feel confident in our ability to tell a sound argument from an invalid one. Moreover, we tend to feel that it really is not an issue of judgement, and that for all their surface brevity, the proofs we construct and publish are, in an absolute sense, genuine proofs. I certainly feel that way. But I also know from experience that the certainty (we) mathematicians feel about this issue is not easily explained to others outside the field, to whom, I suspect, it really does seem as though we are simply playing a game by rules we determine, decided by some sort of secret poll.