5. Implementing Propositional Logic

5.1. Syntax

We have seen that the set of propositional formulas can be defined inductively, and we have seen that Lean makes it easy to specify inductively defined types. It’s a match made in heaven! Here is the definition of the type of propositional formulas that we will use in this course:

namespace hidden

inductive PropForm
  | tr     : PropForm
  | fls    : PropForm
  | var    : String  PropForm
  | conj   : PropForm  PropForm  PropForm
  | disj   : PropForm  PropForm  PropForm
  | impl   : PropForm  PropForm  PropForm
  | neg    : PropForm  PropForm
  | biImpl : PropForm  PropForm  PropForm
  deriving Repr, DecidableEq

end hidden

#print PropForm

open PropForm

#check (impl (conj (var "p") (var "q")) (var "r"))

You can find this example in the file implementing_propositional_logic/examples.lean in the User folder of the course repository.

The command import LAMR.Util.Propositional at the top of the file imports the part of the library with functions that we provide for you to deal with propositional logic. We will often put a copy of a definition from the library in an examples file so you can experiment with it. Here we have put it in a namespace called hidden so that our copy’s full name is hidden.PropForm, which won’t conflict with the one in the library. Outside the hidden namespace, the command #print PropForm refers to the real one, that is, the one in the library. The command open PropForm means that we can write, for example, tr for the first constructor instead of PropForm.tr. Try writing some propositional formulas of your own. There should be squiggly blue lines under the the #print and #check commands in VSCode, indicating that there is Lean output associated with these. You can see it by hovering over the commands, or by moving the caret to the command and checking the Lean infoview window.

The phrase deriving Repr, DecidableEq tells Lean to automatically define functions to be used to test equality of two expressions of type PropForm and to display the result of an #eval. We’ll generally leave these out of the display from now on. You an always use #check and #print to learn more about a definition in the library. If you hold down ctrl and click on an identifier, the VSCode Lean extension will take you to the definition in the library. Simply holding down ctrl and hovering over it will show you the definition in a pop-up window. Try taking a look at the definition of PropForm in the library.

Writing propositional formulas using constructors can be a pain in the neck. In the library, we have used Lean’s mechanisms for defining new syntax to implement nicer syntax.

#check prop!{p  q  (r  ¬ p)  q}
#check prop!{p  q  r  p}

def propExample := prop!{p  q  r  p  ¬ s1  s2 }

#print propExample
#eval propExample

#eval toString propExample

You can get the symbols by typing \and, \to, \or, \not, and \iff in VS Code. And, in general, when you see a symbol in VSCode, hovering over it with the mouse shows you how to type it. Once again, try typing some examples of your own. The library defines the function PropForm.toString that produces a more readable version of a propositional formula, one that, when inserted within the prop!{…} brackets, should produce the same result.

Because PropForm is inductively defined, we can easily define functions using structural recursion.

namespace PropForm

def complexity : PropForm  Nat
  | var _ => 0
  | tr => 0
  | fls => 0
  | neg A => complexity A + 1
  | conj A B => complexity A + complexity B + 1
  | disj A B => complexity A + complexity B + 1
  | impl A B => complexity A + complexity B + 1
  | biImpl A B => complexity A + complexity B + 1

def depth : PropForm  Nat
  | var _ => 0
  | tr => 0
  | fls => 0
  | neg A => depth A + 1
  | conj A B => Nat.max (depth A) (depth B) + 1
  | disj A B => Nat.max (depth A) (depth B) + 1
  | impl A B => Nat.max (depth A) (depth B) + 1
  | biImpl A B => Nat.max (depth A) (depth B) + 1

def vars : PropForm  List String
  | var s => [s]
  | tr => []
  | fls => []
  | neg A => vars A
  | conj A B => (vars A).union (vars B)
  | disj A B => (vars A).union (vars B)
  | impl A B => (vars A).union (vars B)
  | biImpl A B => (vars A).union (vars B)

#eval complexity propExample
#eval depth propExample
#eval vars propExample

end PropForm

#eval PropForm.complexity propExample
#eval propExample.complexity

The function List.union returns concatenation of the two lists with duplicates removed, assuming that the original two lists had no duplicate elements.

5.2. Semantics

The course library defines the type PropAssignment to be List (String × Bool). If v has type PropAssignment, you should think of the expression v.eval s as assigning a truth value to the variable named s. The following function then evaluates the truth value of any propositional formula under assignment v:

def PropForm.eval (v : PropAssignment) : PropForm  Bool
  | var s => v.eval s
  | tr => true
  | fls => false
  | neg A => !(eval v A)
  | conj A B => (eval v A) && (eval v B)
  | disj A B => (eval v A) || (eval v B)
  | impl A B => !(eval v A) || (eval v B)
  | biImpl A B => (!(eval v A) || (eval v B)) && (!(eval v B) || (eval v A))

-- try it out
#eval let v := PropAssignment.mk [("p", true), ("q", true), ("r", true)]
      propExample.eval v

The example at the end defines v to be the assignment that assigns the value true to the strings “p”, “q”, and “r” and false to all the others. This is a reasonably convenient way to describe truth assignments manually, so the library provides a function PropAssignment.mk and notation propassign!{…} to support that.

#check propassign!{p, q, r}

#eval propExample.eval propassign!{p, q, r}

You should think about how the next function manages to compute a list of all the sublists of a given list. It is analogous to the power set operation in set theory.

def allSublists : List α  List (List α)
  | [] => [[]]
  | (a :: as) =>
      let recval := allSublists as
      recval.map (a :: .) ++ recval

#eval allSublists propExample.vars

With that in hand, here is a function that computes the truth table of a propositional formula. The value of truthTable A is a list of pairs: the first element of the pair is the list of true/false values assigned to the elements of vars A, and the second element is the truth value of A under that assignment.

def truthTable (A : PropForm) : List (List Bool × Bool) :=
  let vars := A.vars
  let assignments := (allSublists vars).map (fun l => PropAssignment.mk (l.map (., true)))
  let evalLine := fun v : PropAssignment => (vars.map v.eval, A.eval v)
  assignments.map evalLine

#eval truthTable propExample

We can now use the list operation List.all to test whether a formula is valid, and we can use List.some to test whether it is satisfiable.

def PropForm.isValid (A : PropForm) : Bool := List.all (truthTable A) Prod.snd
def PropForm.isSat(A : PropForm) : Bool := List.any (truthTable A) Prod.snd

#eval propExample.isValid
#eval propExample.isSat

5.3. Normal Forms

The library defines an inductive type of negation-normal form formulas:

inductive Lit
  | tr  : Lit
  | fls : Lit
  | pos : String  Lit
  | neg : String  Lit

inductive NnfForm :=
  | lit  (l : Lit)       : NnfForm
  | conj (p q : NnfForm) : NnfForm
  | disj (p q : NnfForm) : NnfForm

It is then straightforward to define the negation operation for formulas in negation normal form, and a translation from propositional formulas to formulas in negation normal form.

def Lit.negate : Lit  Lit
  | tr   => fls
  | fls  => tr
  | pos s => neg s
  | neg s => pos s

def NnfForm.neg : NnfForm  NnfForm
  | lit l    => lit l.negate
  | conj p q => disj (neg p) (neg q)
  | disj p q => conj (neg p) (neg q)

namespace PropForm

def toNnfForm : PropForm  NnfForm
  | tr         => NnfForm.lit Lit.tr
  | fls        => NnfForm.lit Lit.fls
  | var n      => NnfForm.lit (Lit.pos n)
  | neg p      => p.toNnfForm.neg
  | conj p q   => NnfForm.conj p.toNnfForm q.toNnfForm
  | disj p q   => NnfForm.disj p.toNnfForm q.toNnfForm
  | impl p q   => NnfForm.disj p.toNnfForm.neg q.toNnfForm
  | biImpl p q => NnfForm.conj (NnfForm.disj p.toNnfForm.neg q.toNnfForm)
                               (NnfForm.disj q.toNnfForm.neg p.toNnfForm)

end PropForm

Putting the first in the namespace NnfForm has the effect that given A : NnfForm, we can write A.neg instead of NnfForm.neg A. Similarly, putting the second definition in the namespace PropForm means we can write A.toNnfForm to put a propositional formula in negation normal form.

We can try them out on the example defined above:

#eval propExample.toNnfForm
#eval toString propExample.toNnfForm

To handle conjunctive normal form, the library defines a type Lit of literals. A Clause is then a list of literals, and a CnfForm is a list of clauses.

def Clause := List Lit

def CnfForm := List Clause

As usual, you can use #check and #print to find information about them, and ctrl-click to see the definitions in the library. Since, as usual, defining things using constructors can be annoying, the library defines syntax for writing expressions of these types.

def exLit0 := lit!{ p }
def exLit1 := lit!{ -q }

#print exLit0
#print exLit1

def exClause0 := clause!{ p }
def exClause1 := clause!{ p -q r }
def exClause2 := clause!{ r -s }

#print exClause0
#print exClause1
#print exClause2

def exCnf0 := cnf!{
  -p q -r,
  -p q

def exCnf1 := cnf!{
  p -q,
  p q,
  -p -r,
  -p r

def exCnf2 := cnf!{
  p q,

#print exCnf0
#print exCnf1
#print exCnf2

#eval toString exClause1
#eval toString exCnf2

Let us now consider what is needed to put an arbitrary propositional formula in conjunctive normal form. In Section 4.5, we saw that the key is to show that the disjunction of two CNF formulas is again CNF. Lean’s library has a function List.insert, which adds an element to a list; if the element already appears in the list, it does nothing. It has a function List.union that will form the union of two lists; if the original two lists have no duplicates, the union won’t either. Finally, we have a function List.Union which takes the union of a list of lists. Since clauses are lists, we can use them on clauses:

#eval List.insert lit!{ r } exClause0

#eval exClause0.union exClause1

#eval List.Union [exClause0, exClause1, exClause2]

We can now take the disjunction of a single clause and a CNF formula by taking the union of the clause with each element of the CNF formula. We can implement that with the function List.map:

#eval exCnf1.map exClause0.union

This applied the function “take the union with exClause0” to each element of exCnf1, and returns the resulting list. We can now define the disjunction of two CNF formulas by taking all the clauses in the first, taking the disjunction of each clause with the second CNF, and then taking the union of all of those, corresponding to the conjunctions of the CNFs. Here is the library definition, and an example:

def CnfForm.disj (cnf1 cnf2 : CnfForm) : CnfForm :=
(cnf1.map (fun cls => cnf2.map cls.union)).Union

#eval cnf!{p, q, u -v}.disj cnf!{r1 r2, s1 s2, t1 t2 t3}
#eval toString $ cnf!{p, q, u -v}.disj cnf!{r1 r2, s1 s2, t1 t2 t3}

Functional programmers like this sort of definition; it’s short, clever, and inscrutable. You should think about defining the disjunction of two CNF formulas by hand, using recursions over clauses and CNF formulas. Your solution will most likely reconstruct the effect of the instance map and Union in the library definition, and that will help you understand why they make sense.

In any case, with this in hand, it is easy to define the translation from negation normal form formulas and arbitrary propositional formulas to CNF.

def NnfForm.toCnfForm : NnfForm  CnfForm
  | NnfForm.lit (Lit.pos s) => [ [Lit.pos s] ]
  | NnfForm.lit (Lit.neg s) => [ [Lit.neg s] ]
  | NnfForm.lit Lit.tr      => []
  | NnfForm.lit Lit.fls     => [ [] ]
  | NnfForm.conj A B        => A.toCnfForm.conj B.toCnfForm
  | NnfForm.disj A B        => A.toCnfForm.disj B.toCnfForm

def PropForm.toCnfForm (A : PropForm) : CnfForm := A.toNnfForm.toCnfForm

We can try them out:

#eval propExample.toCnfForm

#eval prop!{(p1  p2)  (q1  q2)}.toCnfForm.toString

#eval prop!{(p1  p2)  (q1  q2)  (r1  r2)  (s1  s2)}.toCnfForm.toString

5.4. Exercises

  1. Write a Lean function that, given any element of PropForm, outputs a list of all the subformulas.

  2. Write a Lean function that, given a list of propositional formulas and another propositional formula, determines whether the second is a logical consequence of the first.

  3. Write a Lean function that, given a clause, tests whether any literal Lit.pos p appears together with its negation Lit.neg p. Write another Lean function that, given a formula in conjunctive normal form, deletes all these clauses.