To citater om matematik

Hvordan ved vi at et formelt system er konsistent?
Hvad er et matematisk bevis?

Do We Know the System Is Consistent?

Up till now, we have only presumed that all theorems, when interpreted as indicated, are true statements. But do we know that that is the case? Could we prove it to be? This is just another way of asking whether the intended interpretations (`and' for '^', etc.) merit being called the "passive meanings" of the symbols. One can look at this issue from two very different points of view, which might be called the "prudent" and "imprudent" points of view. I will now present those two sides as I see them, personifying their holders as "Prudence" and "Imprudence".

Prudence: We will only KNOW that all theorems come out true under the intended interpretation if we manage to PROVE it. That is the cautious, thoughtful way to proceed.

Imprudence: On the contrary. It is OBVIOUS that all theorems will come out true. If you doubt me, look again at the rules of the system. You will find that each rule makes a symbol act exactly as the word it represents ought to be used. For instance, the joining rule makes the symbol '^' act as 'and' ought to act; the rule of detachment makes '' act as it ought to, if it is to stand for 'implies', or `if-then'; and so on. ... you will recognize in each rule a codification of a pattern you use in your own thought. So if you trust your own thought patterns, then you HAVE to believe that all theorems come out true! That's the way I see it. I don't need any further proof. If you think that some theorem comes out false, then presumably you think that some rule must be wrong. Show me which one.

Prudence: I'm not sure that there is any faulty rule, so I can't point one out to you. Still, I can imagine the following kind of scenario. You, following the rules, come up with a theorem — say x. Meanwhile I, also following the rules, come up with another theorem — it happens to be ~x. Can't you force yourself to conceive of that?

Imprudence: All right; let's suppose it happened. Why would it bother you? Or let me put it another way. Suppose that in playing with the MIU-system, I came up with a theorem x, and you came up with xU. Can you force yourself to conceive of that?

Prudence: Of course—in fact both MI and MIU are theorems.

Imprudence: Doesn't that bother you?

Imprudence: Well, yes—provided you wish to interpret `~' as 'not'. But what would lead you to think that `~' should be interpreted as 'not'?

Prudence: The rules themselves. When you look at them, you realize that the only conceivable interpretation for `~' is `not' — and likewise, the only conceivable interpretation for '^' is 'and', etc.

Imprudence: In other words, you are convinced that the rules capture the meanings of those words?

Prudence: Precisely.

Imprudence: And yet you are still willing to entertain the thought that both x and ~x could be theorems? Why not also entertain the notion that hedgehogs are frogs, or that 1 equals 2, or that the moon is made of green cheese? I for one am not prepared even to consider whether such basic ingredients of my thought processes are wrong—because if I entertained that notion, then I would also have to consider whether my modes of analyzing the entire question are also wrong, and I would wind up in a total tangle.

Prudence: Your arguments are forceful . . . Yet I would still like to see a PROOF that all theorems come out true, or that x and ~ x can never both be theorems.

Imprudence: You want a proof. I guess that means that you want to be more convinced that the Propositional Calculus is consistent than you are convinced of your own sanity. Any proof I could think of would involve mental operations of a greater complexity than anything in the Propositional Calculus itself. So what would it prove? Your desire for a proof of consistency of the Propositional Calculus makes me think of someone who is learning English and insists on being given a dictionary which defines all the simple words in terms of complicated ones....

Let's see how our ideal mathematician made out with a student who came to him with a strange question.

Student: Sir, what is a mathematical proof ?

I.M.: You don't know that? What year are you in?

Student: Third-year graduate.

I.M.: Incredible! A proof is what you've been watching me do at the board three times a week for three years! That's what a proof is.

Student: Sorry, sir, I should have explained. I'm in philos­ophy, not math. I've never taken your course.

I.M.: Oh! Well, in that case—you have taken some math, haven't you? You know the proof of the fundamental theorem of calculus—or the fun­damental theorem of algebra?

Student: I've seen arguments in geometry and algebra and calculus that were called proofs. What I'm asking you for isn't examples of proof, it's a def­inition of proof. Otherwise, how can I tell what examples are correct?

I.M.: Well, this whole thing was cleared up by the logi­cian Tarski, I guess, and some others, maybe Russell or Peano. Anyhow, what you do is, you write down the axioms of your theory in a for­mal language with a given list of symbols or al­phabet. Then you write down the hypothesis of your theorem in the same symbolism. Then you show that you can transform the hypoth­esis step by step, using the rules of logic, till you get the conclusion. That's a proof.

Student: But even that doesn't sound like what was done in my courses and textbooks. So mathemati­cians don't really do proofs, after all.

I.M.:  Of course we do! If a theorem isn't proved, it's nothing.

Student: Then what is a proof? If it's this thing with a for­mal language and transforming formulas, no­body ever proves anything. Do you have to know all about formal languages and formal logic before you can do a mathematical proof?

I.M.: Of course not! The less you know, the better. That stuff is all abstract nonsense anyway.

Student: Then really what is a proof?

I.M.: Well, it's an argument that convinces someone who knows the subject.

Student: Someone who knows the subject? Then the defi­nition of proof is subjective; it depends on par­ticular persons. Before I can decide if some­thing is a proof, I have to decide who the experts are. What does that have to do with proving things?

I.M.: No, no. There's nothing subjective about it! Everybody knows what a proof is. Just read some books, take courses from a competent mathematician, and you'll catch on.

Student: Then you decide what a proof is, and if I don't learn to decide in the same way, you decide I don't have any aptitude.