Recipe

Plan a natural deduction proof

Use when: you have premises and a goal and must find a proof, not just check one

Goal: a complete proof whose last line is the goal at the outer level

Taught in Proof strategy

1. 1

   Identify the connective with the widest scope in the goal.

   Example

   In P \to (Q \to R) the main connective is the first \to; in \neg(P \vee Q) it is the \neg.

   Why: the introduction rule for that connective is the likeliest last line.

2. 2

   Write the goal at the bottom and open the subproofs its introduction rule needs.

   Example

   For P \to (Q \to R): a subproof from P to Q \to R, and inside it another from Q to R.

   • \wedge — two subgoals, one per conjunct.
   • \to or \leftrightarrow — one subproof per direction, assuming the left side and aiming for the right.
   • \neg — a subproof assuming the sentence inside the \neg, aiming for \bot.
   • \vee or a letter — no setup yet; go to Step 3.

   Why: each introduction rule has a fixed pattern, so it tells you what the proof above it must contain.

3. 3

   Apply elimination rules to the premises and open assumptions, choosing moves that approach the subgoal.

   Example

   With P and Q assumed and premise (P \wedge Q) \to R: \wedgeI gives P \wedge Q, then \toE gives R.

   • a disjunction you can use — set up \veeE with both cases aiming at the current subgoal.
   • a conditional whose antecedent you have — \toE.

   Why: elimination rules extract what the lines you have already contain.

4. 4

   When the subgoal is a letter or a disjunction and forward work has stalled, assume its negation and aim for \bot.

   Example

   From \neg(P \wedge \neg Q) and P, goal Q: assume \neg Q, build P \wedge \neg Q, clash with the premise, close with IP.

   Why: IP always applies, and the negated goal is a fresh line to reason with.

5. 5

   Close subproofs innermost first with their rules, and confirm the last line is the goal at depth 0.

   Why: a proof that ends inside a subproof still depends on an assumption.