Philosophy 2340
Symbolic Logic

Language, Proof, and Logic
Notes on Chapters 5 and 6

Now we return to doing proofs. Last time we did proofs, we had only the =Intro, =Elim, and Reit rules. Now, however, we have added three logical connectives to our arsenal, and we can introduce rules governing what we can do with each of these.

Proof by Cases; Proof by Contradiction

Chapter 5 concerns informal "methods of proof." Chapter 6 concerns formal proofs. The informal methods apply to logical reasoning in general; the rules in chapter 6 are an attempt to formalize the informal methods and include them in our formal system. Although our homework will emphasize doing formal proofs, in a sense the informal methods are more important. There may be many different ways to formalize these informal methods; what is important about the formal rules is not so much the specific formalization as the general insights that they capture.

The main informal methods discussed in Chapter 5 are:

In proof by cases, we determine what possibilities there are, and then attempt to show that our conclusion follows no matter which of these possibilities obtains.

In proof by contradiction, we assume the opposite of what we want to prove, and show that this assumption leads to a contradiction. Then we conclude that our original assumption was false, i.e. that its negation is true.

Rules for and

The formal system includes not only rules corresponding to these informal methods, but also rules that capture steps that are so obvious that we don't usually notice them in informal reasoning, but that still need to be captured in the formal system. We will have Intro and Elim rules for every connective we introduce.

Today we are discussing only the conjunction and disjunction rules; next time we will consider the negation rules.

So, we need to discuss:

Three of these are very obvious and straightforward. The fourth, disjunction elimination, is more interesting, and corresponds to the method of proof by cases.

Rules for ¬ and

Now we will add Intro and Elim rules for ¬. In the process we introduce a new symbol, , with its own Intro and Elim rules.

Proofs with no Premises

Tautologies are provable with no premises at all. Since they must be true no matter what, i.e. since their truth does not depend on anything else, it is possible to construct proofs for them which start from scratch, so to speak.

Of course, most of the rules in our system can only be used if we already have one or more sentences to apply them to. The only exception we have had up until now is the rule of identity introduction, whose use is pretty limited. Now we have added another rule that requires no earlier steps: negation introduction. (Later we will add another, conditional introduction.) So at this point, if we are attempting to prove something with no premises, we can be pretty certain we will need to use negation introduction. (The only exception would be a proof in which we were just trying to prove something like a=a. But since that's so easy, it's not likely to be assigned as an exercise!)

(One sort-of exception is proofs where we use Taut Con to establish the Law of Excluded Middle, and then use disjunction introduction. But it is not really an exception, because if we actually go through the steps of proving Excluded Middle, we will need to use negation introduction.)

Hints on Constructing Proofs:

  1. Never start a subproof unless you know what rule you intend to use it for, and what the last line of the subproof will be.
  2. Try to see why the overall proof, and each step along the way, makes sense. (I.e. don't treat the rules as just a meaningless game; keep in mind why they are reasonable.)
  3. Work both forward and backward (what rules can you use on the sentences you've already got? What rules might get your final conclusion from some intermediate step?)
  4. If you don't see anything else to do, try ¬Intro.

Last update: February 13, 2013.
Curtis Brown | Symbolic Logic | Philosophy Department | Trinity University
cbrown@trinity.edu