General strategy for constructing a proof
1. Working forward:
(a) Consider a sentence you already have to work with (either as a premise or as
something you've proved already).
(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.).
(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 as an intermediate
step. That becomes a new goal to work toward.
3. If all else fails, try negation intro.
4. If you've derived a new line, or you've made an assumption to get a subproof going, repeat #1 for that line.
5. If you see a good way to get the conclusion if you could get an intermediate step, repeat #2 for the intermediate step.
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 can't prove either disjunct separately). 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 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.
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.
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.