Philosophy 2340
Symbolic Logic

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

(Note: symbols will not display correctly unless you have the Lucida Sans Unicode font installed.)

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:

• proof by cases, and
• proof by contradiction (sometimes called reductio ad absurdum).

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.

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:

• ∧Intro (conjunction introduction)
• ∧Elim (conjunction elimination)
• ∨Intro (disjunction introduction)
• ∨Elim (disjunction elimination)

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

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

• Let's take the easy rule first. This is ¬Elim, which allows us to write down P if we already have ¬¬P.
  
• ¬Intro is trickier. It corresponds to the method of proof that Chapter 5 calls "Indirect Proof" or "Proof by Contradiction." (The same method is also often called "reductio ad absurdum.") 
  
  The general idea: if a sentence leads to a contradiction, it must not be true (so its negation must be true). So at the beginning of a ¬Intro  application, we have a sentence that we have not derived and whose negation we also have not derived. We want to establish that the negation of the sentence is true. So we start by assuming, for the sake of argument, the opposite of what we want to prove -- that is, if we want to prove ¬P, we start by assuming P. If we can derive a contradiction inside the subproof, then back in the main proof, we can infer that ¬P. The idea is that if P leads to a contradiction, then the negation of P must be true.
  
  What do we mean by "a contradiction"? Well, we will use the symbol ⊥ to represent a contradiction. So we need a ⊥Intro rule to allow us to write the symbol ⊥ on a line of our proof. ⊥Intro  works like this: if on earlier lines of our proof (or subproof) we have established any sentences one of which has the form P and the other of which has the form ¬P, then we can write down ⊥. Notice that P can itself be a compound sentence, so, for example, the sentences (Tet(a) ⋀ Large(b)) and ¬(Tet(a) ⋀ Large(b)) would work.
  
  We also have a ⊥Elim rule. This is strictly speaking unnecessary; we could always get the same results without it, but it speeds things up a bit in some circumstances. This rule allows us to write down anything we please once we've gotten ⊥. (This seems strange, but the general idea is that if the sentences you are working with are messed up enough to allow you to derive ⊥, then anything goes.)

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

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.