I used a set of natural language statements and their formalization from Gries and Schneider. I attempted to transform the propositions into Haskell equations. For example, for S0 : $a \land w \Rightarrow p$ the conjunction was split giving $a \Rightarrow p$ and $w \Rightarrow p$ and then the contrapositive rule was applied giving $\neg p \Rightarrow \neg a$ and $\neg p \Rightarrow \neg w$. I then translated those propositions into Haskell conditional equations.
Is the Haskell representation a reasonable transformation? Is there a relation between the execution of the Haskell expression
not e a proof of theorem $\neg e$?
If Superman were able and willing to prevent evil, he would do so. If Superman were unable to prevent evil, he would be ineffective; if he were unwilling to prevent evil, he would be malevolent. Superman does not prevent evil. If Superman exists, he is neither ineffective nor malevolent. Therefore Superman does not exist.
$a$: Superman is able to prevent evil.
$w$: Superman is willing to prevent evil.
$i$: Superman is ineffective.
$m$: Superman is malevolent.
$p$: Superman prevents evil.
$e$: Superman exists.
S0 : $a \land w \Rightarrow p$
S1 : $(\neg a \Rightarrow i) \land (\neg w \Rightarrow \neg m)$
S2 : $\neg p$
S3 : $e \Rightarrow \neg i \land \neg m$
module SUPERMAN where a::Bool w::Bool i::Bool p::Bool e::Bool a | (not p) = False -- S0a w | (not p) = False -- S0b i | (not a) = True -- S1a m | (not w) = True -- S1b p = False -- S2 e | (i || m) = False -- S3 -- Theorems (not e), (i || m), and (i && a) all hold