Strategy for Proofs
1) Check whether there is a disjunctive statement among the premises. If so, set up your proof immediately for disjunction-elimination.
2) Work backwards as much as possible.
a. Identify a goal statement. (At first, the goal statement will be the conclusion.)
b. Identify the rule needed to get to the goal statement (use 3-6 below).
c. Put the sentences required by this use of the rule on your “wishlist.”
d. Repeat this process, using your “wishlist” statements as your new goal(s).
3) Check whether the goal appears as part of an assumption. If so, chances are you will be using the relevant elimination rule to reach the goal. If the goal is not part of an assumption, move on to 4.
a. If the goal is the consequent of a conditional, chances are good that you will be using horseshoe-elimination.
b. If the goal is part of a biconditional, chances are good that you will be using biconditional-elimination.
c. If the opposite of the goal appears in the assumptions, chances are good you will use a negation-rule.
d. If the goal is part of a conjunction, chances are good you will be using ampersand-elimination.
e. If the goal is part of a disjunction, chances are good you will be using disjunction-elimination.
In sum: For any binary
connective c, if the goal G is in a
sentence of the form P c
G, you will probably use the c-elimination rule to derive G. If the
opposite of the goal appears in the premises, use a negation rule.
4) If the goal is not part of an assumption and is non-atomic, identify the main connective of the goal. This will often indicate the introduction rule by which you will introduce the conclusion.
a. If horseshoe is the main connective, you will probably be using horseshoe-introduction—so prepare your proof accordingly (i.e. assume the antecedent in a subproof, plan to end the subproof with the consequent.)
b. If triple-bar is the main connective, you will probably be using triple-bar introduction—so prepare your proof accordingly (viz., as if you were going to introduce two horseshoe statements).
c. If negation is the main connective, you will probably be using negation-introduction—so prepare your proof accordingly (i.e. assume the opposite in a subproof, plan to end in a contradiction.)
d. If ampersand is the main connective, you will probably be using ampersand-introduction. So, put on your wishlist the two conjuncts.
e. If wedge is the main connective, you will probably be using wedge-introduction. Check your premises to see which disjunct looks most obtainable.
f. If none of the suggestions in 5 work out, do a proof by reductio ad absurdum. That is, assume the negation of the goal in a subproof and try to derive a contradiction. Then conclude the goal by negation elimination.
In sum: If a nonatomic goal is not part of an assumption, it usually will be derived by the introduction-rule for its main connective. Otherwise, it will be derived by reductio ad absurdum.
5) Rare case: If the goal is not part of an assumption but is atomic, try a proof by reductio ad absurdum. That is, assume the negation of the goal in a subproof and try to derive a contradiction. Then conclude the goal by negation elimination.
6) Proofs of theorems always begin with subproofs.
Additional Guidance:
EXTREMELY IMPORTANT!!!
NEVER start proving things at random. It is VERY unlikely you will solve the proof this way. If you’re tempted to do this, stop and regroup instead. Recall where you have been, where you want to go, and what you can use to get there. When working backwards, reidentify your goal and start again.