Skip to main content
SWStudyWalks Search

Logic / Unit 5   Logic 221 review, 2 to 3 minutes

Capstone: A Mixed-Strategy Proof

Captions available

The idea

This capstone plans a proof backward from its conclusion, then executes it forward with one discharge nested inside another, and closes by finding a much shorter route through the replacement rules.

In practice

Premises: tilde, open bracket, P dot Q, close bracket. And R horseshoe P. The goal is R horseshoe tilde Q. Plan it backward first. The goal is a conditional, so the outermost move will be a conditional proof: assume R, reach tilde Q. Inside that, tilde Q is a negation, and no premise offers it directly, so an indirect proof will be nested there: assume Q, reach a contradiction. Now execute forward. Line three: assume R, indenting. Line four: P, from lines two and three by modus ponens. Line five: assume Q, indenting a second time. Line six: P dot Q, from lines four and five by conjunction. Line seven: the conjunction of line six with premise one, an explicit contradiction, since line six asserts exactly what premise one denies. Line eight: tilde Q, discharging lines five through seven by indirect proof, and the inner fence closes. Line nine: R horseshoe tilde Q, discharging lines three through eight by conditional proof, and the outer fence closes. Now the shorter route. Premise one, by De Morgan, gives tilde P wedge tilde Q. That, by implication, gives P horseshoe tilde Q. Hypothetical syllogism with premise two gives R horseshoe tilde Q in three lines and no assumptions. Both proofs are valid, and the long one was not wasted — it is what the replacement route is doing underneath.

Where people slip

Nested discharges must close in the order they opened. Closing the outer scope while the inner one is still open produces a proof that reads correctly line by line and licenses a conclusion resting on an assumption nobody ever withdrew.

Your place on the trail

Every lesson rests on earlier ones and opens later ones. Tap any to jump.

Builds on

Unlocks

  • Nothing yet depends on this.

Something wrong in this lesson? Flag it  ·  Sources for Logic