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.

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:

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:

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:

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:

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:

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:

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:

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.

The right side can be proved similarly:

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

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.

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.