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

Mathlib defines a function List.union that returns the concatenation of the two lists with duplicates removed, assuming that the original two lists had no duplicate elements. Unfortunately, that function has quadratic complexity. The file LAMR/Util/Misc defines a more efficient version, List.union', that uses hash sets.

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,
  -p q -r,
  -p q
}

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

def exCnf2 := cnf!{
  p q,
  -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. The file LAMR/Util/Misc.lean defines a function List.union' that forms the union of two lists; if the original two lists have no duplicates, the union won’t either. It also defines 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

Write a Lean function that, given any element of PropForm, outputs a list of all the subformulas.
Write a function in Lean that implements substitution for propositional formulas, and test it on one or two examples.
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.
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.
In Section 5.2, we defined a Lean function PropForm.eval that evaluates a propositional formula with respect to a truth assignment. Define a similar function, CnfForm.eval, that evaluates a formula in conjunctive normal form. (Do it directly: don’t translate it to a propositional formula.)
In Section 5.3, we defined a Lean data type NnfForm for NNF formulas, and we defined a function PropForm.toNnfForm that converts a propositional formula to one in NNF. Notice that the method we used to expand \(\liff\) can lead to an exponential increase in length.

Define a Lean data type EnnfForm for extended negation normal form formulas, which adds the \(\liff\) connective to ordinary NNF. Then define a function that translates any propositional formula to an extended NNF formula.