… 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 type^{1}, 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 `Coq`

^{2}.

```
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 constructor^{3}, 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 types^{4}. 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

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

This might be a good time to install

`Coq`

and an IDE (whether its`Coq-IDE`

or`Proof General`

).↩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.↩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.↩