rationalskepticism.org

mizvekov wrote:I am curious though about how much our proofs differ.

So here's mine:

Code: Select all

-- ⊢ P → P
truth :: Theorem String
truth = let step1 = instL [p, p :=>: p] axiom1
            step2 = instL [p, p :=>: p, p] axiom2
            step3 = head $ mp step2 step1
            step4 = instL [p, p] axiom1 in
        head $ mp step3 step4

-- ⊢ ¬P → P → ⊥
lemma1 :: Theorem String
lemma1 = let step1 = UseTheorem (instL [Not p, Not f] axiom1)
             step2 = Assume (Not p)
             step3 = MP step1 step2
             step4 = matchMP axiom3 step3
         in verify step4

-- ⊢ (¬P → Q) -> (¬P → ¬Q) → P
-- This is Mendelson's axiom3.
mendelson :: Theorem String
mendelson = let step1  = Assume (Not p :=>: Not q)
                step2  = Assume (Not p :=>: q)
                step3  = Assume (Not p)
                step4  = MP step1 step3
                step5  = MP step2 step3
                step6  = matchMP lemma1 step4
                step7  = MP step6 step5
                step8  = discharge (Not p) step7
                step9  = matchMP axiom3 step8
                step10 = UseTheorem (instL [q] truth)
                step11 = MP step9 step10
                step12 = discharge (concl step2) step11
            in verify step12

My lemma isn't quite the same as yours. I basically introduced the notion of false (⊥ or f) as the negation of the tautology "P → P". But I can then easily use this to derive an arbitrary proposition.

Oh, it's a shame I haven' t yet read that book, I definitely should have and there are no excuses.

It's definitely going on my reading list if I ever land a C++ job. I'm thinking I'll go through Scott Meyers again, and then probably Sutter and Coplien too.