All Posts
Constructive Mathematics and Diaconescu's Theorem in Coq
Math Classes Should Be Less Useful
A Formal Introduction to Models of Computation in Coq (Part 3)
A Formal Introduction to Models of Computation in Coq (Part 2)
A Formal Introduction to Models of Computation in Coq (Part 1)
Why Prolog?

Constructive Mathematics and Diaconescu's Theorem in Coq

Constructive mathematics is fantastic. By proving propositions constructively, we obtain algorithms to solve our problems "for free" along with the proof that the algorithm works. If we use a program such a Coq to write our proofs, we not only theoretically have an algorithm, but we can literally extract the source code for the algorithm and use it in other programs, with a guarantee that it's 100% correct. These algorithms aren't always practical, as it's often more difficult to prove the correctness of optimized algorithms, but sometimes the extracted code can be quite useful.

Even mathematicians who regularly use non-constructive methods of proof generally prefer direct, constructive proofs. Not only do such proofs often have practical benefits, but they also tend to clearer. A common mistake among mathematics students, of which I certainly also have been guilty, is unnecessary contradiction; either literally, in that the contradiction goes unused, or in that there is a simpler direct proof.

I should note here that there are several forms of constructivism; to be precise, what I mean here is the Calculus of Inductive Constructions.

This article will be able the interaction between two laws that lead to non-constructive proofs, the Axiom of Choice and the Law of the excluded middle, and we'll formalize a theorem showing that the Axiom of Choice implies the Law of the excluded middle in Coq. Therefore, there will be some Coq code interspersed throughout the article; this proof is fairly simple, so it should be mostly accessible to mathematically sophisticated readers.

If you're curious about constructive mathematics, I suggest you watch Five Stages of Accepting Constructive Mathematics; not because it's any sort of in-depth convincing argument for constructive mathematics (though there is some of that), but it's entertaining.

Note: all the code for this is available on GitHub.

Law of the excluded middle

The Law of the excluded middle is widely accepted in mathematics.

One of the main methods of non-constructive proof is via contradiction, though we should note there are two forms of contradiction, one is constructive; the other is not. For some proposition \(P\), we can prove \(\neg P\) as follows:

  1. Assume \(P\).
  2. Prove \(\text{False}\).
  3. Conclude \(\neg P\).

This version is allowed because it is the definition of \(\neg P\); that is, in Coq:

Definition not (P : Prop) := P -> False.

That is, \(P\) implies false. This is a perfectly constructive form of contradiction. In fact, it's the only way to prove something is false.

The other version of contradiction is trying to prove that \(P\) hold as follows:

  1. Assume \(\neg P\).
  2. Prove \(\text{False}\).
  3. Conclude \(P\).

This is not constructive. We've shown that \(\neg P\) is not true; but this gives us no information about how to actually build a proof (equivalent, a value, via Curry-Howard), for \(P\).

However, if we assume the law of excluded middle, that is, for any proposition \(P\), either \(P \vee \neg P\), the both forms of contradiction become acceptable. We can state this as follows in Coq:

Theorem excluded middle : forall (P : Prop), P \/ ~P.

Naturally, such a law ruins the "constructiveness" of our proofs. Therefore, it is generally not allowed in Coq, though it may be added as an axiom.

Negation of Law of the excluded middle

It's important to note that, while we generally do not accept the law of excluded middle, we also do not accept it's negation, that is, it is not the case that not every proposition is true or false, or \(\neg \neg (P \vee \neg P)\). Interestingly, this is actually a provable theorem in Coq. While the proof itself is not terribly interesting, it's probably good to read this section if you're unfamiliar with Coq. If you are, then the below proof is probably suitable:

Lemma ex_middle_neg : forall (P : Prop), ~(~(P \/ ~P)).
Proof.
intuition.
Qed.

That probably seems like a bit of a "cheat" if you're unfamiliar with Coq, though it is a valid proof. Here intuition means that Coq will automatically search for a proof for us, which generally works if the goal is not too hard to prove.

I'll now give a much more in depth proof that goes through all the little details, and is maybe a easier to understand. We start by introducing our variables, in this case, just the proposition \(P\).

Lemma ex_middle_neg : forall (P : Prop), ~(~(P \/ ~P)).
Proof.
intro P.

We then unfold the definition of not, that is, as it is written above: not P is really just a function from P to False. So what we wish to prove is that, if ~(P \/ ~P) were true, then False is also true—a contradiction. Then we must suppose that ~(P \/ ~P) holds, which we do by introducing the proof for it as a variable.

unfold not.
intros prf.

We now introduce another assumption into our proof, which we'll prove later. This is essentially make a little sub-claim in our proof. We assume that P is false; under this assumption, it's quite easy to prove False, because prf is of type P \/ ~P -> False. We can write this as follows:

cut (P -> False).
- intro assum. (* Here assum : ~P *)
exact (prf (or_intror assum)).

Here or_intror is how we build a proof that A \/ B is true, either by providing a proof of A, via or_introl (standing for "or intro left"), or providing a proof of B, via or_intror (standing for "or intro right"). Note that the type of prf (or_intror assum) is False, so this is exactly what we wanted to prove. We assert this using the exact tactic.

Of course, we don't get to just assume this for free; we now must prove that P is false. Luckily, this is fairly simple, we just assume P, and note that prf lets us immediately conclude False.

- intro assum. (* Here assum : P *)
exact (prf (or_introl assum)).
Qed.

This completes the proof.

Axiom of Choice

If you're not familiar with the Axiom of Choice, it's probably something that hasn't even occurred to you that it would need to be an axiom. Essentially, the axiom of choice says, given any collection of sets, I can (uniquely) choose one element from each set. There's many formulations of the axiom, but we'll use one that plays nice with Coq.

More precisely, given a set A the Axiom of Choice gives a choice function for the set A. That is, a function which, given a subset of A, picks one element from the subset and returns it. Naturally, the set must be inhabited for this property to make sense. We encode this in Coq as two separate axioms: one states the existence of the choice function, the other states the property that it chooses from among the subset.

Variable choice : forall {A : Set}, A -> Ensemble A -> A.
Variable choice_prop : forall {A : Set} (x : Ensemble A) (v : A), Inhabited x -> In x (choice A v x).

Note that in Coq's standard library, sets are called "ensembles." Presumably this is due to the Coq being developed in France, as the French word for "set" is "ensemble."

The above definitions are not exactly the same as what we said earlier, because we need to protect ourselves from introducting inconsistencies into our logic. For example, had we written:

Variable choice : forall {A : Set}, Ensemble A -> A.
Variable choice_prop : forall {A : Set} (x : Ensemble A), In x (choice A x).

We would have the issue mentioned above, that we can pick an element from x even if x has no elements!

Variable choice_prop : forall {A : Set} (x : Ensemble A), Inhabited x -> In x (choice A x).

We could try to fix this by require that x be inhabited; this fixes this particular issue, but we can still use choice to prove False by choosing an element from the empty set, where the universal type is False:

Lemma inconsistent : False.
Proof.
exact (choice False Empty_set).
Qed.

We could require that we only choose from inhabited sets, which seems like a reasonable requirement and does work. However, it's somewhat simpler to just require that the type A be inhabited at all, as follows:

Variable choice : forall {A : Set}, A -> Ensemble A -> A.

This fixes all of our issues, and allows us to select from sets so long as the type is inhabited. Intuitively, if we give it the empty set, we simply select this default element we provide. This poses no issues for choice_prop, because choice_prop still requires that the particular set we apply it to be inhabited.

The Theorem

Now that we've set up all the necessary machinery, we may prove Diaconescu's Theorem. Diaconescu's Theorem states the following: if we accept the Axiom of Choice, then we may conclude for any proposition \(P\) that either \(P\) holds or \(P\) does not hold. In Coq, writing Variable choice ... as we did above assumes the Axiom of Choice, so the statement of the theorem is precisely the statement of the Law of the excluded middle, which we can now prove.

Theorem diaconescu : forall (P : Prop), P \/ ~P.

The Proof

Before we do so, we first define two sets, which, at first glance, seem unrelated. Note in Coq, a set (ensemble) is defined as a function from members of a base Set to Prop, which can be thought of similarly to a boolean value: either true or false. That is, a set tells us, given a value, whether the value is in the set. Sets are therefore defined by their membership. This gives us some intuition for why we can't choose elements from arbitrary sets: we would have to "search" the space of A, which may be infinitely, and our algorithm may never terminate. Therefore, we need someone to provide us with a choice function. Some types, like nat, the type of natural numbers, have natural choice functions, but this is not true in general, because it would require that we be able to produce a value of any type out of "thin air".

Coq assumes the extensionality axiom for us as well:

Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.

where Same_set is:

Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B.

Note that the axiom of specification is implicitly assumed here, because we may construct a "subset" of a type A given any proposition about the elements of A.

We define the two sets \(U\) and \(V\) as follows for some proposition \(P\).

\(U = \{ x \in \{ 0,1 \} : x = 0 \vee P \}\)

\(V = \{ x \in \{ 0,1 \} : x = 1 \vee P \}\)

Note that \( P \) is independent of \( x \), so if \(P\) is true, then both sets contain every element of \(\{0,1\}\).

We'll represent the set \(\{0,1\}\) by the type bool in Coq, because the two are isomorphic and Coq has built-in support for boolean values. We now need to prove some intermediate facts about these two sets, starting with the fact that they are both inhabited. This is quite obvious, but Coq needs a proof of it.

First we define the sets U and V, given a proposition P, recalling that sets are defined to be the function that determines their members.

Definition U (P : Prop) (x : bool) := x = true \/ P.
Definition V (P : Prop) (x : bool) := x = false \/ P.

Lemmas

We must now prove some basic lemmas about the two sets: that they are inhabited, and that U = V when P holds.

Because because inhabited is an existential claim, we must prove the existence of an element that U contains. This is done by saying exists true, because U always contains true. The rest follows from the definition.

Lemma U_inhabited : forall {P : Prop}, Inhabited (U P).
Proof.
intuition.
exists true. (* Here we state that "true" is in U *)
unfold U, In.
intuition.
Qed.

The proof for V is identical, but with false instead of true, so I've omitted it. Note all the code is available in the GitHub repository.

We also need one other important fact about U and V: if P is true, then both sets contain both true and false (or \(0\) and \(1\)). We formalize this as follows. If P holds, then every boolean (in particular, true and false), are contained in U, and similarly for V. This holds easily by intuition, so we just let Coq build the proof term for us.

Lemma P_imp_in_U : forall {P : Prop}, P -> forall (x : bool), In (U P) x.
Proof.
intuition.
unfold U, In.
intuition.
Qed.

Using these facts and extensionality, we can now prove that, as we stated above, if P holds, then U = V. Recall the definition of Extensionality_Ensembles and Same_set from above, which simply says that if \(U \subseteq V\) and \(V \subseteq U\), then \(U = V\). The definition of subset, or Included, as it is called in Coq, is:

Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x.

which corresponds to the usual set-theoretic discussion. Of course, since if P is true, then both sets contain all booleans, this is fairly easily proved using

Lemma P_imp_full : forall {P : Prop}, P -> U P = V P.
Proof.
intuition.
apply Extensionality_Ensembles.

unfold Same_set, Included.
intuition.
- now (apply P_imp_in_V).
- now (apply P_imp_in_U).
Qed.

The Main Theorem

We are now ready to prove the main theorem, and we start by applying the choice function to the sets U and V.

Theorem diaconescu : forall (P : Prop), P \/ ~P.
Proof.
intuition.

pose proof choice_prop bool (U P) true U_inhabited as fu.
pose proof choice_prop bool (V P) true V_inhabited as fv.

Let's consider the possibilities here. Let's call the choice function \(f\): by the definition of the choice function, we have \(f(U) \in U\) and \(f(V) \in V\). Essentially, there's two cases here: either \(f(U) = f(V)\), or \(f(U) \neq f(V)\). If \(f(U) \neq f(V)\), then \(P\) is false, because if it were true, then \(U = V\). To do this analysis, we use the inversion tactic, which takes a hypothesis \(H\), and decomposes it, essentially tells us if \(H\) is true, then some other \(I\) must also be true. For example, if \( 0 + x = 0 \), then \( x = 0 \); here \(H\) would be \(0 + x = 0\) and \(I\) would be \(x = 0\). When we apply this to fu and fv, defined above, we get that either fu = true or P and either fv = false or P. There are the following cases:

  • When \(f(U) = 0\) and \(f(V) = 1\).
  • When \(f(U) = 0\) and \(P\).
  • When \(P\) and \(f(V) = 0\).
  • When \(P\) and \(P\).

Note the last two cases can be condensed into just one, because they both include \(P\) which is the thing we are trying to prove.

Let's first consider the case that \(f(U) \neq f(V)\). Recall we wish to show P \/ ~P, in this case, we want to show that ~P, so we select the right side to prove, and assume P, as usual. Then by P_imp_full, we know that U V = V P. But then the choice function should have select the same element, because they are the same set! So then \(f(U) = f(V)\), but we know this is not true, because false is not true. Because this is a contradiction, P must be false in this case.

- right.
intros prf. (* Here prf : P *)
pose proof P_imp_full prf as eq_prf. (* Here eq_prf : U P = V P *)
now (rewrite eq_prf, H0 in H). (* H0 : choice (V P) = false *)

The next two cases are that \(f(U) = 0\) and \(P\) and then just that \(P\). These are quite simple, because both include the proof of \(P\), so we can prove them both as follows, finishing the proof.

- now left.
- now left.
Qed.

Consequences

I generally think of math as a sort of game (opr meta-game, perhaps), where we design systems using different rulesets and see how interesting they are, the object of the game being to design the most interesting system. In this view, the Axiom of Choice, like any other rule, may be part of some rulesets, and not part of others. I tend to think that not using the Axiom of Choice makes the resulting systems more interesting, but of course there are trade-offs.

At first glance the Axiom of Choice seems extremely obvious, so obvious that only a pedant would even bother to state it in the first place, it actually ends up having many unintuitive consequences. For example, the Axiom of Choice implies that all sets can be well-ordered, even the real numbers, which is indeed quite strange. It also can be used to show the Banach-Tarski paradox.

However, not taking the Axiom of Choice also produces strange results: for example, without the Axiom of Choice, we cannot prove that all vector spaces have a basis, as the two statements are equivalent.

But, as we have just shown, there is yet another unintuitive consequence of the Axiom of Choice: the Law of the excluded middle. You may protest that the law of the excluded middle is, in fact, extremely intuitive. However, consider what it means in a constructive context, like Coq. We consider a proposition to be true when we have a proof of it, and we have a proof of something when we are able to make a value of that type. The Law of the excluded middle does something strange then: either the proposition is false, or it conjures up a proof for us, regardless of what we want to prove. Naturally, this consequence is the reason that the Axiom of Choice and law of the excluded middle are generally not used in Coq. Really, it all boils down to the fact that it's weird to say "\(X\) exists, but I can't show it to you."

Last updated: 18.09.2019
Older

This website is written in Prolog