9. Propositional Logic in Lean

In Chapter 3, we considered the use of Lean as a programming language, and in Chapter 5 we saw that you can use Lean to define data types for things like propositional formulas and truth assignments, and thereby implement algorithms that act on these objects.

In this chapter, we will show how to represent propositional formulas directly in Lean’s underlying foundation. In this sense, we are using Lean’s foundation as an object language rather than a metalanguage for logic. To clarify the distinction, imagine implementing one programming language, such as Lisp, in another programming language, like C++. In this scenario, we can characterize Lisp as being the object language, that is, the one that is being implemented, and C++ as the metalanguage, the one that is carrying out the implementation. What we did in Chapter 5 is similar: we are used one logical system, Lean, to implement another one, propositional logic. One goal of this chapter is to clarify the sense in which Lean itself is a logical system, which is to say, its language can be used to state mathematical theorems and prove them. Propositional logic is only a starting point. In chapters to come we will see that Lean’s logical foundation is powerful and expressive enough to carry out almost any mathematical argument.

This means that Lean’s logical foundation serves as both a programming language and a mathematical language. Combining the two brings a number of benefits:

  • It allows us to specify the behavior of computer programs in the same language that we write them.

  • It allows us to prove, rigorously, that our computer programs are correct, which is to say, that they meet their specifications.

  • It allows us to enforce preconditions on our programs. For example, we can write functions whose input is required to be a positive integer, a requirement that is enforced statically, at compile time. Compiler optimizations can make use of this knowledge.

  • It allows us to compute with objects in our mathematical libraries.

  • It gives us ways of using computation in mathematical proofs.

Although we will not discuss it in this course, Lean also serves as its own metaprogramming language, which means that we can use Lean to develop automation that can help us construct programs and proofs. In that way, Lean becomes a self-extending system, meaning that we can improve its support for programming and theorem proving using the system itself.

9.1. Implication

In Lean, we can declare variables that range over propositions, and then use them to build more complicated propositions.

variable (p q r s : Prop)

#check True
#check False
#check p  q
#check p  q
#check p  q
#check p  q
#check ¬ p

Hovering over the symbols will give you options for typing them. Using \and, \or, \to, \iff, and \not will work.

In Lean, if p has type Prop, then a term t of type p is a proof of p. Lean’s proof language is essentially the same as its programming language, which means that we can write proofs the same way we write programs. Instead of using the identifier def, it is conventional to use the word theorem to name the proof of a proposition.

theorem foo : p  q  p  q :=
  fun hp hq => And.intro hp hq

theorem bar : p  q  q  p :=
  fun hp, hq => hq, hp

The expression after the := is sometimes called a proof term.

You can read more about writing proof terms in Theorem Proving in Lean 4. In this chapter, we will describe an alternative method of writing proofs, using tactics. A tactic proof is essentially a piece of metacode, a list of instructions that tells Lean how to construct the proof term. In Lean, we enter tactic mode with the keyword by.

example : p  p := by
  intro h
  apply h

Here the keyword example simply introduces an unnamed theorem (or definition). The intro tactic introduces the hypothesis and names it h. If you put the cursor on that line and check the Lean infoview in the editor, you will see the current state of the proof, that looks like this:

p q r s : Prop
h : p
 p

Think of this as a sequent, as described in the last chapter: it expresses that the current goal is to prove p, using the assumption h : p. In contrast to the sequent calculus we considered for natural deduction, here the hypothesis that p holds is labeled with the identifier h. You can use any identifier as a label. Also, in contrast with the sequent calculus for natural deduction, the variables p, q, r, and s are included, together with their type. Later on we will see that other kinds of data, like natural numbers, can be included as variables in the context. Notice also that in Lean, hypotheses like α : Type, p : Prop, n : Nat, and h : p are all possible, so the context can include variables ranging over data types, propositions, elements of the data types, and proofs (or assumptions) that the propositions hold.

In intro tactic implements the implication introduction rule of the natural deduction calculus. The apply tactic in the proof applies the hypothesis h to solve the goal. In this case, since h solves the goal exactly, we could write exact h instead. We could also write assumption, which tells Lean to look for any assumption in the context that solves the goal. This corresponds to the assumption rule in the natural deduction calculus.

The apply tactic can also be used to apply an implication.

example (h1 : p  q) (h2 : p) : q := by
  apply h1
  exact h2

In this example, applying p → q to the goal reduces the task of proving q to the task of proving p. Lean also provides a means of reasoning forward from hypotheses, using the have tactic:

example (h1 : p  q) (h2 : p) : q := by
  have h3 : q := h1 h2
  exact h3

Here the first line of the proof states an intermediate goal of proving q, which is achieved by applying h1 to h2. The result is named h3, which we can then use in the next line. We can leave out the information that h3 is a proof of q, because Lean can figure that out:

example (h1 : p  q) (h2 : p) : q := by
  have h3 := h1 h2
  exact h3

Defining h3 to be h1 h2 and then applying it is just the same as using exact h1 h2 directly to solve the goal, and that, in turn, amounts to constructing the proof h1 h2.

example (h1 : p  q) (h2 : p) : q := by
  exact h1 h2

example (h1 : p  q) (h2 : p) : q := h1 h2

9.2. Conjunction

There is a theorem in the library called And.intro that encodes the and-introduction rule in the natural deduction calculus, telling us that we can prove p ∧ q by proving each of p and q in turn.

theorem and_example : p  q  p  q := by
  intro hp
  intro hq
  apply And.intro
  . exact hp
  . exact hq

#print and_example

example : p  q  p  q :=
  fun hp hq => And.intro hp hq

After applying And.intro, the goal is split into two goals, one which requires us to prove p, and the other which requires us to prove q. Each of these is accomplished with the exact tactic. As you step through the proof, you can see the state change. The periods in each case serve to focus on the next goal, so that only that goal is visible in that part of the proof. Strictly speaking, they are not necessary; try deleting them to confirm that the proof still goes through. Still, they provide a nice way of making the structure of the proof manifest, and this, in turn, results in more robust proof scripts. The #print statement shows that the tactics have the effect of constructing a proof term. The subsequent example provides the proof term explicitly. In fact, the term makes it clear that introducing hp and hq and then applying And.intro is an unnecessary detour. The theorem we have proved is exactly And.intro.

example : p  q  p  q := And.intro

At this point, there are two tricks that are worth mentioning. First, at any point in a proof, you can solve the current goal with the admit tactic. You can prove any theorem at all using admit. It’s cheating, and the squiggly line the editor puts underneath the word tells you as much. But it is often a useful device when writing proofs, because it means you can temporarily close a goal to work on others, and then come back to it.

The other trick is to use the done tactic. The done tactic doesn’t do anything; it just declares that the proof is over. If the proof isn’t over, Lean gives you an error message, and the error message tells you exactly the remaining goals. So this gives you a way to mark the end of a proof in progress, so that you can easily monitor what is left to be done.

The natural way to use a conjunction h : p ∧ q in a hypothesis is to split it to the hypotheses hp : p and hq : q. This rule is commonly used in sequent calculi. There are various ways to do it. One is to use a destructuring have:

example : p  q  q  p := by
  intro h
  have hp, hq := h
  apply And.intro
  . exact hq
  . exact hp

Here the angle brackets are Lean’s anonymous constructor notation. You can type them with \< and \>. In this case, the have command tells Lean to match against whatever constructor matches the proposition, in this case, And.intro. Another option is to use the cases tactic, which matches the cases against the constructor:

example : p  q  q  p := by
  intro h
  cases h with
  | intro hp hq =>
    exact And.intro hq hp

example : p  q  q  p := by
  intro h
  cases h
  case intro hp hq =>
    exact And.intro hq hp

These are two slightly different formulations of the same proof. Notice that in the second variation we drop the keyword with and use the case tactic instead of the vertical bar.

Here are some examples of using the pattern-matching have with the ordinary one.

example (h1 : p  q) (h2 : p) : q := by
  have h3 : q := h1 h2
  exact h3

In the first example, the second have claims an auxiliary statement, r, and proves it with the term h2 hq. The third example shows that we can also prove the intermediate claim in tactic mode, using the keyword by.

The have statement is similar to a let statement that we have already seen when we used Lean as a programming language. In fact, using a let also works:

example (h1 : p  q) (h2 : q  r) : p  r := by
  let hp, hq := h1
  let hr : r := by
    apply h2
    exact hq
  exact And.intro hp hr

example (h1 : p  q) (h2 : q  r) : p  r := by
  let hp, hq := h1
  exact And.intro hp (h2 hq)

With both have and let, we can take the proofs to abbreviate the result of substituting the proof of r where we used hr, as in the last example above. There is a subtle difference between have and let: while the data in the let statement is available in the body of the statement after the let, a have only records the existence of an expression of the corresponding type. When we use a have, typically we only care that the corresponding fact has been proved, and the specifics of the proof are irrelevant. For that reason, have is more appropriate for proofs.

9.3. Disjunction

The theorem Or.inr in the library corresponds to the right introduction rule, which proves p ∨ q from p. The left introduction rule is given by Or.inl. We can carry out a proof by cases using either the theorem Or.elim or the cases tactic.

example : p  q  q  p := by
  intro h
  apply Or.elim h
  . intro hp
    apply Or.inr
    exact hp
  . intro hq
    apply Or.inl
    exact hq

example : p  q  q  p := by
  intro h
  cases h with
  | inl hp =>
    exact Or.inr hp
  | inr hq =>
    exact Or.inl hq

example : p  q  q  p := by
  intro h
  cases h
  case inl hp =>
    exact Or.inr hp
  case inr hq =>
    exact Or.inl hq

Notice that in contrast to casing on a conjunction, which results in one new goal and two new hypotheses, casing on a disjunction results in two new goals, each with one new hypothesis.

9.4. Negation

In Lean, ¬ p is defined to be p → False. For most purposes, the two expressions are interchangeable. This means that you can prove ¬ p by assuming p and deriving False, and if you have hp : p and hnp : ¬ p, then the result hnp hp of applying the first to the second is a proof of False. The following illustrates these ideas in action.

example (h : p  q) : ¬ q  ¬ p := by
  intro hnq hp
  apply hnq
  apply h
  apply hp

Here, intro hnp hp is equivalent to writing intro hnp followed by intro hp. Lean provides other means of dealing with negations. For example, the contradiction tactic finishes off a goal whenever the context contains a statement and its negation.

example (h1 : p) (h2 : ¬ p) : q := by
  contradiction

example (h1 : p  q) (h2 : ¬ p) : q := by
  apply Or.elim h1
  . intro hp
    contradiction
  . intro hq
    exact hq

In a similar way, the theorem absurd shows that anything follows from a statement and its negation. The first and second examples below are really the same: writing by exact t simply constructs the proof t.

example (h1 : p) (h2 : ¬ p) : q := by
  exact absurd h1 h2

example (h1 : p) (h2 : ¬ p) : q := absurd h1 h2

example (h1 : p  q) (h2 : ¬ p) : q := by
  apply Or.elim h1
  . intro hp
    exact absurd hp h2
  . intro hq
    exact hq

The contradiction tactic also works if the context contains False. Alternatively, casing on h : False finishes off a proof. Intuitively, there are no cases!

example (h : False) : p := by
  contradiction

example (h : False) : p := by
  cases h

The principles we have used before all fall within what is known as intuitionistic logic. Many mathematical arguments require classical logic, which is embodied in the law of the excluded middle. In Lean, if p is a proposition, em p is the principal p ∨ ¬ p.

example (h1 : p  q) : ¬ p  q := by
  apply Or.elim (Classical.em p)
  . intro hp
    apply Or.inr
    apply h1
    exact hp
  . intro hnp
    apply Or.inl
    exact hnp

example : ¬ ¬ p  p := by
  intro hnnp
  apply Or.elim (Classical.em p)
  . intro hp; exact hp
  . intro hnp
    contradiction

The following illustrate two other formulations of classical logic, allowing proof by cases and proof by contradiction.

example : ¬ ¬ p  p := by
  intro hnnp
  apply Classical.byCases
  . intro (hp : p)
    exact hp
  . intro (hnp : ¬ p)
    exact absurd hnp hnnp

example : ¬ ¬ p  p := by
  intro hnnp
  apply Classical.byContradiction
  intro (hnp : ¬ p)
  exact hnnp hnp

9.5. Miscellany

The rules for bi-implication are illustrated by the next two examples.

example (h1 : p  q) (h2 : p) : q := by
  have h3, h4 := h1
  apply h3
  exact h2

example (h1 : p  q) : q  p := by
  have h2, h3 := h1
  apply Iff.intro
  . exact h3
  . exact h2

It is worth keeping in mind that tactics serve to construct proof terms, and that you can often be more concise by writing the proof terms yourself, as in the following examples.

example : p  q  q  p :=
  fun h => Or.elim h (fun hp => Or.inr hp) (fun hq => Or.inl hq)

example (h1 : p  q) : ¬ q  ¬ p :=
  fun hnq hp => hnq (h1 hp)

You should think about these examples and how they work. One strategy for learning how to write proof terms is to name the theorems that you prove with tactics, and then use the #print command to print them out.