General strategy for constructing a proof

1. Working forward:

(a) Consider each sentence you already have to work with (either as a premise or as something you've proved already) in turn.
(b) Identify the form of this sentence (e.g. negation, conjunction, etc.).
(c) Check whether you can apply the corresponding Elim rule (negation elim, conjunction elim, etc.).
(d) If so, the rule will tell you what to write next!

2. Working backward:

(a) Identify your current goal (either the final conclusion, or an intermediate step you would like to prove).
(b) Identify the form of this sentence (negation, conjunction, etc.).
(c) Check whether you can use the corresponding Intro rule (negation intro, conjunction intro, etc.) to obtain it.
(d) If you already have the justification steps you need to use the Intro rule to get your current goal, you're done!
(e) If you don't already have the justification steps you need to use the Intro rule, check to see what else you would need in order to use it, and tentatively write that down (near the bottom of your proof, just before the final conclusion and any other intermediate steps you have already written down) as a desired intermediate step. That becomes a new goal to work toward. (Writing it down at this stage is just wishful thinking, since you haven't proved it yet. But it's useful wishful thinking because it gives you a new goal to work toward.)

Note: there is no guarantee that working backward will be successful. If it doesn't work, backtrack and try something else! (See comment about vIntro below.)

3. If all else fails, try negation intro.

4. If you've derived a new line, or you've made an assumption to begin a subproof, repeat step 1 for that line.

5. If you write down an intermediate step (as you're working backward), repeat step 2 for that line.

Continue working forward from the premises and backward from the conclusion, until the two chains of reasoning meet in the middle (hopefully!).

Remarks on individual rules:

Disjunction Introduction

Normally this is not useful in a main proof (because usually the reason you are trying to prove a disjunction is that you don't have enough information to prove either disjunct separately). So working backward is not likely to be helpful when your current goal is a disjunction. You will more often be able to use vIntro in subproofs.

Disjunction Elimination

If you are using disjunction elimination, you need to look at a disjunction that you already have as a premise or an earlier line of the proof. Set up one subproof for each disjunct of the disjunction. The first line of the subproof should be the disjunct. The last line of every one of the subproofs should be exactly the same, namely whatever your current goal is. Then the first line after the subproofs will be the sentence you reached as the last line of each subproof, by Disjunction Elimination.

Negation Introduction

Assume the opposite of what you want to prove. (You must think backward here! Look at your goal and assume the opposite of that. Don't assume the opposite of something you already have!) Derive a contradiction as the last line of the subproof. Get what you want, i.e. the negation of your starting assumption, by Negation Introduction in the first line after the subproof.

Where does the contradiction come from? You'll need to use the Contradiction Intro rule, which means that you will need sentences of the form P and ~P on separate lines. Usually the best strategy is to look for a negation that you already have available (as a premise, assumption, or something you've already proved), and try to prove the opposite, i.e. the same thing without the negation. (So for instance if you already have ~(A v B), it would be a good idea to prove A v B in order to get your contradiction.) Normally you won't be able to prove the opposite of the assumption line of the subproof you are currently working on, so you will want to look elsewhere to find the sentence you want to prove the opposite of.

Subproofs in General

Never start a subproof unless you know what rule you are using it for, what the assumption should be, what the last line of the subproof should be, and what the first line after the subproof will be.

Last update: September 19, 2014.
Curtis Brown | Symbolic Logic | Philosophy Department | Trinity University
cbrown@trinity.edu