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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
