User:Hakerh400/Theorem prover

Introduction

In this tutorial we explain how to create a very simple theorem prover in Haskell using generalised algebraic data types. We first define axioms and inference rules, then write a formal proof of a theorem and then write a program to check whether the proof is valid.

Formal system

The formal logic system that we use in this example is a simplified version of Łukasiewicz system. We define the following inference rules (the first two are axioms because they have no premises and the third one is Modus ponens):

${\begin{aligned}&\vdash x\to (y\to x)\\&\vdash (x\to (y\to z))\to ((x\to y)\to (x\to z))\\x,x\to y&\vdash y\end{aligned}}$

We call the first one Ax1, the second one Ax2 and the third one MP. Implication is represented by -> and the inference symbol is |-. We want to prove that $(x\to x)$ for any predicate $x$ (the theorem of the reflexivity of the implication).

Before we start, we want to make sure that x,y,z must be well-formed formulas. A well-formed formula in our system is only a predicate. A predicate is either an implication, or some contant predicate P (just as an example to reduce the generality). We can construct an implication only if both arguments are WFFs (well-formed formulas). The constant predicate P is a WFF by definition.

The program

{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE KindSignatures #-} main :: IO () main = putStrLn output output :: String output = show (th_impl_refl (PredP P)) ---------------------------------------------------------------------------------------------------- data Pred :: * -> * where PredP :: P -> Pred P PredImpl :: Impl a b -> Pred (Impl a b) data P :: * where P :: P data Impl :: * -> * -> * where Impl :: Pred a -> Pred b -> Impl a b data Infer :: * -> * where Ax1 :: Pred a -> Pred b -> Infer (Impl a (Impl b a)) Ax2 :: Pred a -> Pred b -> Pred c -> Infer (Impl (Impl a (Impl b c)) (Impl (Impl a b) (Impl a c))) MP :: Infer (Impl a b) -> Infer a -> Infer b ---------------------------------------------------------------------------------------------------- instance Show (Pred a) where show (PredP a) = show a show (PredImpl a) = show a instance Show P where show P = "P" instance Show (Impl a b) where show (Impl a b) = "(" ++ (show a) ++ " -> " ++ (show b) ++ ")" instance Show (Infer a) where show (Ax1 a b) = "(Ax1 " ++ (show a) ++ " " ++ (show b) ++ ")" show (Ax2 a b c) = "(Ax2 " ++ (show a) ++ " " ++ (show b) ++ " " ++ (show c) ++ ")" show (MP a b) = "(MP " ++ (show a) ++ " " ++ (show b) ++ ")" ---------------------------------------------------------------------------------------------------- type T1 a = Impl a a type T2 a = Impl a (T1 a) type T3 a = Impl a (Impl (T1 a) a) type T4 a = Impl (T2 a) (T1 a) th_impl_refl :: forall a. Pred a -> Infer (Impl a a) th_impl_refl x = step_6 where step_1 = PredImpl (Impl x x) :: Pred (T1 a) step_2 = Ax1 x x :: Infer (T2 a) step_3 = Ax1 x step_1 :: Infer (T3 a) step_4 = Ax2 x step_1 x :: Infer (Impl (T3 a) (T4 a)) step_5 = MP step_4 step_3 :: Infer (T4 a) step_6 = MP step_5 step_2 :: Infer (T1 a)

Explanation

Data types

We define four data types. The first data type is Pred, which stands for predicate. It represents predicate WFF (currently the only type of WFF in our system). It is an "abstract" data type in the sense that it just represents a label that we assign to already constructed other data types. In particular, it says that we can label P as a predicate, or we cal label an implication as a predicate. It is like an abstract class in OOP languages.

The next data type is P, which does not have any particular meaning in the system. It is just there for us to be able to examine the result of the proof (otherwise, any attemp to construct a predicate would not terminate).

The third data type is Impl, which stands for implication. As we explained, it "asserts" that both of its arguments must be predicates.

The last data type is Infer, which represents a proof of a predicate. We can construct it using three different constructors. We can either use one of the axioms (Ax1 or Ax2), or we can apply Modus ponens.

Next, we have some functions for stringifying our data types. They are just for analyzing the results.

Theorem

Finally, we define and prove theorem th_impl_refl, which states that for any predicate a, the statement $(a\to a)$ is true. We prove it in six steps. The first step proves that if a is a predicate, then Impl a a is also a predicate (types T1..T4 are defined just as aliases to save space). Steps 2 and 3 apply axiom Ax1, step 4 applies axiom Ax2 and steps 5 and 6 apply Modus ponens. The type signature of each step is used for correctness check.

Verifying the proof

If the program does not compile, either the proof is wrong, or you have syntax errors. If the program compiles, it still does not mean that the proof is correct, because you may have a cyclic theorem dependency in your proof. You need to run the program and make sure the program halts. If the program does not halt, it probably means you have a cyclic dependency somewhere.

The output of the program is the proof of the theorem for sample statement P that we introduced just for this purpose. The program show the following output:

(MP (MP (Ax2 P (P -> P) P) (Ax1 P (P -> P))) (Ax1 P P))

Adding new features

It is very easy to add new features (axioms, inference rules, definitions, data types, theorems, etc). For example, if we want to add new axiom Ax3 that defines negation:

$\vdash (\lnot x\to \lnot y)\to (y\to x)$

and we want to prove that $\lnot \lnot x\to (\lnot x\to x)$ for any statement $x$, then we need update the program by adding a new data type Not for negation, new axiom Ax3 as an Infer constructor, and finally theorem th_2 that proves what we need.

{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE KindSignatures #-} main :: IO () main = putStrLn output output :: String output = show (th_2 (PredP P)) ---------------------------------------------------------------------------------------------------- data Pred :: * -> * where PredP :: P -> Pred P PredImpl :: Impl a b -> Pred (Impl a b) PredNot :: Not a -> Pred (Not a) data P :: * where P :: P data Impl :: * -> * -> * where Impl :: Pred a -> Pred b -> Impl a b data Not :: * -> * where Not :: Pred a -> Not a data Infer :: * -> * where Ax1 :: Pred a -> Pred b -> Infer (Impl a (Impl b a)) Ax2 :: Pred a -> Pred b -> Pred c -> Infer (Impl (Impl a (Impl b c)) (Impl (Impl a b) (Impl a c))) Ax3 :: Pred a -> Pred b -> Infer (Impl (Impl (Not a) (Not b)) (Impl b a)) MP :: Infer (Impl a b) -> Infer a -> Infer b ---------------------------------------------------------------------------------------------------- instance Show (Pred a) where show (PredP a) = show a show (PredImpl a) = show a show (PredNot a) = show a instance Show P where show P = "P" instance Show (Impl a b) where show (Impl a b) = "(" ++ (show a) ++ " -> " ++ (show b) ++ ")" instance Show (Not a) where show (Not a) = "~" ++ (show a) instance Show (Infer a) where show (Ax1 a b) = "(Ax1 " ++ (show a) ++ " " ++ (show b) ++ ")" show (Ax2 a b c) = "(Ax2 " ++ (show a) ++ " " ++ (show b) ++ " " ++ (show c) ++ ")" show (Ax3 a b) = "(Ax3 " ++ (show a) ++ " " ++ (show b) ++ ")" show (MP a b) = "(MP " ++ (show a) ++ " " ++ (show b) ++ ")" ---------------------------------------------------------------------------------------------------- type T1 a = Impl a a type T2 a = Impl a (T1 a) type T3 a = Impl a (Impl (T1 a) a) type T4 a = Impl (T2 a) (T1 a) th_impl_refl :: forall a. Pred a -> Infer (Impl a a) th_impl_refl x = step_5 where wff_1 = PredImpl (Impl x x) :: Pred (T1 a) step_1 = Ax1 x x :: Infer (T2 a) step_2 = Ax1 x wff_1 :: Infer (T3 a) step_3 = Ax2 x wff_1 x :: Infer (Impl (T3 a) (T4 a)) step_4 = MP step_3 step_2 :: Infer (T4 a) step_5 = MP step_4 step_1 :: Infer (T1 a) type T5 a = Impl (T6 a) (T9 a) type T6 a = Not (Not a) type T7 a = Impl (Not a) (T6 a) type T8 a = Impl (Impl (T6 a) (T7 a)) (Impl (T6 a) (T10 a)) type T9 a = Impl (T7 a) (T10 a) type T10 a = Impl (Not a) a th_2 :: forall a. Pred a -> Infer (Impl (Not (Not a)) (Impl (Not a) a)) th_2 x = step_7 where wff_1 = PredNot (Not x) :: Pred (Not a) wff_2 = PredNot (Not wff_1) :: Pred (T6 a) wff_3 = PredImpl (Impl wff_1 wff_2) :: Pred (T7 a) wff_4 = PredImpl (Impl wff_1 x) :: Pred (T10 a) wff_5 = PredImpl (Impl wff_3 wff_4) :: Pred (T9 a) step_1 = Ax3 x wff_1 :: Infer (T9 a) step_2 = Ax1 wff_5 wff_2 :: Infer (Impl (T9 a) (T5 a)) step_3 = MP step_2 step_1 :: Infer (T5 a) step_4 = Ax2 wff_2 wff_3 wff_4 :: Infer (Impl (T5 a) (T8 a)) step_5 = MP step_4 step_3 :: Infer (T8 a) step_6 = Ax1 wff_2 wff_1 :: Infer (Impl (T6 a) (T7 a)) step_7 = MP step_5 step_6 :: Infer (Impl (T6 a) (T10 a))

Explanation

We renamed some of the steps to separate "WFF" proofs from "Infer" proofs (we also updated th_impl_refl). The program outputs the following proof:

(MP (MP (Ax2 ~~P (~P -> ~~P) (~P -> P)) (MP (Ax1 ((~P -> ~~P) -> (~P -> P)) ~~P) (Ax3 P ~P))) (Ax1 ~~P ~P))

Notice that WFF steps are almost half of the total steps. If we remove the WFF checks, we can make the proof of the theorem a lot simpler. However, forcing a formula to be well-formed is important, because the system can be expanded to include other types of expressions (such as sets and proper classes). We want to make sure that the arguments of an implication are predicates, and not for example sets. Also, WFF can be generalized to any level of abstraction, so if we decide to introduce quantifiers, we can use WFF checks to ensure that there are no free identifiers in the top-level expression (each identifier must be bound to a quantifier parameter name). When we talk about identifiers, they can be implemented as De Bruijn indices and substitutions can be achieved by a recursive constraint that ensures that all occurrences of the bound variable are replaced.