A Theorem Prover for Intuitionistic Propositional Logic

One of the standard textbooks for ML, the "other" functional programming language, is Paulson's ML for the Working Programmer. Some years back, this is the book that I first learnt functional programming from. The book culminates in a theorem prover for classical first order logic, which is the kind of task that functional programming languages are ideally suited to. Recently I got interested in logic again, so I thought I'd write a theorem prover in Haskell, borrowing freely from the ML book.

(Note to Haskell fans: I have a soft spot for ML - it was my first - but somewhat to my surprise, I found that everything came out shorter and more readable in Haskell.)

There are several different approaches to computer theorem proving. The most powerful theorem provers are based on the resolution principle - which is the engine behind the Prolog programming language. However, the resolution principle is best suited to classical logic. A more flexible approach, which can more easily be used with other logics, is to use sequent calculus.

First of all, we need to understand some notation. We'll start with natural deduction. An inference rule is represented as a line with the premisses above the line and the conclusion below the line. For example, this rule

p   q
-----
 p&q

says that from p and q as premisses, we can conclude p&q. The idea is that you construct a proof tree by balancing applications of inference rules one on top of another.

However, natural deduction is a little unwieldy. The problem is that we sometimes prove things by making an assumption and seeing what happens. For example, to prove that p -> q, we could try assuming p, and seeing whether we can deduce q. The sequent calculus is a convenient way to handle these assumptions. If A is our set of assumptions, then we write
A |- p
to mean that p is provable assuming A. The |- is called the turnstile symbol. The inference rule we were after for implication is then

p |- q
-------
|- p->q

If we can prove q by assuming p, then we can conclude that p->q (with no assumptions)

A proof then consists of a tree, starting with axioms (things we know to be true) at the top, working down via our inference rules to the thing to be proved at the bottom. For example, here is a proof of p&q -> q&p

--------    --------  (Axiom)
p,q |- q    p,q |- p
--------    --------  (LeftConj)
p&q |- q    p&q |- p
--------------------  (RightConj)
     p&q |- q&p
   -------------  (RightImpl)
   |- p&q -> q&p

Starting at the top: It is certainly true that if you assume {p,q}, then q is provable (on the left), and likewise p (on the right). Next, on both sides, if something is provable assuming {p,q}, then it is provable assuming {p&q}. Next, on the assumption {p&q}, we have independently proved both q and p. From this we can deduce, on the same assumption, q&p. Finally, on the assumption p&q, we have proved q&p, from which we can deduce (with no assumption) p&q->q&p. The labels to the right of the lines are the names of the inference rules used at each step.

We're about ready to write some Haskell. Here are the data structures that we're going to need.

import List (delete, intersect)
import Maybe (isJust, fromJust)

data Prop = Atom String |       -- atomic propositions
            Conj Prop Prop |    -- conjunctions (logical AND)
            Disj Prop Prop |    -- disjunctions (logical OR)
            Impl Prop Prop      -- implications
            deriving Eq

data Sequent = Seq [Prop] [Prop]    -- Seq ps qs means ps |- qs

data Rule = Axiom | LeftConj | RightConj | LeftDisj | RightDisj | LeftImpl | RightImpl |
            LeftImplAtom | LeftImplConj | LeftImplDisj | LeftImplImpl deriving Show

data ProofTree = PT Sequent Rule [ProofTree]

A couple of comments:

First, when we introduced sequents, they always had a single proposition on the RHS of the turnstile symbol: A |- p meant p is provable from assumptions A. So why have we defined Sequent with a list of Prop for the RHS? The answer is that although intuitionistic logic allows just one proposition on the RHS, classical logic allows more than one. We're going to start with intuitionistic logic, but we might want to extend to classical logic later, so it's a good idea to plan ahead.

Second, ProofTree doesn't look like a tree datatype - it doesn't have separate Leaf and Branch variants. This is because we're going to represent leaf nodes by having the list of child nodes empty. This accords with the notation we used in the example proof tree, in which the axioms were shown below a line, with nothing above the line.

Next, we need some show functions, to output our datatypes in a readable way.

instance Show Prop where
    show (Atom p) = p
    show (Conj p q) = "(" ++ show p ++ "&" ++ show q ++ ")"
    show (Disj p q) = "(" ++ show p ++ "|" ++ show q ++ ")"
    show (Impl p q) = "(" ++ show p ++ "->" ++ show q ++ ")"

instance Show Sequent where
    show (Seq ps qs) = " " ++ unbracket (show ps) ++ " |- " ++ unbracket (show qs) ++ " "
        where unbracket cs = init $ tail cs  -- remove the "[" and "]"

instance Show ProofTree where
    show tree = showtree 0 tree
        where showtree i (PT sequent rule children) = concatMap (showtree (i+2)) children
                                                      ++ replicate i ' ' ++ show sequent ++ "    (" ++ show rule ++ ")\n"

Laying out a proof tree like the example I gave earlier would be hard work, so I've taken a short cut and decided to show the tree structure by indentation instead. Each node is shown on a separate line, with children above their parents, indented with respect to their parents. Basically, it'll look like an upside-down XML document.

> PT (Seq [] [Impl (Atom "p") (Atom "p")]) RightImpl [PT (Seq [Atom "p"] [Atom "p"]) Axiom []]
  p |- p    (Axiom)
 |- (p->p)    (RightImpl)

Finally, we'd like a more convenient way to input these datatypes. We could make use of a monadic parser library such as Parsec. However, I prefer to cheat, and piggy back on Haskell's own parser:

a = Atom "a"
b = Atom "b"
c = Atom "c"
p = Atom "p"
q = Atom "q"
r = Atom "r"

infixr 4 -->

p --> q = Impl p q

instance Num Prop where
    p + q = Disj p q
    p * q = Conj p q

ps |- qs = Seq ps qs

> a+b --> p*q
((a|b)->(p&q))
> [] |- [p-->p]
 |- (p->p)

I guess this might upset purists. The problem is that | and -> are already taken by Haskell syntax. However, the decision to use + and * for | and & makes more sense than it might appear at first. Under the Curry-Howard correspondence between intuitionistic logic and type theory, a&b corresponds to the product type a*b - (a,b) in Haskell - and a|b corresponds to the sum type a+b - Either a b in Haskell.

Good, we've got some datatypes, now we need to write some code to prove theorems. The basic approach is to start with the theorem to be proved as our goal. Given a goal, we first of all check whether it's an axiom. If it is then we're done. Otherwise, we try to use our inference rules to replace the goal by simpler subgoals, and then try to prove them recursively.

The first thing we need then, is some inference rules. The following are the rules for the system G3ip, a sequent calculus for intuitionistic propositional logic. (Note, I've missed out rules for negation.)

Axiom     --------  (p atomic)
          p,A |- p

          p,q,A |- r                               A |- p    A |- q
LeftConj  ----------                    RightConj  ----------------
          p&q,A |- r                                  A |- p&q

          p,A |- r    q,A |- r                      A |- p      A |- q
LeftDisj  --------------------          RightDisj  --------    --------
               p|q,A |- r                          A |- p|q    A |- p|q

          p->q,A |- p    q,A |- r                   p,A |- q
LeftImpl  -----------------------       RightImpl  ---------
                 p->q,A |- r                       A |- p->q

We need to encode these rules as tactics - given a goal, they should try to find a rule which can be applied, and generate subgoals. The way you apply a rule is that you find a match between the goal and the bottom of the rule - the subgoals are then given by the top of the rule. Let's write the code and look at some examples.

isAtom (Atom _) = True
isAtom _ = False

axiomG3ip (Seq as [p]) | isAtom p && p `elem` as = [([],Axiom)]
                       | otherwise               = []

leftConjG3ip (Seq as [r]) = zip [ [Seq (p : q : delete f as) [r]] | f@(Conj p q) <- as] (repeat LeftConj)

rightConjG3ip (Seq as [Conj p q]) = [ ( [Seq as [p], Seq as [q]], RightConj) ]
rightConjG3ip _ = []

leftDisjG3ip (Seq as [r]) = zip [ let as' = delete f as in [Seq (p:as') [r], Seq (q:as') [r]] | f@(Disj p q) <- as] (repeat LeftDisj)

rightDisjG3ip (Seq as [Disj p q]) = zip [ [Seq as [p]], [Seq as [q]] ] (repeat RightDisj)
rightDisjG3ip _ = []

leftImplG3ip (Seq as [r]) = zip [ [Seq as [p], Seq (q: delete f as) [r]] | f@(Impl p q) <- as] (repeat LeftImpl)

rightImplG3ip (Seq as [Impl p q]) = [ ( [Seq (p:as) [q]], RightImpl) ]
rightImplG3ip _ = []

> leftDisjG3ip $ [p+q,a+b] |- [r]
[([ p,(a|b) |- r , q,(a|b) |- r ],LeftDisj),([ a,(p|q) |- r , b,(p|q) |- r ],LeftDisj)]

The example says that if our goal is to show that assuming p|q and a|b, r is provable, then there are two ways to generate two subgoals - either by splitting the p|q or by splitting the a|b.

To make a theorem prover, what we need to do is, given a goal, use the tactics to generate candidate sets of subgoals. Then for a given set of subgoals, try to prove them recursively. Sometimes, this won't be possible, in which case we need to try a different set of subgoals. We'll use depth first search.

(f +++ g) x = f x ++ g x

tacticsG3ip = axiomG3ip +++ leftConjG3ip +++ rightConjG3ip +++ leftDisjG3ip +++ rightDisjG3ip +++ leftImplG3ip +++ rightImplG3ip

proof tactics sequent =
    let subtrees = [(subtree,rule) | (subgoal,rule) <- tactics sequent, subtree <- [map (proof tactics) subgoal], all isJust subtree]
    in if null subtrees
       then Nothing
       else let (subtree,rule) = head subtrees in Just (PT sequent rule (map fromJust $ subtree))

Let's try it out.

> proof tacticsG3ip ([] |- [p --> (q --> p)])
Just
    q,p |- p    (Axiom)
  p |- (q->p)    (RightImpl)
 |- (p->(q->p))    (RightImpl)
> proof tacticsG3ip ([] |- [p*(q+r) --> p*q+p*r])
Just
          q,p |- p    (Axiom)
          q,p |- q    (Axiom)
        q,p |- (p&q)    (RightConj)
      q,p |- ((p&q)|(p&r))    (RightDisj)
          r,p |- p    (Axiom)
          r,p |- r    (Axiom)
        r,p |- (p&r)    (RightConj)
      r,p |- ((p&q)|(p&r))    (RightDisj)
    p,(q|r) |- ((p&q)|(p&r))    (LeftDisj)
  (p&(q|r)) |- ((p&q)|(p&r))    (LeftConj)
 |- ((p&(q|r))->((p&q)|(p&r)))    (RightImpl)
> proof tacticsG3ip ([] |- [(a --> b) --> ((c --> a) --> (c --> b))])
ERROR - C stack overflow

Uh oh - what's gone wrong?

Well, it turns out that there's a problem with the set of rules that we chose. If you look again at the table of rules for G3ip, you'll see that there's something a little different about the left implication rule, compared to all the others. In every other rule, the sequents that you are asked to prove as subgoals are simpler than the goal itself. As a result, every time we apply a tactic, our subgoals become simpler, with the consequence that the search is guaranteed to terminate. With left implication however, this isn't true, with the consequence that we can get into infinite loops. Indeed, what's happening in our problem case is that after a couple of steps, we're getting into the following loop:

> leftImplG3ip $ [a-->b] |- [a]
[([(a->b) |- a,  b |- a],LeftImpl)]

Applying the left implication tactic to the goal a->b |- a generates the same goal as a subgoal.

There are several different approaches that can be taken to solve this. The simplest is just to limit the search depth.

proofDL tactics depth sequent =
    if depth == 0
    then Nothing
    else let subtrees = [(subtree,rule) | (subgoal,rule) <- tactics sequent, subtree <- [map (proofDL tactics (depth-1)) subgoal], all isJust subtree]
         in if null subtrees
            then Nothing
            else let (subtree,rule) = head subtrees in Just (PT sequent rule (map fromJust $ subtree))

> proofDL tacticsG3ip 10 $ [] |- [(a --> b) --> ((c --> a) --> (c --> b))]
Just
        c,(c->a),(a->b) |- c    (Axiom)
          a,c,(a->b) |- a    (Axiom)
          b,a,c |- b    (Axiom)
        a,c,(a->b) |- b    (LeftImpl)
      c,(c->a),(a->b) |- b    (LeftImpl)
    (c->a),(a->b) |- (c->b)    (RightImpl)
  (a->b) |- ((c->a)->(c->b))    (RightImpl)
 |- ((a->b)->((c->a)->(c->b)))    (RightImpl)

Another possibility would be to explicitly check for repetition of subgoals. I'm not going to pursue that here.

The third possibility is to see whether we can fix the rule that's causing the problem. It turns out that we can. The system G4ip has the same inference rules as G3ip, except that LeftImpl is replaced by four special cases:

                p,q,A |- r
LeftImplAtom  -------------  (p atomic)
              p->q,p,A |- r
       
              c->(d->b),A |- e
LeftImplConj  ----------------
               c&d->b,A |- e
       
              c->b,d->b,A |- e
LeftImplDisj  ----------------
               c|d->b,A |- e
       
              d->b,c,A |- d    b,A |- e
LeftImplImpl  -------------------------
                  (c->d)->b,A |- e

Of course, you should convince yourself that these inference rules are valid.

This leads to the following code:

leftImplAtomG4ip (Seq as [r]) = zip [ [Seq (q : delete f as) [r]] | f@(Impl p@(Atom _) q) <- as, p `elem` as] (repeat LeftImplAtom)

leftImplConjG4ip (Seq as [e]) = zip [ [Seq ((Impl c (Impl d b)) : delete f as) [e]] | f@(Impl (Conj c d) b) <- as] (repeat LeftImplConj)

leftImplDisjG4ip (Seq as [e]) = zip [ [Seq (Impl c b : Impl d b : delete f as) [e]] | f@(Impl (Disj c d) b) <- as] (repeat LeftImplDisj)

leftImplImplG4ip (Seq as [e]) = zip [ let as' = delete f as in [Seq (Impl d b : as') [Impl c d], Seq (b : as') [e]] | f@(Impl (Impl c d) b) <- as] (repeat LeftImplImpl)

tacticsG4ip = axiomG3ip +++ leftConjG3ip +++ rightConjG3ip +++ leftDisjG3ip +++ rightDisjG3ip +++ rightImplG3ip +++
              leftImplAtomG4ip +++ leftImplConjG4ip +++ leftImplDisjG4ip +++ leftImplImplG4ip

proofG4ip = proof tacticsG4ip

> proofG4ip $ [] |- [(a --> b) --> ((c --> a) --> (c --> b))]
Just
          b,a,c |- b    (Axiom)
        a,c,(a->b) |- b    (LeftImplAtom)
      c,(c->a),(a->b) |- b    (LeftImplAtom)
    (c->a),(a->b) |- (c->b)    (RightImpl)
  (a->b) |- ((c->a)->(c->b))    (RightImpl)
 |- ((a->b)->((c->a)->(c->b)))    (RightImpl)

So, we've written a theorem prover for intuitionistic propositional logic. The source is in Gentzen.hs. As a bonus, the source also contains code for the system G3cp for classical propositional logic.

One way to take the code forward would be to extend it to predicate logic - that is, allow variables, functions and quantifiers. Maybe I'll do that one day. However, at the moment I'm more interested in exploring the connection between intuitionistic logic and type theory. You see, the sequent
(a->b) |- ((c->a)->(c->b))
is actually saying something about types. It's saying that if you have a function f :: a->b, then you can make a function g :: (c->a)->(c->b). In fact it's easy:

g h = f . h

More next time.

Sources

Troelstra & Schwichtenberg, Basic Proof Theory, second edition
Dyckhoff, Contraction-Free Sequent Calculi for Intuitionistic Logic
Paulson, ML for the Working Programmer