Now you build proofs yourself. You know the eight rules of inference and how to justify a line (Justifying Proof Lines). The question is which line to write next.
Key idea
Keep the conclusion in view. Look for it inside the premises, then ask which rule could produce it and what that rule needs. Write only lines that move you toward the conclusion.
Why it works
From any set of premises you could derive endless lines: by Add alone, $p \lor q$, $p \lor r$, $(p \lor q) \lor s$ and so on. Most are useless. A proof is a search, and the conclusion tells you where to search. If the conclusion is the consequent of a premise, you need that premise's antecedent; if it is a conjunct, you need the conjunction; if it is a disjunct, you need the negation of the other disjunct.
Worked examples
Worked example: A three-line proof
Premises: $p \to q$, $r \land \neg q$. Prove $\neg p \land r$.
- The conclusion is a conjunction, so get each conjunct and use Conj.
- $\neg p$: MT needs $\neg q$. Get it by Simp 2 (line 3: $\neg q$).
- Line 4: $\neg p$ by MT 1, 3.
- Line 5: $r$ by Simp 2.
- Line 6: $\neg p \land r$ by Conj 4, 5.
Answer: Done in four new lines.
Worked example: Missing line
Premises: $p \lor q$, $\neg p$, $q \to s$. Lines: 4. ?, DS 1, 2; 5. $s$, MP 3, 4. What is line 4?
- DS on line 1 with $\neg p$ gives the other disjunct.
Answer: $q$
Worked example: Using Add
Premises: $p$, $(p \lor q) \to r$. Prove $r$.
- $r$ is the consequent of premise 2; MP needs $p \lor q$.
- Line 3: $p \lor q$ by Add 1.
- Line 4: $r$ by MP 2, 3.
Answer: Done.
Common mistake
Writing down every line you can infer and getting lost. A proof with twenty wandering lines is hard to finish and hard to check. Start from the conclusion: find it in the premises, name the rule that would free it, and make the next goal whatever that rule needs.
It also helps to read the premises once before writing anything. Mark which ones are conditionals (they want MP or MT), which are disjunctions (DS or CD), and which are conjunctions (Simp). Often the shapes alone show the path: a conjunction gets split, its parts feed a conditional, and the result is the conclusion.
If you get stuck in the builder above, delete your last line and try the step you planned backward from the conclusion.
- Where is the conclusion in the premises?
- Which rule would produce it?
- What does that rule need, and do I have it?
- If not, make that the new goal and repeat.