Capturing Number Theory in Haskell

In Chapter VII of GEB, the author gives a description of Gentzen’s Propositional Calculus, along with some examples of applying its rules, and in Chapter VIII, the author gives a description of TNT (Typographical Number Theory).

In this post we’ll provide an implementation of these systems in Haskell.

Propositional calculus

On page 181 the symbols of the system are listed. We can map them nicely in Haskell:

data PropCalc =
  P | Q | R
  | Not PropCalc
  | And PropCalc PropCalc
  | Or PropCalc PropCalc
  | Imp PropCalc PropCalc
  deriving (Show, Eq)

We will slightly rewrite this to make it more generic. This will allow us to later embed this system in other systems.

data VarEg = P | Q | R deriving (Show, Eq)

data PropCalc a =
  PropVar a
  | Not (PropCalc a)
  | And (PropCalc a) (PropCalc a)
  | Or (PropCalc a) (PropCalc a)
  | Imp (PropCalc a) (PropCalc a)
  deriving (Show, Eq)

In the book, what follows after this is a list of formation rules. For example, here’s how we can implement and-intro and and-elim:

-- And intro
ruleJoin :: PropCalc a -> PropCalc a -> PropCalc a
ruleJoin x y = And x y

-- And elim l
ruleSepL :: PropCalc a -> PropCalc a
ruleSepL (And x y) = x
ruleSepL x = x

-- And elim r
ruleSepR :: PropCalc a -> PropCalc a
ruleSepR (And x y) = y
ruleSepR x = x

That is, we just lift the values from the object level to Haskell’s level, and Haskell’s neat type system takes care of everything else.

Perhaps the most powerful rule is the implication-intro. Here’s its implementation:

-- Imp intro
ruleCarryOver :: (PropCalc a -> PropCalc a) -> PropCalc a -> PropCalc a
ruleCarryOver f x = Imp x (f x)

We rely on Haskell’s machinery for functions (lambda calculus) to take care of it. Now we can prove neat stuff, such as $P \land Q \to Q \land P$ :

> ruleCarryOver (\pq -> ruleJoin (ruleSepR pq) (ruleSepL pq)) (ruleJoin (PropVar P) (PropVar Q))
Imp (And (PropVar P) (PropVar Q)) (And (PropVar Q) (PropVar P))

Another proof that $P \to (Q \to (P \land Q))$ :

> ruleCarryOver (\x -> ruleCarryOver (\y -> ruleJoin x y) (PropVar Q)) (PropVar P)
Imp (PropVar P) (Imp (PropVar Q) (And (PropVar P) (PropVar Q)))

Neat!

One of the rules is about double negation, which the author refers to as the double-tilde rule, meaning that $P$ and $\neg \neg P$ are interchangeable. Their implementation in Haskell is simple:

-- Not intro
ruleDoubleTildeIntro :: PropCalc a -> PropCalc a
ruleDoubleTildeIntro x = Not (Not x)

-- Not elim
ruleDoubleTildeElim :: PropCalc a -> PropCalc a
ruleDoubleTildeElim (Not (Not x)) = x
ruleDoubleTildeElim x = x

So now we can do stuff like:

> ruleDoubleTildeIntro (PropVar Q)
Not (Not (PropVar Q))

However, how do we apply this rule to $R$ within $P \land (Q \lor R)$ ? Our current implementation doesn’t allow for that, because it only accepts a full formula and doesn’t know how to do replacements in its subformulas. Let’s fix this.

The idea is to create a function that will accept a “path” (which subformula we want to work on), a rule that will be applied to this subformula, and a formula.

data Pos = GoLeft | GoRight

type Path = [Pos]

applyPropRule :: Path -> (PropCalc a -> PropCalc a) -> PropCalc a -> PropCalc a
applyPropRule [] f x = f x
applyPropRule (GoLeft:xs) f (Not x) = Not (applyPropRule xs f x)
applyPropRule (GoLeft:xs) f (And x y) = And (applyPropRule xs f x) y
applyPropRule (GoLeft:xs) f (Or x y) = Or (applyPropRule xs f x) y
applyPropRule (GoLeft:xs) f (Imp x y) = Imp (applyPropRule xs f x) y
applyPropRule (GoRight:xs) f (Not x) = Not (applyPropRule xs f x)
applyPropRule (GoRight:xs) f (And x y) = And x (applyPropRule xs f y)
applyPropRule (GoRight:xs) f (Or x y) = Or x (applyPropRule xs f y)
applyPropRule (GoRight:xs) f (Imp x y) = Imp x (applyPropRule xs f y)
applyPropRule _ _ x = x

Of course, going left or right doesn’t make much sense for unary operators, so our implementation will just drill down in the Not operator if it finds either a left or a right. But, left and right do make sense for binary operators – we drill on the left and the right argument respectively.

Now we can use it to apply the double negation rule to $R$ within $P \land (Q \lor R)$ as follows:

> applyPropRule [GoRight, GoRight] ruleDoubleTildeIntro (And (PropVar P) (Or (PropVar Q) (PropVar R)))
And (PropVar P) (Or (PropVar Q) (Not (Not (PropVar R))))

Neat! We now have our logic defined. The full code of this logic is available here.

Number theory

Starting on page 204, a description of a number theoretic system is given which implements Peano’s axioms, under the name TNT – Typographical Number Theory. Further, the logic we defined earlier is embedded into this system.

Let’s start by writing the Haskell implementation for TNT.

For the arithmetical part, we have variables, zero, and the operations successor, addition, multiplication.

data Vars = A | B | C | D | E deriving (Show, Eq)

data Arith =
  Var Vars
  | Z
  | S Arith
  | Plus Arith Arith
  | Mult Arith Arith
  deriving (Show, Eq)

Now we can represent things like $0 + 1*A$ as follows:

> Plus Z (Mult (S Z) (Var A))
Plus Z (Mult (S Z) (Var A))

The next step is to implement the components from first-order logic (quantifiers and arithmetical equations):

data FOL =
  Eq Arith Arith
  | ForAll Vars (PropCalc FOL)
  | Exists Vars (PropCalc FOL)
  deriving (Show, Eq)

We can now encode Peano’s axioms as follows:

-- forall a, not (S a = 0)
axiom1 = PropVar (ForAll A (Not (PropVar (Eq (S (Var A)) Z))))

-- forall a, (a + 0) = a
axiom2 = PropVar (ForAll A (PropVar (Eq (Plus (Var A) Z) (Var A))))

-- forall a, forall b, a + Sb = S(a + b)
axiom3 = PropVar (ForAll A (PropVar (ForAll B (PropVar (Eq (Plus (Var A) (S (Var B))) (S (Plus (Var A) (Var B))))))))

-- forall a, (a * 0) = 0
axiom4 = PropVar (ForAll A (PropVar (Eq (Mult (Var A) Z) Z)))

-- forall a, forall b, a * Sb = (a * b + a)
axiom5 = PropVar (ForAll A (PropVar (ForAll B (PropVar (Eq (Mult (Var A) (S (Var B))) (Plus (Mult (Var A) (Var B)) (Var A)))))))

Neat. We will only list a few of the rules here, for the sake of example:

-- Rule of interchange: forall x !y -> ! exists x, y
ruleInterchangeL :: PropCalc FOL -> PropCalc FOL
ruleInterchangeL (PropVar (ForAll x (Not y))) = Not (PropVar $ Exists x y)
ruleInterchangeL x = x

-- Rule of symmetry: a = b == b == a
ruleSymmetry :: PropCalc FOL -> PropCalc FOL
ruleSymmetry (PropVar (Eq a b)) = PropVar (Eq b a)
ruleSymmetry x = x

Similarly to applyPropRule, we construct applyFOLRule:

-- Might be useful for some rules that may require drilling, like `ruleInterchangeL`
applyFOLRule :: Path -> (PropCalc FOL -> PropCalc FOL) -> PropCalc FOL -> PropCalc FOL
applyFOLRule [] f x = f x
applyFOLRule (_:xs) f (PropVar (ForAll x y)) = PropVar (ForAll x (applyFOLRule xs f y))
applyFOLRule (_:xs) f (PropVar (Exists x y)) = PropVar (Exists x (applyFOLRule xs f y))
applyFOLRule (_:xs) f (Not x)                = Not (applyFOLRule xs f x)
applyFOLRule (GoLeft:xs) f (And x y)         = And (applyFOLRule xs f x) y
applyFOLRule (GoRight:xs) f (And x y)        = And x (applyFOLRule xs f y)
applyFOLRule (GoLeft:xs) f (Or x y)          = Or (applyFOLRule xs f x) y
applyFOLRule (GoRight:xs) f (Or x y)         = Or x (applyFOLRule xs f y)
applyFOLRule (GoLeft:xs) f (Imp x y)         = Imp (applyFOLRule xs f x) y
applyFOLRule (GoRight:xs) f (Imp x y)        = Imp x (applyFOLRule xs f y)
applyFOLRule _ _ x = x

Now we can proceed with an example proof:

> step1 = applyFOLRule [] ruleInterchangeL axiom1
Not (PropVar (Exists A (PropVar (Eq (S (Var A)) Z))))
> step2 = applyFOLRule [GoRight, GoRight] ruleSymmetry step1
Not (PropVar (Exists A (PropVar (Eq Z (S (Var A))))))
> step3 = applyFOLRule [GoRight, GoRight] ruleDoubleTildeIntro step2 -- apply from Gentzen
Not (PropVar (Exists A (Not (Not (PropVar (Eq Z (S (Var A))))))))

That is, from $\forall A, \neg S A = Z$ , we proved that $\neg \exists A, \neg \neg Z = S A$ follows, which is awesome 🙂 Note how we applied a rule from the embedded system (Gentzen) within the current system (TNT).

This wraps our number theoretical system. The full code of this system is available here.

Conclusion

Not sure what to conclude here, other than that I had fun implementing this.

For the nth time, I was amazed by Haskell’s machinery to encode systems like these. With this implementation, I think I really got to see how powerful Haskell is for tasks like this.

I could have probably used Racket (Scheme) for this, but implementing all the rules and the applyXrule functions was a breeze given Haskell’s type-checking mechanism.