[Haskell-cafe] Re: Propositional logic question
apfelmus
apfelmus at quantentunnel.de
Tue Jun 26 04:45:54 EDT 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
More information about the Haskell-Cafe
mailing list