This module defines the type of theorems and the primitive inference rules. > module Theorem(Theorem, hyp, concl, just, assume, disch, mp, > conj_intro, conj_elim, > disj_intro, disj_elim, > neg_intro, neg_elim, > module Term, module Monad) where > import Term > import List > import Monad > newtype Theorem = T {thm :: ([Term],Term)} > deriving Eq A theorem is an ordered pair of: - a list of hypotheses/assumptions, used as a set - the conclusion/consequence Discussion: We are hiding the internal representation of Theorem. As a result, any caller to this module cannot create their own theorems randomly, but must use our primitive inference rules to obtain new theorems. (Of course, they can write their inference rules, but those have to call ours.) This is how we prevent faulty logic. In other words, we reduce proof verification to type checking --- you aren't proving anything until you obtain a Theorem. This idea comes from HOL. Pretty-printing a theorem (in the Show framework of Haskell.) The assumption list and the conclusion are separated by the turnstile symbol "|-". > instance Show Theorem where > showsPrec _ (T (hs,c)) = showsPrec 0 hs . showString " |- " . showsPrec 0 c Auxilliary functions to extract the hypotheses and the conclusion of a theorem. > hyp = fst . thm > concl = snd . thm Now our primitive inference rules. They are basically from natural deduction. Convention: for inferences that may fail, the result type is Maybe t, where t is the result of success. We then make use of the monadic status of Maybe to simplify error handling in sequences of inference rules. There are some examples in module Inference of using these inference rules to build more interested inference rules; they also illustrate how the Maybe monad helps us handle (and ignore) errors. We could use the Either type instead of the Maybe type. Advantage: it can store the reason of failure when an inference rule fails. First, a helper function that extracts the successful value of a Maybe value. (It aborts if the Maybe value is a failure.) > just :: Maybe a -> a > just = maybe (error "inference error") id Assumption introduction: for any term t, we have t |- t > assume :: Term -> Theorem > assume t = T ([t],t) Discharge, aka ==> introduction: from A,t |- u deduce A |- t ==> u > disch :: Term -> Theorem -> Theorem > disch term thm@(T(hs,c)) = T(delete term hs, Imp term c) Modus ponens, aka ==> elimination: from A1 |- t ==> u A2 |- t deduce A1 u A2 |- u > mp :: Theorem -> Theorem -> Maybe Theorem > mp (T(h1,c1)) (T(h2,c2)) > | isImp c1 && sub1 c1 == c2 = Just (T(h1 `union` h2, sub2 c1)) > | otherwise = Nothing && introduction: from both A1 |- t A2 |- u deduce A1 u A2 |- t && u > conj_intro :: (Theorem,Theorem) -> Theorem > conj_intro (T(h1,c1), T(h2,c2)) = T(h1 `union` h2, Conj c1 c2) && elimination: from A |- t && u deduce both A |- t A |- u > conj_elim :: Theorem -> Maybe (Theorem,Theorem) > conj_elim (T(h, Conj c1 c2)) = Just (T(h,c1), T(h,c2)) > conj_elim t = Nothing || introduction: given a term, from A |- t deduce both A |- t || term A |- term || t > disj_intro :: Term -> Theorem -> (Theorem,Theorem) > disj_intro term (T(h,c)) = (T(h, Disj c term),T(h, Disj term c)) || elimination, aka case analysis: from A |- x || y and both A1,x |- z A2,y |- z deduce A u A1 u A2 |- z the terms x and y are removed from A u A1 u A2. > disj_elim :: Theorem -> (Theorem,Theorem) -> Maybe Theorem > disj_elim (T(a, Disj t1 t2)) (T(a1,c1), T(a2,c2)) > | c1 == c2 && > t1 `elem` a1 && > t2 `elem` a2 = Just (T(a `union` (delete t1 a1) `union` (delete t2 a2), > c1)) > | otherwise = Nothing > disj_elim _ _ = Nothing ~ introduction, aka reductio ad absurdum: given term x, from A,x |- y && ~y deduce A |- ~x > neg_intro :: Term -> Theorem -> Maybe Theorem > neg_intro x (T(as,Conj y1 (Neg y2))) > | y1 == y2 && x `elem` as = Just (T(delete x as, Neg x)) > | otherwise = Nothing > neg_intro _ _ = Nothing ~ elimination, which is reductio ad absurdum dualized: given term ~x, from A,~x |- y && ~y deduce A |- x We need both versions of reductio ad absurdum because no other inference rules let us deduce a|-~~a or ~~a|-a. > neg_elim :: Term -> Theorem -> Maybe Theorem > neg_elim nx@(Neg x) (T(as,Conj y1 (Neg y2))) > | y1 == y2 && nx `elem` as = Just (T(delete nx as, x)) > | otherwise = Nothing > neg_elim _ _ = Nothing