… 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
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
Inductive True : Prop := I : True
True is a type of type
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.
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
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
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
B is a proposition of type
and that can be constructed (introduced/proved) given terms (proves) of
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
B by either proving
A and using
or_introl rule to introduce
A \/ B, or proving
B and using
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
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.
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
*) 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:
We can also prove a combined proposition by splitting a conjunction and using
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.
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.
Of course the type system should be rich enough to allow this.↩
This might be a good time to install
Coqand an IDE (whether its
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.↩