Proof Strategy: Working Backward
This video presents the same text shown beside it, spoken and on screen. It adds nothing the text does not say.
Working backward means reading the conclusion first and asking what single move would deliver it, then treating that requirement as a new goal, until the chain of requirements reaches the premises.
Premises: A horseshoe B, and B horseshoe C, and A. The goal is B dot C. Start at the goal. It is a conjunction, so the last line will be a conjunction move, which means both halves must already stand alone. Halve the problem: get B, and get C. Take B first. It is the consequent of the first premise, so modus ponens frees it if A is available — and A is a premise. That branch is settled before anything is written. Now C, the consequent of the second premise, freed by modus ponens if B is available, and B was reached a moment ago. Both halves are accounted for. Only now write the proof, top down: B from premises one and three, C from premise two and that new line, then the conjunction. The plan and the finished proof are one object read in opposite directions.
Working backward identifies what is needed; it does not license writing it down. A goal is not a line, and a line stating the conclusion because the plan called for it is an assertion rather than a derivation. The backward pass is planning, and the forward pass is the proof.
Builds on
Unlocks
- Nothing yet depends on this.