Here are some important things to keep in mind when doing proofs. These observations are all based on unproductive things I've noticed people have a tendency to do (and useful things they have a tendency not to do).
If you need to prove a conditional, identify the antecedent and consequent of the conditional that you want to prove. Set up a subproof with the antecedent as its assumption, and the consequent as its last line. Then get the conditional as the first step after the subproof, by Conditional Introduction. Make sure the assumption of the subproof is the antecedent of the conditional you are trying to prove, not the antecedent of some conditional you have as a premise or an earlier line!
On the other hand, 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 a subproof for each disjunct of the disjunction. The last line of every one of the subproofs should be the conclusion you are trying to reach. Then the first line after the subproofs will be the conclusion you reached as the last line of each subproof, by Disjunction Elimination.
Assume the opposite of what you want to prove. Derive a contradiction as the last line of the subproof. Get what you want by Negation Introduction as the first line after the subproof.
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.
As a general rule of thumb, if you have a proof in which all the premises are quantifier sentences (universals or existentials), and the conclusion is also a quantifier sentence, you will want to apply the various sorts of rules in the following order. (The general idea is (a) to do quantifier eliminations to get propositional formulas, then use the propositional rules, then use quantifier introduction rules to get back to quantifier statements, but this is complicated by (b) the need to use the rules that have more restrictions earlier than rules that have fewer restrictions so that you can use the same constants as often as possible.)
General Advice on Proofs
General Strategy for Constructing a Proof
1 - look at the premises and see whether any elimination rules apply (i.e. if you have a conjunction, you'll probably want to use conjunction Elim; if you have a disjunction, you'll probably want to use disjunction Elim; etc. One exception is that negation Elim is not useful on garden-variety negations, but only on double negations).
2 - look at the conclusion and see whether any intro rules would get you there (if the conclusion is a conjunction, it's usually easiest to derive the conjuncts separately and then use conjunction Intro to get the final conclusion; if the conclusion is a negation, it may be a good idea to try to get it by negation Intro. One exception: disjunction Intro is usually not the best way to derive a disjunction, because often you won't be able to prove the disjuncts separately.)
3 - if it looks like nothing else will work, try negation intro.
If you've derived a new line, or you've made an assumption to get a subproof going, repeat #1 for that line.
If you see a good way to get the conclusion if you could get an intermediate step, repeat #2 for the intermediate step.
Keep on going until, working forward from the premises and backward from the conclusion, the two chains of reasoning meet in the middle (hopefully!).
last update: November
Curtis Brown | Symbolic Logic | Philosophy Department | Trinity University