Hilbert Systems

(Try this prover online!)

Most objections to computer-assisted proofs are themselves objectionable. However, one concern is valid: how can a program prove a theorem correctly if its source code is complex and therefore likely riddled with bugs?

Take the first proof of the four colour map theorem, which relied upon a one-off program written in IBM 370 assembly to tediously check numerous cases. Do we believe it did its job perfectly? Could there be, say, an off-by-one bug in some loop that causes it to skip a case that actually requires 5 colours?

How about our MESON prover for first-order logic? Are there really no bugs in our code?

The LCF theorem prover pioneered a solution to this problem: develop a core module that exports a few functions which provide the only ways to create theorems. These functions correspond to the laws of logic.

If this core module is correctly implemented, the rest of our program can be buggy, yet still produce only correct theorems because ultimately it is forced to obey the core’s rules of inference.

This is a proven approach in software engineering. For instance, a red-black tree module typically exports functions that maintain particular invariants, such as ensuring a tree is always approximately balanced and is a binary search tree. No matter how we call the exported functions, these invariants always hold.

Prelude

We write a theorem prover that our bootstrapped compiler can build.

We start with definitions that are normally at our fingertips thanks to Prelude:

▶ Toggle prelude

Terms, Formulas, Theorems

We define data types for terms and first-order formulas. This time, we avoid recursion schemes: our compiler can handle them, but lacks support for pattern synonyms and deriving Functor.

data Term = Var String | Fun String [Term] deriving Eq

data FO = Top | Bot | Atom String [Term]
  | Not FO | FO :/\ FO | FO :\/ FO | FO :==> FO | FO :<=> FO
  | Forall String FO | Exists String FO
  deriving Eq

A value of type Theorem should only exist if it contains a valid formula. Only functions corresponding to the rules of inference or axiom schema should be able to create Theorem values.

data Theorem = Theorem FO

Functions for pretty-printing:

instance Show Term where
  showsPrec _ = \case
    Var s -> (s ++)
    Fun s ts -> (s ++) . showParen (not $ null ts)
      (foldr (.) id $ intersperse (", "++) $ map shows ts)

instance Show FO where
  showsPrec p = \case
    Top -> ('1':)
    Bot -> ('0':)
    Atom s ts -> shows $ Fun s ts
    Not x -> ('~':) . showsPrec 4 x
    x :/\ y -> showParen (p > 3) $ showsPrec 3 x . (" /\\ " ++) . showsPrec 3 y
    x :\/ y -> showParen (p > 2) $ showsPrec 2 x . (" \\/ " ++) . showsPrec 2 y
    x :==> y -> showParen (p > 1) $ showsPrec 2 x . (" ==> " ++) . showsPrec 1 y
    x :<=> y -> showParen (p > 1) $ showsPrec 2 x . (" <=> " ++) . showsPrec 1 y
    Forall s x -> showParen (p > 0) $ ("forall " ++) . (s++) . (". "++) . showsPrec 0 x
    Exists s x -> showParen (p > 0) $ ("exists " ++) . (s++) . (". "++) . showsPrec 0 x

Rules and Axioms

We follow along chapter 6 of John Harrison’s 'Handbook of Practical Logic and Automated Reasoning'.

We need a helper function to determine if a given variable appears in a term:

occurs s t = s == t || case t of
  Var _ -> False
  Fun _ args -> any (occurs s) args

And another to determine if a given variable is free in a formula:

isFree t = \case
  Top -> False
  Bot -> False
  Atom _ ts -> any (occurs t) ts
  Not x -> isFree t x
  x :/\ y -> isFree t x || isFree t y
  x :\/ y -> isFree t x || isFree t y
  x :==> y -> isFree t x || isFree t y
  x :<=> y -> isFree t x || isFree t y
  Forall v x -> not (occurs (Var v) t) && isFree t x
  Exists v x -> not (occurs (Var v) t) && isFree t x

A dash of syntax sugar to make constructing equalities prettier in our code:

s =: t = Atom "=" [s, t]

The two rules of inference are modus ponens and generalization:

ponens (Theorem (p :==> q)) (Theorem p') | p == p' = Theorem q
gen x (Theorem t) = Theorem $ Forall x t

Now for the axioms (cf. Wikipedia’s article on Hilbert systems). Our propositional fragment is built from implication and falsehood, so we start with the S and K combinators, and the law of the excluded middle (LEM). Then we add a few rules for quantified variables and a few for equality.

axiomK p q        = Theorem $ p :==> (q :==> p)
axiomS p q r      = Theorem $ (p :==> (q :==> r)) :==> ((p :==> q) :==> (p :==> r))
axiomLEM p        = Theorem $ ((p :==> Bot) :==> Bot) :==> p
axiomAllImp x p q = Theorem $ Forall x (p :==> q) :==> (Forall x p :==> Forall x q)
axiomImpAll x p | isFree (Var x) p = Theorem $ p :==> Forall x p
axiomExEq x t | occurs (Var x) t = Theorem $ Exists x $ Var x =: t
axiomRefl t       = Theorem $ t =: t
axiomFunCong  f ls rs = Theorem $ foldr (:==>) (Fun f ls =: Fun f rs) $ zipWith (=:) ls rs
axiomPredCong p ls rs = Theorem $ foldr (:==>) (Atom p ls :==> Atom p rs) $ zipWith (=:) ls rs

In theory, we could write all our formulas with just implication, falsehood and the universal quantifier, but for our sanity’s sake we support all the popular connectives:

axiomIffImp1 p q = Theorem $ (p :<=> q) :==> (p :==> q)
axiomIffImp2 p q = Theorem $ (p :<=> q) :==> (q :==> p)
axiomImpIff p q  = Theorem $ (p :==> q) :==> ((q :==> p) :==> (p :<=> q))
axiomTrue        = Theorem $ Top :<=> (Bot :==> Bot)
axiomNot p       = Theorem $ Not p :<=> (p :==> Bot)
axiomAnd p q     = Theorem $ (p :/\ q) :<=> ((p :==> (q :==> Bot)) :==> Bot)
axiomOr p q      = Theorem $ (p :\/ q) :<=> Not (Not p :/\ Not q)
axiomExists x p  = Theorem $ Exists x p :<=> Not (Forall x $ Not p)

We’re done! We have built an interactive theorem prover.

Well, we would have if we had a REPL (though edit-compile-run is tolerable) and if our compiler supported modules: the Theorem data constructor should never be used again, and modules would enforce this. (Ideally we’d also provide a unidirectional pattern synonym for matching purposes.)

Instead, we must rely on the honour system: from now on, Theorem may only appear when pattern matching.

Calculemus!

We prove theorems and derive rules:

-- |-  p ==> p
impRefl p = ponens (ponens
  (axiomS p (p :==> p) p)
  (axiomK p $ p :==> p))
  (axiomK p p)

-- |- p ==> p ==> q  /  |- p ==> q
impDedup th@(Theorem (p :==> (_ :==> q))) = ponens (ponens (axiomS p p q) th) (impRefl p)

-- |- q  /  |- p ==> q
addAssum p th@(Theorem f) = ponens (axiomK f p) th

-- |- q ==> r  /  |- (p ==> q) ==> (p ==> r)
impAddAssum p th@(Theorem (q :==> r)) = ponens (axiomS p q r) (addAssum p th)

-- |- p ==> q  |- q ==> r  /  |- p ==> r
impTrans th1@(Theorem (p :==> _)) th2 = ponens (impAddAssum p th2) th1

-- |- p ==> r  /  |- p ==> q ==> r
impInsert q th@(Theorem (p :==> r)) = impTrans th (axiomK r q)

-- |- p ==> q ==> r  /  |- q ==> p ==> r
impSwap th@(Theorem (p :==> (q :==> r))) = impTrans (axiomK q p) $ ponens (axiomS p q r) th

-- |- (q ==> r) ==> (p ==> q) ==> (p ==> r)
impTransTh p q r = impTrans (axiomK (q :==> r) p) (axiomS p q r)

-- |- p ==> q  /  |- (p ==> r) ==> (q ==> r)
impAddConcl r th@(Theorem (p :==> q)) = ponens (impSwap (impTransTh p q r)) th

-- |- (p ==> q ==> r) ==> (q ==> p ==> r)
impSwapTh p q r = impTrans (axiomS p q r) $ impAddConcl (p :==> r) $ axiomK q p

-- |- (p ==> q ==> r) ==> (s ==> t ==> u)  /  |- (q ==> p ==> r) ==> (t ==> s ==> u)
impSwap2 th@(Theorem ((p :==> (q :==> r)) :==> (s :==> (t :==> u))))
  = impTrans (impSwapTh q p r) (impTrans th (impSwapTh s t u))

-- |- p ==> q ==> r  |- p ==> q  /  |- p ==> r
rightMP ith th = impDedup (impTrans th (impSwap ith))

-- |- p <=> q  /  |- p ==> q
iffImp1 th@(Theorem (p :<=> q)) = ponens (axiomIffImp1 p q) th

-- |- p <=> q  /  |- q ==> p
iffImp2 th@(Theorem (p :<=> q)) = ponens (axiomIffImp2 p q) th

-- |- p ==> q  |- q ==> p  /  |- p <=> q
impAntisym th1@(Theorem (p :==> q)) th2 = ponens (ponens (axiomImpIff p q) th1) th2

-- |- p ==> (q ==> 0) ==> 0  /  |- p ==> q
rightDoubleNeg th@(Theorem (p :==> ((_ :==> Bot) :==> Bot))) = impTrans th $ axiomLEM p

-- |- 0 ==> p
exFalso p = rightDoubleNeg $ axiomK Bot (p :==> Bot)

-- |- 1
truth = ponens (iffImp2 axiomTrue) (impRefl Bot)

-- |- s = t ==> t = s
eqSym s t = let
  rth = axiomRefl s
  f th = ponens (impSwap th) rth
  in f $ f $ axiomPredCong "=" [s, s] [t, s]

-- |- s = t ==> t = u ==> s = u
eqTrans s t u = let
  th1 = axiomPredCong "=" [t, u] [s, u]
  th2 = ponens (impSwap th1) (axiomRefl u)
  in impTrans (eqSym s t) th2

examples =
  [ axiomOr (Atom "x" []) (Atom "y" [])
  , impTransTh (Atom "Foo" []) (Atom "Bar" []) (Atom "Baz" [])
  , eqSym (Var "a") (Var "b")
  , eqTrans (Var "x") (Var "y") (Var "z")
  ]

concl (Theorem t) = t
main = mapM_ (putStr . flip shows "\n" . concl) examples

Ben Lynn blynn@cs.stanford.edu 💡

Hilbert Systems

Prelude

Terms, Formulas, Theorems

Rules and Axioms

Calculemus!

Contents