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

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

• Is there an important reason to use Haskell? You might find it helpful if I point you to Prolog for these kind of tasks. – Sandro Lovnički Dec 21 '18 at 22:56
• @SandroLovnički I am researching specific claims made about Haskell and proofs e.g. an earlier question – Patrick Browne Dec 22 '18 at 0:40
• Haskell is a programming language, not a proof assistant / theorem prover, or a system for automated reasoning over logical theories. At most, given boolean values for variables, it can compute boolean expressions, essentially applying truth tables, like most programming languages can. – chi Dec 22 '18 at 9:15
• @chi So the relation between the execution and a proof is that with Haskell (or other language) we can compute a truth table? Is this TT a model or interpretation of the original propositions? – Patrick Browne Dec 22 '18 at 9:54

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.
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.