5. Logic

In the course of Chapter 2 and Chapter 4 we learned the “grammar” of the various logical symbols, like \(\land\), \(\forall\) and \(\to\). In those chapters, logical reasoning took place in fairly concrete mathematical situations: problems about equalities and inequalities in the natural numbers, the rational numbers, and so on.

In this chapter, we take a more abstract point of view, studying the process of logical reasoning in its own right. The central concept is the concept of logical equivalence: transformations to the logical structure of a statement which are always valid, because the “before” and “after” can be deduced from each other using only abstract logical reasoning, not anything specific to the mathematical situation at hand.

The most important logical equivalences are those covered in the final section of the chapter, Section 5.3. These are logical equivalences which move a negation symbol (\(\lnot\)) to a deeper position in a logical statement. Taken together, these transformations give us a way to delay and minimize our encounters with \(\lnot\), the most awkward logical symbol.

5.1. Logical equivalence

5.1.1. Example

If you abstract away the numbers, definitions, equations and inequalities, you are left with pure logic problems. And the pure logic tactics like obtain, apply, constructor, and so on can still be used.

example {P Q : Prop} (h1 : P ∨ Q) (h2 : ¬ Q) : P := by
  obtain hP | hQ := h1
  · apply hP
  · contradiction

It’s hardly worth trying to write proofs like this in words. The \(P\) and \(Q\) are abstract propositions (Prop), and this is just a game of manipulation.

example (P Q : Prop) : P → (P ∨ ¬ Q) := by
  intro hP
  left
  apply hP

5.1.2. Example

We can think of propositional logic statements in the following way. Imagine that each variable, like \(P\), can be either “true” or “false”. There are fixed rules for how truth and falsehood combine under logical operations. For example, \(P \land Q\) is true if \(P\) and \(Q\) are both true, and otherwise it is false. We can record this information in a table called a truth table:

P	Q	(P ∧ Q)
true	true	true
false	true	false
true	false	false
false	false	false

Likewise here is the rule for \(\lnot P\): it is the opposite of \(P\).

P	¬P
true	false
false	true

Using the rules for the basic operations, we can work out the truth table for a more complex statement step by step from the operations it’s composed of. For example, here’s how to find the truth table for \(\lnot(P \land \lnot Q)\): first compute the table for \(\lnot Q\), then for \(P \land \lnot Q\), then finally for \(\lnot(P \land \lnot Q)\).

P	Q	¬Q	(P ∧ ¬Q)	¬(P ∧ ¬Q)
true	true	false	false	true
false	true	false	false	true
true	false	true	true	false
false	false	true	false	true

You should practise doing this by hand, but the Lean command #truth_table will also do it automatically.

#truth_table ¬(P ∧ ¬ Q)

That’s how I generated these pictures! The #truth_table command was written by Joseph Rotella with contributions from Ryan Edmonds; both are students at Brown University.

5.1.3. Exercise

Here are the rules for the remaining basic logical operations:

P	Q	(P ∨ Q)
true	true	true
false	true	true
true	false	true
false	false	false

P	Q	(P → Q)
true	true	true
false	true	true
true	false	false
false	false	true

P	Q	(P ↔ Q)
true	true	true
false	true	false
true	false	false
false	false	true

Problem

Work out the truth table for \(P \leftrightarrow (\lnot P \lor Q)\).

Then check it in Lean.

5.1.4. Example

Two propositional logic formulas are said to be logically equivalent, if the “if and only if” between them can be proved in Lean. For example,

Problem

Show that \(P \lor P\) is logically equivalent to \(P\).

example (P : Prop) : (P ∨ P) ↔ P := by
  constructor
  · intro h
    obtain h1 | h2 := h
    · apply h1
    · apply h2
  · intro h
    left
    apply h

An important caveat here is that there is still one logic tactic which hasn’t been introduced yet (see Section 5.2). So there are some pairs of propositional logic formulas which are logically equivalent in a way that we can’t yet demonstrate.

5.1.5. Example

Problem

Show that \(P \land (Q \lor R)\) is logically equivalent to \((P \land Q) \lor (P \land R)\).

This is a long one. I’ve done the first direction and left the second for you.

example (P Q R : Prop) : (P ∧ (Q ∨ R)) ↔ ((P ∧ Q) ∨ (P ∧ R)) := by
  constructor
  · intro h
    obtain ⟨h1, h2 | h2⟩ := h
    · left
      constructor
      · apply h1
      · apply h2
    · right
      constructor
      · apply h1
      · apply h2
  · sorry

We will not prove it in this book, but two statements in propositional logic are logically equivalent if and only if they have the same truth table. For example, compare the output of these two Lean commands:

#truth_table P ∧ (Q ∨ R)
#truth_table (P ∧ Q) ∨ (P ∧ R)

5.1.6. Example

We can also perform this kind of abstract logic game when quantifiers are involved.

example {P Q : α → Prop} (h1 : ∀ x : α, P x) (h2 : ∀ x : α, Q x) :
    ∀ x : α, P x ∧ Q x := by
  intro x
  constructor
  · apply h1
  · apply h2

Here the \(P\) and \(Q\) are predicates, abstractions of a statement involving a variable (here called \(x\)). Statements about quantified predicates are sometimes referred to as first-order logic.

Here’s another example of abstract logical reasoning involving quantifiers.

example {P : α → β → Prop} (h : ∃ x : α, ∀ y : β, P x y) :
    ∀ y : β, ∃ x : α, P x y := by
  obtain ⟨x, hx⟩ := h
  intro y
  use x
  apply hx

The concept of logical equivalence also still makes sense in this setting.

Problem

Show that \(\lnot\exists x, P(x)\) is logically equivalent to \(\forall x, \lnot P(x)\).

example (P : α → Prop) : ¬ (∃ x, P x) ↔ ∀ x, ¬ P x := by
  constructor
  · intro h a ha
    have : ∃ x, P x
    · use a
      apply ha
    contradiction
  · intro h h'
    obtain ⟨x, hx⟩ := h'
    have : ¬ P x := h x
    contradiction