Capstone: A Mixed-Strategy Proof

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.

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.