Posted on April 26, 2019

… or “the missing Law of Excluded Middle”.

First things first, Law of Excluded Middle or LEM is an axiom of logic that states that either some proposition A holds or its negation ¬A holds, there is no third choice. LEM is one of the core tenets of formal reasoning in “classical” branches of mathematics, and for me as a classically trained mathematician this is indeed a very natural way of thinking.

Recently, I got interested in the theory of programming languages. The discipline differs a great deal from functional analysis, probability theory or other familiar branches of mathematics, and learning required starting from the very basics, including proof theory and intuitionistic logic.

Honestly, this all did feel pretty daunting and unproductive given how much effort was required even for simple proofs. So I figured that doing exercises in code instead of pencil & paper should make it more fun.

Ahead are some basic pieces of intuitionistic logic accompanied by snippets of Coq code.

Propositions and types

Propositions are the foundation of logic. A proposition is a factual claim that in the context of intuitionistic logic can be proved only by providing an evidence or, in other words, by constructing a proof.

There is a well known correspondence between propositions and types. In short, each proposition can be represented as a special type1, and constructing a proof is equivalent to constructing an instance (or a term) of this type.

The idea of proofs as terms can be seen more clearly in how True and False are defined in Coq2.

Print True.
Inductive True : Prop :=  I : True

Print is a built-in command that prints a definition of a symbol. In this particular example we can see that True is a type of type Prop (where Prop is a basic type for propositions) and it has one constructor3, namely I. The fact that I is a nullary constructor reflects the idea that we don’t need anything to prove True, we can just provide I as a proof right away as can be seen below:

Example true_is_true: True.
Proof. exact I. Qed.

true_is_true is a proposition of type True and we prove this proposition by providing an instance I of required type using exact I command.

Similarly, False is defined as:

Print False.
Inductive False : Prop :=

There is no constructor for this type which again matches our intuition that we cannot prove falsehood. However, if we somehow get a proof of False we can prove any other proposition out of it. A standard function False_ind reflects this in its type:

Check False_ind.
False_ind : forall P : Prop, False -> P

Logical connectives

Complex propositions are built from simpler ones using logical connectives. One example of a connective is implication. It is built into Coq, but its form A -> B suggests the following reading: we can prove an implication if given a proof of A we can prove B.

Next logical connective is conjunction denoted by /\. It is not built-in, but rather defined in a standard library as:

Print and.
Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B

A conjunction of propositions A and B is a proposition of type and that can be constructed (introduced/proved) given terms (proves) of A and B.

Another logical connective is disjunction denoted by \/ and defined as:

Print or.
Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B

This one has two constructors which means we can prove a disjunction of A and B by either proving A and using or_introl rule to introduce A \/ B, or proving B and using or_intror rule.

Negation is a derived connective denoted by ~, which doesn’t have its own introduction rules, but is rather defined as:

Print not.
not = fun A : Prop => A -> False ; <----
     : Prop -> Prop

The part A -> False captures the idea that to prove a negation of A we need to prove that A is contradictory.

Biconditional or iff as another derived connective denoted by <-> and defined as:

Print iff.
iff = fun A B : Prop => (A -> B) /\ (B -> A) ; <----
     : Prop -> Prop -> Prop

All these connectives are regular types4. Currently, we have everything needed to start proving interesting theorems, but you are encouraged to explore the standard library further.

Simple proofs

Coq is designed to be used interactively. Just reading proofs without seeing the state of the proof in Coq’s output is rather laborious. I’ll show some intermediate output between (* and *) in the code samples below, but installing Coq and executing proofs step-by-step is strongly encouraged.

We start by proving two lemmas that state that when some proposition is a direct consequence of a disjunction then it is a direct consequence of any side of a disjunction. Let’s do the left side first.

Lemma or_impl: forall A B C: Prop,
    ((A \/ B) -> C) -> (A -> C).
Proof.
  (*
    This is a default state of the proof:
    1 subgoal (ID 1)

    ============================
    forall A B C : Prop, (A \/ B -> C) -> A -> C

    To actually get anything done we need to introduce
    the propositions and premises into the scope using
    intros command.
   *)
  intros A B C H_or H_A.
  (*
    1 subgoal (ID 6)

    A, B, C : Prop
    H_or : A \/ B -> C
    H_A : A
    ============================
    C

    The goal has changed: now we need to prove C using
    hypotheses in the scope.

    We see that there is a single way to prove C and it
    is by proving A \/ B from H_or.

    Since we have a proof of A in a form of H_A we can
    prove A \/ B using or_introl constructor. The resulting
    term is named Pf_or.
   *)
  pose (Pf_or := or_introl H_A: A \/ B).
  (*
    1 subgoal (ID 10)

    A, B, C : Prop
    H_or : A \/ B -> C
    H_A : A
    Pf_or := (or_introl H_A : A \/ B) : A \/ B
    ============================
    C

    Now we can prove C from Pf_or and H_or by modus ponens.
   *)
  apply H_or in Pf_or as Pf.
  (*
    1 subgoal (ID 13)

    A, B, C : Prop
    H_or : A \/ B -> C
    H_A : A
    Pf_or := (or_introl H_A : A \/ B) : A \/ B
    Pf : C
    ============================
    C
   *)
  exact Pf.
Qed.

The right side can be proved similarly:

Lemma or_impr: forall A B C: Prop,
    ((A \/ B) -> C) -> (B -> C).
Proof.
  intros A B C H_or H_B.
  pose (Pf_B := or_intror H_B : A \/ B).
  apply H_or in Pf_B as Pf.
  exact Pf.
Qed.

We can also prove a combined proposition by splitting a conjunction and using or_impl and or_impr to prove each side separately:

Lemma or_implr: forall (A B C: Prop),
    ((A \/ B) -> C) -> ((A -> C) /\ (B -> C)).
Proof.
  intros A B C H_or.
  split.
  (*
    A, B, C : Prop
    H_or : A \/ B -> C
    ============================
    A -> C

    subgoal 2 (ID 10) is:
    B -> C
   *)
  - exact (or_impl A B C H_or).
  - exact (or_impr A B C H_or).
Qed.

This lemma will come in handy when we try to prove a theorem about the law of excluded middle in the next section.

We don’t need no LEM

The theorem we’re going to prove can be written as \(\neg \neg (A \lor \neg A)\). Although, at first it may seem like gobbledygook, it has a very clear and profound meaning. The \(A \lor \neg A\) part is exactly LEM, and the whole theorem can be read as:

Intuitionistic logic /does not/  /refute/ the /Law of Excluded Middle/.
                        ¬            ¬                   A∨¬A

Note that “does not refute” is not the same as “asserts”. In fact, double negation elimination \(\neg \neg A \implies A\) is an axiom of classical logic and equivalent to LEM.

The annotated proof in Coq is given below. Although, the proof may seem rather straightforward, especially with or_implr lemma proved previously, it definitely didn’t seem trivial to me and took some time to figure out all the necessary pieces. So, hopefully someone will find it interesting.

Theorem not_refuting_LEM: forall (A: Prop), ~~(A \/ ~A).
Proof.
  intro A.
  (*
    1 subgoal (ID 5)

    A : Prop
    ============================
    ~ ~ (A \/ ~ A)

    We cannot do anything with negation as it is.
    To proceed we need to unfold it, according to
    the definition.
   *)
  unfold not.
  (*
    A : Prop
    ============================
    (A \/ (A -> False) -> False) -> False

    Not we can bring the left hand side of
    the implication into scope.
   *)
  intro H_refuteLEM.
  (*
    1 subgoal (ID 7)

    A : Prop
    H_refuteLEM : A \/ (A -> False) -> False
    ============================
    False

    We can furter break down H_refuteLEM into 2
    pieces using or_implr lemma and destruct
    tactic.
   *)
  apply or_implr in H_refuteLEM.
  (*
    1 subgoal (ID 8)

    A : Prop
    H_refuteLEM : (A -> False) /\ ((A -> False) -> False)
    ============================
    False
   *)
  destruct H_refuteLEM as [H_refuteA H_refuteNotA].
  (*
    1 subgoal (ID 14)

    A : Prop
    H_refuteA : A -> False
    H_refuteNotA : (A -> False) -> False
    ============================
    False

    Here we can use H_refuteA to prove the right hand
    side of H_refuteNotA.
   *)
  apply H_refuteNotA in H_refuteA as Pf_False.
  (*
    1 subgoal (ID 17)

    A : Prop
    H_refuteA : A -> False
    Pf_False : False
    H_refuteNotA : (A -> False) -> False
    ============================
    False
   *)
  exact Pf_False.
Qed.

Footnotes

  1. Of course the type system should be rich enough to allow this.↩︎

  2. This might be a good time to install Coq and an IDE (whether its Coq-IDE or Proof General).↩︎

  3. Constructors are also called introduction rules. Indeed, constructors can be thought of as rules that introduce a term of specific type given some other terms.↩︎

  4. Here implication and inductive types are basic building blocks. Other connectives are defined in terms of them. But this is not the only way to axiomatize logic; there is a handful others with different basic connectives, axioms and inference rules.↩︎