Can this set of propositions be represented and proved in Haskell?

Question

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$?

Natural language

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.

Formalize

$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

Answer 1

Your Haskell encoding fails to capture proofs in propositional calculus (which is what the book you referred to does). The failure is not due to your using Haskell, but because of your encoding evaluation of Boolean values instead of proofs, and these are two completely different things.

When people speak about "Haskell proving things" they mean the following: given a type t which represents a proposition $T$ via the propositions as types translation, does there exists a Haskell program p of type t which corresponds to a proof of $T$?

Example: the proposition $((A \land B \Rightarrow C) \Rightarrow (A \Rightarrow B) \Rightarrow (A \Rightarrow C)$ corresponds to the (polymorphic) type ((a,b) -> c) -> (a -> b) -> (a -> c). The program \ f g x -> f (x, g x) has this type, and therefore corresponds to a proof of the proposition. The kind of logic that can be represented in this way is intuitionistic.

However, because Haskell has general recursion, not every Haskell program corresponds to a proof, and in fact Haskell cannot be considered as a proof system. It is a programming language. A better choice is Agda or Idris.

You are translating propositions into Boolean algebra which you then encode using the Haskell datatype Bool. You are therefore misusing the phrase "prove in Haskell". At best you are trying to evaluate Boolean expressions, which is not the same thing. You defined, in a somewhat convoluted way, a (partial) evaluation strategy that evaluates various Boolean propositions. It's not a very good one, for instance if you change p = True line to p = False, your program fails to evaluate a.

This has nothing whatsoever to do with Haskell because it is not specific to it. You can do the exact same thing in just about any programming language, and even in Excel. However, as was suggested already twice, prolog seems to be the most appropriate tool for the problem at hand. You are not "researching" Haskell here. I believe we already tried to explain this to you in the previous question you linked to. I hope it gets across this time.