[Haskell-cafe] Re: Propositional logic question

26 Jun 2007


      Eric wrote:
...
This seems rather complicated! What about this:
A => (B => C)
=      { X => Y   ==  ¬X \/ Y }
   ¬A \/ (¬B \/ C)
=      {associativity}
   (¬A \/ ¬B) \/ C
=      { DeMorgan }
   ¬(A /\ B) \/ C
=      { X => Y   ==  ¬X \/ Y }
   A /\ B   =>  C
E.
That works for classical logic where ¬A \/ A always holds, but the task
here is to prove it for intuitionistic logic.

Regards,
apfelmus