# Hilbert Systems

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 💡