… 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.↩︎