4. Predicate logic

4.1. Predicates, relations and quantifiers

Predicate logic extends propositional logic, we can use it to talk about objects and their properties. The objects are organized in types, such as ℕ : Type the type of natural numbers \(\{0,1,2,3,\dots\}\) or bool : Type the type of booleans \(\{\mathrm{tt} , \mathrm{ff}\}\), or lists over a given A : Type: list A : Type, which we will introduce in more detail soon. To avoid talking about specific types we introduce some type variables:

try it!

variables A B C : Type

We talk about types where you may be used to sets. While they are subtle differences (types are static while we can reason about set membership in set theory) for our purposes types are just a replacement of sets.

A predicate is just another word for a property, e.g. we may use Prime : ℕ → Prop to express that a number is a prime number. We can form propositions such as Prime 3 and Prime 4, the first one should be provable while the negation of the second holds. Predicates may have several inputs in which case we usually call them relations, examples are ≤ : ℕ → ℕ → Prop or inList : A → list A → Prop to form propositions like 2 ≤ 3 and InList 1 [1,2,3] (both of them should be provable).

In the sequel we will use some generic predicates for examples, such as

try it!

 variables PP QQ : A → Prop
 

The most important innovation of predicate logic are the quantifiers, which we can use to form new propositions:

• universal quantification (∀), read ∀ x : A , PP x as all x in A satisfy PP x.
• existential quantification (∃), read ∃ x : A, PP x as there is an x in A satsifying PP x.

Both quantifiers bind weaker then any other propositional operator, that is we read ∀ x : A, PP x ∧ Q as ∀ x : A , (PP x ∧ Q). We need parenheses to limit the scope, e.g. (∀ x : A, PP x) ∧ Q which has a different meanting to the proposition before.

It is important to understand bound variables, essentially they work like scoped variables in programming. We can shadow variables as in ∀ x:A , (∃ x : A , PP x) ∧ QQ x, here the x in PP x referes to ∃ x : A while the x in QQ x refers to ∀ x : A. Bound variables can be consistently renamed, hence the previous proposition is the same as ∀ y:A , (∃ z : A , PP z) ∧ QQ y, which is actually preferable since shadowing variables should be avoided because it confuses the human reader.

Now we have introduced all these variables what can we do with them. We have new primitive proposition:

• equality (=), given a b : A we write a = b which we read as a is equal to b.

In the moment we only have variables as elements of types but this will change soon when we introduce datatypes and functions.

4.2. The universal quantifier

To prove that a proposition of the form ∀ x : A , PP x holds we assume that there is given an arbitrary element a in A and prove it for this generic element, i.e. to prove PP a, we use assumption a to do this. If we have an assumption h : ∀ x : A , PP x and our current goal is PP a for some a : A then we can use apply h to prove our goal. Usuall we have some combination of implication and for all like h : ∀ x : A, PP x → QQ x and now if our current goal is QQ a and we invoke apply h Lean will instantiate x with a and it remains to show QQ a.

Best to do some examples. Let’s say we want to prove

(∀ x : A, PP x) → (∀ y : A, PP y → QQ y) → ∀ z : A , QQ z

Here is a possible translation into english where we assume that A stands for the type of students in the class, PP x means x is clever and QQ x means x is funny then we arrive at:

If all students are clever then if all clever students are funny then all students are funny.

try it!

 example : (∀ x : A, PP x)
   → (∀ y : A, PP y → QQ y)
   → ∀ z : A , QQ z :=
 begin
   assume p pq a,
   apply pq,
   apply p,
 end
  

Note that after assume the proof state is:

p : ∀ (x : A), PP x,
pq : ∀ (y : A), PP y → QQ y,
a : A
⊢ QQ a

That is the x in QQ x has been replaced by a. I could have used x again but I though this may be misleading because you may think that you have to use the same variable as in the quantifier.

Let’s prove a logical equivalence imvolving ∀ and ∧, namely that we can interchange them. That is we are going to prove

(∀ x : A, PP x ∧ QQ x)  ↔ (∀ x : A , PP x) ∧ (∀ x : A, QQ x)

To illustrate this: to say that all students are clever and funny is the same as saying that all students are clever and all students are funny.

Here is the Lean proof:

try it!

example : (∀ x : A, PP x ∧ QQ x)
  ↔ (∀ x : A , PP x) ∧ (∀ x : A, QQ x) :=
  begin
    constructor,
    assume h,
    constructor,
    assume a,
    have pq : PP a ∧ QQ a,
    apply h,
    cases pq with pa qa,
    exact pa,
    assume a,
    have pq : PP a ∧ QQ a,
    apply h,
    cases pq with pa qa,
    exact qa,
    assume h,
    cases h with hp hq,
    assume a,
    constructor,
    apply hp,
    apply hq,
  end

I am using a new structural rule here. After assume a I am in the following state (ignoring the parts not relevant now):

h : ∀ (x : A), PP x ∧ QQ x,
a : A
⊢ PP a

Now I cannot say apply h because PP a is not the conclusion of the assumption. My idea is that I can prove PP a ∧ QQ a from h and from this I can prove PP a. Hence I am using

have pq : PP a ∧ QQ a,

which creats a new goal:

h : ∀ (x : A), PP x ∧ QQ x,
a : A
⊢ PP a ∧ QQ a

h : ∀ (x : A), PP x ∧ QQ x,
a : A,
pq : PP a ∧ QQ a
⊢ PP a

but also inserts an assumption pq in my original goal. Now I can prove PP a ∧ QQ a using apply h and then I am left with:

h : ∀ (x : A), PP x ∧ QQ x,
a : A,
pq : PP a ∧ QQ a
⊢ PP a

which I can prove using cases on pq.

4.3. The existential quantifier

To prove a proposition of the form ∃ x : A , PP x it is enough to prove PP a for any a : A. We use existsi a for this and we are left having to prove PP a. Note that a can be any expression of type A not necessarily a variable. However so far we haven’t seen any way to construct elements, but this will change soon.

On the other hand to use an assumption of the form h : ∃ x : A ,  P x we are using cases h with x px which replaces h with two assumptions x : A and px : P x.

Again it is best to look at an example. We are going to prove a proposition very similar to the one for ∀:

(∃ x : A, PP x) → (∀ y : A, PP y → QQ y) → ∃ z : A , QQ z

Here is the english version using the same translation as before:

If there is a clever student and all clever students are funny then there is a funny student.

Here is the Lean proof:

try it!

example : (∃ x : A, PP x)
  → (∀ y : A, PP y → QQ y)
  → ∃ z : A , QQ z :=
begin
  assume p pq,
  cases p with a pa,
  existsi a,
  apply pq,
  exact pa,
end

After the assume we are in the following state:

p : ∃ (x : A), PP x,
pq : ∀ (y : A), PP y → QQ y
⊢ ∃ (z : A), QQ z

We first take p apart using cases p with a pa:

pq : ∀ (y : A), PP y → QQ y,
a : A,
pa : PP a
⊢ ∃ (z : A), QQ z

and now we can use existsi a:

pq : ∀ (y : A), PP y → QQ y,
a : A,
pa : PP a
⊢ QQ a

which we now should know how to complete.

As ∀ can be exchanged with ∧, ∃ can be exchanged with ∨. That is we are going to prove the following equivalence:

(∃ x : A, PP x ∨ QQ x) ↔ (∃ x : A , PP x) ∨ (∃ x : A, QQ x)

Here is the english version

There is a student who is clever or funny is the same as saying there is a student who is funny or there is a student who is clever.

Here is the complete lean proof (for you to step through online):

try it!

example : (∃ x : A, PP x ∨ QQ x)
              ↔ (∃ x : A , PP x) ∨ (∃ x : A, QQ x) :=
begin
  constructor,
  assume h,
  cases h with a ha,
  cases ha with pa qa,
  left,
  existsi a,
  exact pa,
  right,
  existsi a,
  exact qa,
  assume h,
  cases h with hp hq,
  cases hp with a pa,
  existsi a,
  left,
  exact pa,
  cases hq with a qa,
  existsi a,
  right,
  exact qa,
end

4.4. Another Currying equivalence

You may have noticed that the way we prove propositions involving → and ∀ is very similar. In both cases wem use assume to prove them by introducing an assumption in the first case a proposition and in the secnde an element in a type and in both cases we use them using apply to prove the current goal. Similarily ∧ and ∃ behave similar: in both cases we prove them using constructor where we have to construct two components in the first case the two sides of the conjunction and in the second the element and the proof that it satisfies the property. And in both case we are using cases with two components which basically replaces the assumption by its two components.

The similarity can be seen by establishing another currying-style equivalence. While currying in propositional logic had the form

P ∧ Q → R ↔ P → Q → R

where we turn a conjunction into an implication, currying for predicate logic has the form

(∃ x : A, QQ x) → R  ↔ (∀ x : A , QQ x → R)

ths time we turn an existential into a universal quantifier. For the intuition, we use QQ x to mean x is clever and R means the professor is happy. Hence the equivalence is:

If there is a student who is clever then the professor is happy is equivalent to saying if any student is clever then the professor is happy.

Here is the proof in Lean:

try it!

theorem curry_pred : (∃ x : A, PP x) → R  ↔ (∀ x : A , PP x → R)  :=
begin
  constructor,
  assume ppr a p,
  apply ppr,
  existsi a,
  exact p,
  assume ppr pp,
  cases pp with a p,
  apply ppr,
  exact p,
end

4.5. Equality

There is a generic relation which can be applied to any type: equality. Given a b : A we can construct a = b : Prop expressing that a and b are equal. we can prove that everything is equal to itself using the tactic reflexivity.

try it!

example : ∀ x : A, x=x :=
begin
  assume a,
  reflexivity,
end

If we have assumed an equality h : a=b we can use it to rewrite a into b in the goal. That is if our goal is PP a we say rewrite h and this changes the goal into PP b. Here is a simple example (with a little twist):

try it!

example:  ∀ x y : A, x=y → PP y → PP x :=
begin
  assume x y eq p,
  rewrite eq,
  exact p,
end

Sometimes we want to use the equality in the other direction, that is we want to replace b by a. In this case we use rewrite← h. Here is another example which is actually what I wanted to do first:

try it!

example:  ∀ x y : A, x=y → PP x → PP y :=
begin
  assume x y eq p,
  rewrite← eq,
  exact p,
end

Equality is an equivalence relation, it mens that it is

• reflexive (∀ x : A, x=x),
• symmetric (∀ x y : A, x=y → y=x)
• transitive (∀ x y z : A, x=y → y=z → x=z)

We have already shown reflexivity using the appropriately named tactic. We can show symmetry and transitivity using rewrite:

try it!

theorem sym_eq : ∀ x y : A, x=y → y=x :=
begin
  assume x y p,
  rewrite p,
end

After the assume the goal is:

x y : A,
p : x = y
⊢ y = x

Now I was expecting that after rewrite p the goal would be:

x y : A,
p : x = y
⊢ y = y

but actually rewrite automatically applies reflexivity if possible, hence we are already done.

Moving on to transitivity:

try it!

theorem trans_eq : ∀ x y z : A, x=y → y=z → x=z :=
begin
  assume x y z xy yz,
  rewrite xy,
  exact yz,
end

Sometimes we want to use an equality not to rewrite the goal but to reqrite another assumption. We can do this giving rise to another proof of trans.

try it!

theorem trans_eq : ∀ x y z : A, x=y → y=z → x=z :=
begin
  assume x y z xy yz,
  rewrite<- xy at yz,
  exact yz,
end

That is by saying rewrite xy at yz we are using xy to rewrite yz. The same works for rewrite←.

Actually Lean already has built-in tactics to deal with symmetry and transitivity which are often easier to use:

try it!

example : ∀ x y : A, x=y → y=x :=
begin
  assume x y p,
  symmetry,
  exact p
end

example : ∀ x y z : A, x=y → y=z → x=z :=
begin
  assume x y z xy yz,
  transitivity,
  exact xy,
  exact yz,
end

After we say``transitivity`` the goals looks a bit strange:

2 goals
A : Type,
x y z : A,
xy : x = y,
yz : y = z
⊢ x = ?m_1

A : Type,
x y z : A,
xy : x = y,
yz : y = z
⊢ ?m_1 = z

The ?m_1 is a placeholder since Lean cannot figure out at this point what we are going to use as the intermidiate term. We can just proceed, because as soon as we say exact xy, Lean can figure out that ?m_1 is y and we are left with:

A : Type,
x y z : A,
xy : x = y,
yz : y = z
⊢ y = z

which is the 2nd goal with ?m_1 instantiated. Actually we are not going to use transitivity in equational proofs but we use a special format for equational proofs indicated by calc:

try it!

example : ∀ x y z : A, x=y → y=z → x=z :=
begin
  assume x y z xy yz,
  calc
    x = y   : by exact xy
    ... = z : by exact yz,
end

After calc we prove a sequence of equalities where each step is using by followed by some tactics. Any subsequent line starts with ... which stends for the last expression of the previous line, in this case y.

There is one more property we expect from equality. Assume we have a function f : A → B and we know that x = y for some x y : A then we want to be able to conclude that f x = f y. We say that equality is a congruence. We can prove this easily using rewrite:

try it!

theorem congr_arg : ∀ f : A → B , ∀ x y : A, x = y → f x = f y :=
begin
  assume f x y h,
  rewrite h,
end

We will use congr_arg f :  ∀ x y : A, x = y → f x = f y when we need that f preserves equality.

There is a special proof style in Lean for equational proofs calc which enables to have more readable equational derivations, which we will introduce later.

4.6. Classical Predicate Logic

We can use classical logic in predicate logic even though the explanation using truth tables doesn’t work anymore, or let’s say we have to be prepared to use infinite truth tables which need a lot of paper to write out.

There are predicate logic counterparts of the de Morgan laws which now say that you can move negation through a quantifier by negating the component and switching the quantifier. And again one of them is provable intuitionistically:

try it!

theorem dm1_pred : ¬ (∃ x : A, PP x) ↔ ∀ x : A, ¬ PP x :=
begin
  constructor,
  assume h x p,
  apply h,
  existsi x,
  exact p,
  assume h p,
  cases p with a pa,
  apply h,
  exact pa,
end

While the other direction again needs classical logic:

try it!

theorem dm2_pred : ¬ (∀ x : A, PP x) ↔ ∃ x : A, ¬ PP x :=
begin
  constructor,
  assume h,
  apply raa,
  assume ne,
  apply h,
  assume a,
  apply raa,
  assume np,
  apply ne,
  existsi a,
  exact np,
  assume h na,
  cases h with a np,
  apply np,
  apply na,
end

Actually I had to use indirect proof raa twice to derive the left to right direction. Still our explanation we had given previously still applies: the existential statement ∃ x : A, ¬ PP x conatins information but the negated universal one ¬ (∀ x : A, PP x) deosn’t. Intuitively: knowing that not all students are stupid doesn’t give you a way to come up with a student who is not stupid.

4.7. Summary of tactics

Here is the summary of basic tactics for predicate logic:

	How to prove ?	How to use?
∀	assume h	apply h
∃	existsi a	cases h with x p
=	reflexivity	rewrite h rewrite← h

Note that the a after exsistsi can be any expression of type A, while h x p are variables.