117 } Pv~P

Intuitively it also makes sense that this should be a logical truth if we assume that each sentence P is either true or false -- which means that either P or ~P are true. Here is our proof.

117 } Pv~P

This proof is worth examining closely. It is an interesting and beautiful proof. There is simply no way to start it without assuming the negation of what we want to prove. On line 1 we assume the negation of the logical truth that we are trying to prove. That is the only way to get this proof started.

And then we have to figure out how to get a contradiction.

What we can do is assume P on line 2 and then use vI on line 3. This gives us a contradiction on line 4, which enables us to derive ~P on line 5. This in turn leads to a second contradiction on line 7 that is based only on the initial assumption we made. So we can negate that assumption on line 8, giving us the proof of the logical truth on line 9.

Why did we assume P on line 2? When we assume P on line 2, we of course we have an RA strategy in mind, so as to get ~P on line 5. Yet the reason we want to get ~P on line 5 is to get Pv~P on line 6. Notice that the proof is not finished there at line 6, even though Pv~P appears on line 6 (and that is indeed what we are trying to prove), but we are not done because line 6 has an assumption (line 1) whereas we wish to show here that Pv~P is a logical truth, that is, that it can be derived with no assumptions. And we are able to do this on line 9.

This proof requires creativity! We have to be on our toes to do it. The key is knowing how to use the humble vI Rule that we use on lines 3 and 6. (If you had forgotten about that Rule, you would not be able to do this proof!) We now are at a point where we will be able to use creativity in skillfully using all of our Rules to develop some complex proofs.

The assumption of P on line 2 makes sense because it works out. When we look at each line in the proof, we obviously have used our Rules correctly on each and every line, and we have indeed reached the final line where we have Pv~P based on no assumptions. So we certainly do succeed in proving that Pv~P is a logical truth for our system.

Now we can ask another question. Should sequent 117 really be regarded as a "logical truth"? That is, given the meaning of "or", does it follow that for any sentence P, either P or ~P is true (no matter what P may be talking about)? Philosophers disagree about this point.Those who think the sentence should not be regarded as logically true will point to sentences like "Professor X now has stopped stealing money from his students." If this sentence is represented as P, one might object that neither P nor ~P is true in the normal case where we are talking about a professor who never stole any money at all (P isn't true because Prof. X hasn't stopped, since he never started; but ~P isn't true either because that says he hasn't stopped!) But most sentences are such that either P or ~P is true, and some philosophers will try to defend 117 as a logical truth.

This sort of puzzle actually has led to the development of alternative systems of basic logic that do not treat sequent 117 as a logical truth pertaining to "or". One can create such alternative systems by adding, deleting, or revising our basic standard Rules. For example, we could get so-called "Intuitionistic" logic by re-examining our concept of negation, and fiddling with the Rule DN --were we to revise this Rule so that we could derive ~~P from P, but we could not go from ~~P to P, we get the Intuitionistic alternative to Standard logic; and we actually would not be able to prove 117 in the new Intuitionistic system! (Notice the role of our DN in the step from 8 to 9 in the proof above; and it turns out there'd be no other way to prove it in our system. So sequent 117 would not a logical truth in the so-called Intuitionistic system.)

We also can prove other things in our system that some philosophers of logic have found suspect. Once we have put the spotlight on the core notions things sometimes are not as simple as they seem to be at first. Investigations such as these, of course, go well beyond the scope of our present course in basic Standard logic --not because it would be too difficult for you to understand, but simply because we are going to run out of time (the semester will end too soon). If you are interested, you can look into this on your own, e.g. in some books by Susan Haack, such as Philosophy of Logics (Cambridge, 1978).