Solving alethic modal logic formulas using truth trees

Question

Disclaimer: this first section is about alethic modal logic and truth trees. It's important to the question but significant parts of the code can probably be reviewed without it. You're welcome to skip ahead.

Alethic Modal Logic

For those who don't know, alethic modal logic is a superset of propositional logic enhanced with the necessity and possibility operators. Given a set of possible worlds, modal logic can express that a formula is true at all worlds as it is necessary that and that a formula is true at at least one world as it is possible that.

Truth Trees

A nice way to prove that a modal formula is always true is by using truth threes. If you don't feel like watching the video (as well as some follow-up videos) linked, here's a quick rundown of how it works:

In order to prove a formula always hold, given a set of axioms, you negate the formula and then apply a set of rules determined by the set of axioms and try to reduce the formula to a contradiction. If some branch does not result in a contradiction, the negated formula is true for some choice of primitive propositions and the original function is not necessarily true.

In modal logic (System K) there are the following rules:

• ¬¬f -> add f to the current branch in the current world
• f&g -> add f and g to the current branch in the current world
• ¬(f&g) -> make two branches, add ¬f to one, ¬g to the other
• ◇f (possibility) -> create a new world and add f to that world
  • also add all gs so that □g (necessity) at the current branch in the current world

When you add axiom T, the possibility relationship become reflexive, hence:

• ◇f -> add f to the current branch in the current world

All other formulas can be reduced to one of the above, as it is done in the formulaType function.

---

Code Explanation

I have implemented a (rather naive) version of modal truth trees in Haskell which I would like to have reviewed. Here's what you'll find in the code below along with some of my concerns and questions:

ModalFormula

This is the data type representing a modal formula. I've used TypeOperators to make it possible to write the formulas in a more or less natural way. I've also refrained from making it a type class because I felt like that would make it a lot easier to pattern match against them, but that may have been a mistake.

FormulaType

This represents the basic types of formulas that all formulas can be reduced to. In hindsight, I'm not terribly happy with this, since it seems like these types depend on the system of axioms you choose.

the function formulaType constructs these objects based on a ModalFormula.

World

This represents a possible world. It contains primitive functions that hold true at that world as well as formulas that are necessary and possible at that world and finally pairs of formulas, one of which is true. There are no other formulas, since those get deconstructed the moment they are added.

I'm not very pleased that I'm not using the type system to ensure that primitives only contains primitive propositions and their negations. I feel like it night be possible using GADT's or type classes, but it might not be worth the effort.

addPrimitrive function and friends

These four functions add the formulas as one of the four types to the world and return the result. They use lenses, which I added in later, so the three last functions are trivially straightforward (might not be worth having as a function).

The addPrimitive function has an additional use: it returns Nothing if the resuting world would be inconsistent. It might be better to extract that functionality, but it felt natural to implement it like this.

FormulaAdder

FormulaAdders are functions that add a formula to a world accoring to a set of axioms. baseAdd and addAll implement the basic functionality and addK and addT enhance an adder with axiom K and T respectively.

k and t are FormulaAdders that correspond to system K and System T respectively, created by composing FormulaAddders that correspond to axioms and passing the result to baseAdder

prove and satisfiable

The prove function is pretty straightforward if the implementation of satisfiable is given. It constructs an world containing the negation of the formula that is to be proven and checks whether that world is satisfiable.

I'm not very pleased that I have to repeat explicitly add the negated formula at this point and deal with the returned world possibly being Nothing here, maybe there's a nicer way to do this.

The satisfiable function recursively calls itself and tries to evaluate all formulas in the world until it encounters an inconsistent world.

The implementation of this function might be a bit complex and possibly should have been split up more or written on more lines.

General concerns

• I might have gone overboard on trying to write code using point-free style
  • is it too much?
  • could some of it have been written better still using point-free style?
• I've used view patterns where it seemed fitting but might have gone overboard there as well
  • is my use of view patterns readable?
• Did I miss some really cool features of Haskell that could have made this code more elegant?
• Unless it's really, really bad, I'm not very interested in performance

The Code

Without further ado, here's the code:

{-# Language TypeOperators, ViewPatterns, TemplateHaskell #-}

-- Contains data stuctures to represent alethic modal logic formulas
-- and functions to prove these formulas in system K and T.
module ModalLogic (
    ModalFormula(..), prove, neg,
    FormulaAdder,
    World, emptyW, k, t
) where

import Data.Maybe
import Control.Lens
import Data.Set (Set, insert, empty, deleteFindMax, toList)
import Control.Monad ((>=>))

-- The infix TypeOperators to construct modal formulas.
infixl 6 :<=>
infixl 7 :=>
infixl 8 :|
infixl 9 :&

-- a modal formula
data ModalFormula = P Int | Q Int
                  | Not ModalFormula | Nec ModalFormula | Pos ModalFormula
                  | ModalFormula :& ModalFormula | ModalFormula :| ModalFormula
                  | ModalFormula :=> ModalFormula | ModalFormula :<=> ModalFormula
    deriving (Show, Read, Eq, Ord)

-- the type of a formula with regards to how it acts in a truth three 
data FormulaType = Primitive ModalFormula
                 | Branching (ModalFormula, ModalFormula)
                 | Possibility ModalFormula
                 | Necessity ModalFormula
                 | Multiple [ModalFormula]

-- a possible world
data World = World { _primitives    :: Set ModalFormula,
                     _branching     :: Set (ModalFormula, ModalFormula),
                     _possibilities :: Set ModalFormula,
                     _necessities   :: Set ModalFormula }
    deriving Show
makeLenses ''World

-- a possible world with no formulas in it
emptyW :: World
emptyW = World empty empty empty empty

-- the negation of a given formula
neg :: ModalFormula -> ModalFormula
neg (Not f) =     f
neg      f  = Not f

-- adds a primitive expression (a primitive or its negation) to a world
-- returns Nothing if the resulting World is inconsistent
addPrimitive :: ModalFormula -> World -> Maybe World
addPrimitive f ((neg f `elem`) . view primitives -> True) = Nothing
addPrimitive f w = Just . (primitives %~ (insert f)) $ w

-- adds a branch to a world
addBranching :: (ModalFormula, ModalFormula) -> World -> World
addBranching f = branching %~ (insert f)

-- adds a possiblitily to a world
addPossibility :: ModalFormula -> World -> World
addPossibility f = possibilities %~ (insert f)

-- adds a necessity to a world
addNecessity :: ModalFormula -> World -> World
addNecessity f = necessities %~ (insert f)   

-- a function that adds a formula to a world according to certain rules
-- corresponds to a system in logic
type FormulaAdder = ModalFormula -> World -> Maybe World

-- adds all formulas in a list to a world using a given FormulaAdder
addAll :: FormulaAdder -> [ModalFormula] -> World -> Maybe World
addAll a fs =  flip (foldr $ (=<<) . a) fs . Just

-- adds basic rules to a FormulaAdder
-- use this to construct a FormulaAdder
baseAdd :: FormulaAdder -> FormulaAdder
baseAdd _ (formulaType -> Primitive f)        = addPrimitive f
baseAdd _ (formulaType -> Branching t@(f, g)) = Just . addBranching t
baseAdd a (formulaType ->  Multiple fs)       = addAll (baseAdd a) fs
baseAdd a f = a f

---- Axioms ----
-- pass these or a composition of these to baseAdd

-- adds Possibility and Necessity to a FormulaAdder
addK :: FormulaAdder -> FormulaAdder
addK _ (formulaType -> Possibility f) = Just . addPossibility f
addK _ (formulaType -> Necessity   f) = Just . addNecessity f
addK _ _ = Just . id

-- adds Reflexivity to a FormulaAdder
addT :: FormulaAdder -> FormulaAdder
addT a (formulaType -> Necessity f) = baseAdd a f
addT _ _ = Just . id

-- composes two FormulaAdders imto one that applies all rules
comp :: FormulaAdder -> FormulaAdder -> FormulaAdder
comp a1 a2 f = a1 f >=> a2 f

-- FormulaAdder corresponding to System K
k = baseAdd $ addK k
-- FormulaAdder corresponding to System T
t = baseAdd $ comp (addK t) (addT t)

-- converts a modal formula in a basic formula type
formulaType :: ModalFormula -> FormulaType
-- primitive
formulaType f@     (P _)  = Primitive f
formulaType f@     (Q _)  = Primitive f
formulaType f@(Not (P _)) = Primitive f
formulaType f@(Not (Q _)) = Primitive f
-- neccesity
formulaType      (Nec f)  =   Necessity       f
formulaType (Not (Nec f)) = Possibility $ neg f
-- possibility
formulaType      (Pos f)  = Possibility       f
formulaType (Not (Pos f)) =   Necessity $ neg f
-- conjunction
formulaType      (f :| g)  = Branching (f, g)
formulaType (Not (f :| g)) = formulaType $ neg f :& neg g
-- disjunction
formulaType      (f :& g)  = Multiple [f, g]
formulaType (Not (f :& g)) = formulaType $ neg f :| neg g
-- implication
formulaType      (f :=> g)  = formulaType $ Not f :|     g
formulaType (Not (f :=> g)) = formulaType $     f :& Not g
-- equivalence
formulaType      (f :<=> g)  = formulaType $     (f :& g) :| (neg f :& neg g)
formulaType (Not (f :<=> g)) = formulaType $ (neg f :& g) :|     (f :& neg g)
-- double negation
formulaType (Not (Not f)) = formulaType f  

-- returns true if a modal formula is provable in a given system (FormulaAdder)
prove :: FormulaAdder -> ModalFormula -> Bool
prove a = not . fromMaybe False . fmap (satisfiable a) . flip a emptyW . Not

-- splits a Set in a single elements and the rest if possible
sMaxRest :: Ord a => Set a -> Maybe (a, Set a)
sMaxRest ((==empty) -> True) = Nothing
sMaxRest s = Just $ deleteFindMax s

-- returns true if a given world is satisfiable in a given system (FormulaAdder)
satisfiable :: FormulaAdder -> World -> Bool
-- apply branching rules first
satisfiable a 
            w@(sMaxRest . view branching -> Just ((f, g), bs)) 
                = let newWorld = (branching .~ bs $ w) in
                  -- a world is satifiable if any of its branches is satisfiable
                  any (fromMaybe False) . map (fmap (satisfiable a) . flip a newWorld ) $ [f, g]
-- apply possibilities next
satisfiable a 
            w@(sMaxRest . view possibilities -> Just (f, fs))
                      -- all neccesities must be true in every possible world
                = let createdWorld =  addAll a (toList (insert f (_necessities w))) emptyW
                      newWorld = (possibilities .~ fs $ w) in
                  -- both the current world and the created world must be satisfiable
                  all (fromMaybe False) . map (fmap (satisfiable a)) $ [Just newWorld, createdWorld]
-- a world is satisfiable if there are no more rules left to apply
satisfiable _ _ = True

Answer 1

sMaxRest is maxView.

hlint points out some redundant brackets and suggests using maybe in prove.

addPossibility, addBranching and addNecessity are superfluous once-used one-liners.

All the World passing can be abstracted with the State monad. For example, addAll becomes traverse_ (I assume reversing the order of adding does no harm) and can be inlined. And Sets are Traversable, so no need for toList. And comp becomes liftA2 (>>) and can be inlined. (I note these because it might otherwise look like I'm rewriting the code from scratch as opposed to reviewing.)

{-# Language TypeOperators, ViewPatterns, TemplateHaskell, FlexibleContexts, RankNTypes #-}

-- Contains data stuctures to represent alethic modal logic formulas
-- and functions to prove these formulas in system K and T.
module ModalLogic (
    ModalFormula(..), prove, neg,
    FormulaAdder,
    World, emptyW, k, t
) where

import Data.Maybe
import Control.Lens
import Data.Set (Set, insert, maxView)
import qualified Data.Set as S
import Control.Monad ((>=>))
import Control.Monad.State
import Control.Applicative
import Data.Foldable (traverse_, asum)

-- The infix TypeOperators to construct modal formulas.
infixl 6 :<=>
infixl 7 :=>
infixl 8 :|
infixl 9 :&

-- a modal formula
data ModalFormula = P Int | Q Int
                  | Not ModalFormula | Nec ModalFormula | Pos ModalFormula
                  | ModalFormula :& ModalFormula | ModalFormula :| ModalFormula
                  | ModalFormula :=> ModalFormula | ModalFormula :<=> ModalFormula
    deriving (Show, Read, Eq, Ord)

-- the type of a formula with regards to how it acts in a truth three 
data FormulaType = Primitive ModalFormula
                 | Branching (ModalFormula, ModalFormula)
                 | Possibility ModalFormula
                 | Necessity ModalFormula
                 | Multiple [ModalFormula]

-- a possible world
data World = World { _primitives    :: Set ModalFormula,
                     _branching     :: Set (ModalFormula, ModalFormula),
                     _possibilities :: Set ModalFormula,
                     _necessities   :: Set ModalFormula }
    deriving Show
makeLenses ''World

-- a possible world with no formulas in it
emptyW :: World
emptyW = World S.empty S.empty S.empty S.empty

-- the negation of a given formula
neg :: ModalFormula -> ModalFormula
neg (Not f) =     f
neg      f  = Not f

-- adds a primitive expression (a primitive or its negation) to a world
-- returns Nothing if the resulting World is inconsistent
addPrimitive :: ModalFormula -> StateT World Maybe ()
addPrimitive f = do
  guard =<< gets ((neg f `notElem`) . view primitives)
  primitives %= insert f

-- a function that adds a formula to a world according to certain rules
-- corresponds to a system in logic
type FormulaAdder = ModalFormula -> StateT World Maybe ()

-- adds basic rules to a FormulaAdder
-- use this to construct a FormulaAdder
baseAdd :: FormulaAdder -> FormulaAdder
baseAdd _ (formulaType -> Primitive f)        = addPrimitive f
baseAdd _ (formulaType -> Branching t@(f, g)) = branching %= insert t
baseAdd a (formulaType ->  Multiple fs)       = traverse_ (baseAdd a) fs
baseAdd a f = a f

---- Axioms ----
-- pass these or a composition of these to baseAdd

-- adds Possibility and Necessity to a FormulaAdder
addK :: FormulaAdder -> FormulaAdder
addK _ (formulaType -> Possibility f) = possibilities %= insert f
addK _ (formulaType -> Necessity   f) = necessities   %= insert f
addK _ _ = pure ()

-- adds Reflexivity to a FormulaAdder
addT :: FormulaAdder -> FormulaAdder
addT a (formulaType -> Necessity f) = baseAdd a f
addT _ _ = pure ()

-- FormulaAdder corresponding to System K
k :: FormulaAdder
k = baseAdd $ addK k
-- FormulaAdder corresponding to System T
t :: FormulaAdder
t = baseAdd $ (>>) <$> addK t <*> addT t

-- converts a modal formula in a basic formula type
formulaType :: ModalFormula -> FormulaType
-- primitive
formulaType f@     (P _)  = Primitive f
formulaType f@     (Q _)  = Primitive f
formulaType f@(Not (P _)) = Primitive f
formulaType f@(Not (Q _)) = Primitive f
-- neccesity
formulaType      (Nec f)  =   Necessity       f
formulaType (Not (Nec f)) = Possibility $ neg f
-- possibility
formulaType      (Pos f)  = Possibility       f
formulaType (Not (Pos f)) =   Necessity $ neg f
-- conjunction
formulaType      (f :| g)  = Branching (f, g)
formulaType (Not (f :| g)) = formulaType $ neg f :& neg g
-- disjunction
formulaType      (f :& g)  = Multiple [f, g]
formulaType (Not (f :& g)) = formulaType $ neg f :| neg g
-- implication
formulaType      (f :=> g)  = formulaType $ Not f :|     g
formulaType (Not (f :=> g)) = formulaType $     f :& Not g
-- equivalence
formulaType      (f :<=> g)  = formulaType $     (f :& g) :| (neg f :& neg g)
formulaType (Not (f :<=> g)) = formulaType $ (neg f :& g) :|     (f :& neg g)
-- double negation
formulaType (Not (Not f)) = formulaType f  

-- returns true if a modal formula is provable in a given system (FormulaAdder)
prove :: FormulaAdder -> ModalFormula -> Bool
prove a f = isNothing $ evalStateT (a (Not f) >> satisfiable a) emptyW

-- returns true if a given world is satisfiable in a given system (FormulaAdder)
satisfiable :: FormulaAdder -> StateT World Maybe ()
satisfiable a = join
   $  handleBranching   <$> zoom branching     (StateT maxView)
  <|> handlePossibility <$> zoom possibilities (StateT maxView)
  <|> pure (pure ()) where
  -- a world is satifiable if any of its branches is satisfiable
  handleBranching (f, g) = (a f >> satisfiable a) <|> (a g >> satisfiable a)
  -- both the current world and the created world must be satisfiable
  handlePossibility f = do
    ns <- uses necessities $ insert f
    satisfiable a
    put emptyW
    -- all neccesities must be true in every possible world
    traverse_ a ns
    satisfiable a

Shouldn't the current world automatically be satisfiable if the created one is? Or is this one of the things nonstandard FormulaAdders might change? FormulaType and formulaType look like they ought to be removed and inlined respectively, but I'm not sure how to keep lines where you use formulaType from duplicating.