Propositional logic.

Logic.lhs

> import Data.Set as S
> import Data.Map as M
> import Data.Maybe
> import Control.Monad (liftM, liftM2)

> import Test.QuickCheck

A statement is a sentence that is determinately true of determinately false independently of the circumstances in which it is used.

> data Proposition = Implies Proposition Proposition
>                  | And Proposition Proposition
>                  | Or Proposition Proposition
>                  | Not Proposition
>                  -- Sentence letter
>                  | Literal String

> instance Arbitrary Proposition where
>   arbitrary = frequency [(3, (liftM Literal) $ elements ["a", "b", "c", "d", "e"])
>                        , (1, (liftM Not) arbitrary)
>                        , (1, (liftM2 And) arbitrary arbitrary)
>                        , (1, (liftM2 Or) arbitrary arbitrary)
>                        , (1, (liftM2 Implies) arbitrary arbitrary)]

> instance Show Proposition where
>   show (Implies p q) = "(" ++ show p ++ " => " ++ show q ++ ")"
>   show (And p q) = "(" ++ show p ++ " & " ++ show q ++ ")"
>   show (Or p q) = "(" ++ show p ++ " | " ++ show q ++ ")"
>   show (Not p) = "-" ++ show p
>   show (Literal p) = p

> literals :: Proposition -> Set String
> literals (Literal s)   = S.fromList [s]
> literals (Not p)       = literals p
> literals (And p q)     = literals p `S.union` literals q
> literals (Or p q)      = literals p `S.union` literals q
> literals (Implies p q) = literals p `S.union` literals q

> type Assignment = Map String Bool

In general there are 2^n truth-assignments to n sentence letters.

> product :: [[a]] -> [[a]]
> product [] = [[]]
> product (x:xs) = concat [Prelude.map (y :) rest | y <- x] where rest = Main.product xs

> assignments :: Proposition -> [Assignment]
> assignments p = [M.fromList $ zip ls as | as <- Main.product $ replicate (length ls) [True, False]]
>   where
>       ls = S.toList $ literals p

> interpret :: Proposition -> Assignment -> Bool
> interpret (Literal s)   m = fromJust $ M.lookup s m
> interpret (Not p)       m = not $ interpret p m
> interpret (And p q)     m = interpret p m && interpret q m
> interpret (Or p q)      m = interpret p m || interpret q m
> interpret (Implies p q) m = if interpret p m then interpret q m else True

A truth-functional schema that comes out true under all interpretations of its sentence letters is said to be valid.

> isValid :: Proposition -> Bool
> isValid p = all (interpret p) (assignments p)

A truth-functional schema that comes out true under at least one interpretation is said to be satisfiable.

> isSatisfiable :: Proposition -> Bool
> isSatisfiable p = any (interpret p) (assignments p)

A truth-functional schema that comes out true under no interpretation is said to be satisfiable.

> isUnsatisfiable :: Proposition -> Bool
> isUnsatisfiable = not . isSatisfiable

A schema, p, implies another schema, q, if for all assignments that make p true, q is true.

> implies :: Proposition -> Proposition -> Bool
> implies p q = isValid $ Implies p q

> prop_ImplySelf p = implies p p

> prop_Commutativity p q r = implies p q && implies q r ==> implies p r

> prop_Valid p q = isValid p ==> implies q p

> prop_Unsatisfiable p q = isUnsatisfiable p ==> implies p q

> prop_Equality p q r = p == q && q == r ==> p == r
> prop_Equality2 p q  = p == q ==> q == p
> prop_Equality3 p q  = isValid p && p == q ==> isValid q

For instance, -p implies -(p.q).

> testProp2 = implies (Not (Literal "p")) (Not (And (Literal "p") (Literal "q")))

But, p does not imply q.

> testProp3 = implies (Literal "p") (Literal "q")

Equivalence is mutual implication.

> instance Eq Proposition where
>   p == q = implies p q && implies q p

> testProp = And (Literal "a") (Literal "b")
> testAssign = M.fromList [("a", True), ("b", False)]