Posted: Apr 07, 2012 7:55 am
mizvekov wrote:I am curious though about how much our proofs differ.
So here's mine:

Code: Select all
`-- ⊢ P → Ptruth :: Theorem Stringtruth = 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 Stringlemma1 = 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 Stringmendelson = 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.