Proof Strategy

Reading the Proof Off the Goal

Knowing the rules does not tell you which to apply. Strategy does, and the central insight is that the shape of the goal dictates the method.

Working backwards from the goal is almost always more productive than working forwards from the premises. Forward reasoning generates whatever the rules happen to allow, most of which is irrelevant; backward reasoning generates only what would actually help.

Indirect proof, assume the negation of the goal and derive a contradiction, is the universal fallback, available whatever the goal looks like. It is often the only route when the goal is atomic, since an atom has no connective to guide you.

Subproofs nest, and the nesting has a strict discipline: an inner subproof may use lines from any subproof still open around it, but never from one already closed. Depth is often necessary, proving $P \rightarrow (Q \rightarrow R)$ requires two nested assumptions, one for each conditional.

Several derived rules are provable from the basic ones and then used freely as shorthand:

• Modus tollens: from $P \rightarrow Q$ and $\neg Q$, infer $\neg P$
• Hypothetical syllogism: from $P \rightarrow Q$ and $Q \rightarrow R$, infer $P \rightarrow R$
• Disjunctive syllogism: from $P \vee Q$ and $\neg P$, infer $Q$
• Contraposition: $P \rightarrow Q$ is equivalent to $\neg Q \rightarrow \neg P$

Derived rules add no power, anything provable with them is provable without, but they shorten proofs enormously, which matters in practice.

Common pitfall: grinding forwards from the premises hoping the conclusion appears. It rarely does. Look at the goal first: a conditional goal tells you to assume its antecedent, and that single move often turns an intractable problem into a routine one.