[Haskell-cafe] Re: Propositional logic question

[apfelmus]

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