Is the law of excluded middle true?

With the possibility of effective constructions provided by computers, the difference between classical logic and mathematics on the first hand, and constructive logic and mathematics on the second hand turns out to produce concrete effects: indeed, constructive arguments directly increase the computational content of proofs. For instance, to prove the existence of an object satisfying a predicate, a constructive logic requires the provision of an object, whereas in classical logic, it suffices to prove the absurdity of the non existence.

The law of excluded middle is the logical divide that allows both sides to be clearly split. Following Bishop, it can be described as a principle of omniscience: classical mathematicians are quite omniscient while constructive mathematicians know what they prove. Precisely, the law of excluded middle is the strongest principle of omniscience: if it was constructive, it would mean the decidability of the logic. Variants, which are weaker principles, are possible: they are called limited principles of omniscience.

From a constructive perspective, these principles of omniscience are mainly used in two contexts.

In these contexts, weakening the law of excluded middle to get a limited principle of omniscience is beneficial: the weaker the principle of omniscience, the more the Brouwerian counterexamples are and the more akin the constructive theory and the classical one are.

Thus, a limited principle of omniscience is based on a proposition that admits no constructive proof. A question remains open: how to determine whether a proposition has no constructive proof?

For both methods, the logic used is intuitionistic, possibly enriched with extra axioms. For instance, in Gentzen's sequent calculus LJ for intuitionistic logic, it is possible to prove that the law of excluded middle has no proof, as a direct consequence of the cut elimination theorem. When the underlying logic are identical between both methods, the second method is just a particular case of the first one. The interesting case is when the second method resorts to a logic enriched with an extra axiom, assumed to be consistent. Then, if the proposition has been proved to be false in the enriched logic, we can deduce by the completeness theorem (with respect to Kripke models) that it cannot be proved in the bare logic. This is exactly the way that we follow.

Indeed, in the post, we prove that a specific limited principle of omniscience is false, in Russian constructive mathematics. The principle is important since it is the one used by Bishop when he developed the foundations of constructive analysis. Russian constructive mathematics are based on intuitionistic logic enriched with a computability axiom. The extra axiom allows the halting problem for computable functions to be refuted. The proof then proceeds by reduction to the halting problem. It has been developed in the proof assistant COQ, which ensures that the logic is intuitionistic. More generally, the proof provides a framework to develop a theory for computability, based on an abstract model of computations.

Table of Contents

The limited principle of omniscience: a weak form of excluded middle

The law of excluded middle asserts that any proposition is either true or false. From a constructive perspective, the law corresponds to a maximal principle of omniscience: a mathematician could decide the truth of any proposition. In classical mathematics, that is mathematics developed by using classical logic, the law is an axiom. It is especially useful in situations where no constructive argument has been found. It is then possible to strengthen the hypotheses by considering two cases, given some relevant proposition \(p\):

  • a first case where \(p\) is true,
  • a second case where \(\neg p\) is true.

In constructive mathematics, which are developed by using intuitionistic logic, the law is not an axiom. Indeed, the preceding argument is considered as non-constructive, as long as the alternative cases cannot be constructively decided. This is the difference between a "mathematics of being" and a "mathematics of doing"2. Actually, if we require that all the functions over natural numbers definable in the logic are effectively computable, then we can show that the law of excluded middle is false and therefore must be rejected.

Precisely, we consider a weak form of the law of excluded middle, only valid for the existential quantification of decidable predicates over natural numbers. Bishop calls this instance of the law, due to Brouwer3, the limited principle of omniscience: a mathematician that could apply the principle would be omniscient only for a class of properties involving natural numbers. Intuitively, the principle has no constructive proof: we need to iterate over natural numbers to check the existence of a natural number satisfying the decidable predicate. Formally, if we admit the axioms underlying Russian constructive mathematics, we can even prove that the principle is false.

Refutation of the principle (in Russian constructive mathematics)

Russian constructive mathematics adhere to a fundamental principle dealing with computability, and corresponding to an abstract form of Church's thesis.

  • Enumerability: There is an enumeration \((f_i)_i\) of all partial functions that are definable over natural numbers.

That is the reason why these mathematics are also qualified as recursive. In the following, we give a concise presentation of the theory sufficient to prove that the limited principle of omniscience is false. Precisely, it is an explanation of the COQ script, where we try to emphasize its strong correspondence with a textual formalization. Note that the order of the definitions is not always respected.

Inductive definition of natural numbers

As in the standard library, the set \(\mathbb{N}\) of natural numbers is inductively defined as follows: a natural number is either zero or the successor of a natural number.

\[\small n \ ::=\ 0 \mid \mathtt{S} n \]
Inductive Nat : Set := Zero | Succ (n: Nat).

Limited principle of omniscience

The limited principle of omniscience, abbreviated as LPO, asserts that any predicate \(p\) satisfies the following property.

\[\small (\forall x.p(x) \vee \neg p(x)) \rightarrow ((\exists x. p(x)) \vee \neg(\exists x. p(x))). \]
Definition decidable (P : Prop) : Prop := P \/ ~P.
Definition existenceDecidability (p : Nat -> Prop): Prop :=
   (forall (n : Nat), (decidable (p n))) -> (decidable (exists (n : Nat), (p n))).
Definition LimitedOmniscience: Prop := (forall (p : Nat -> Prop), existenceDecidability p).

Reduction systems

The most interesting point deals with the computational model.

First, in COQ, all functions are total: they terminate for each given argument. However, we need to represent partial functions, which are undefined for some arguments. There are two cases, according to the decidability of the domain. If it is undecidable, then we model functions as their graphs, which are functional relations. If it is decidable, partial functions are encoded as total functions: a partial function from \(A\) to \(B\) becomes a total function from \(A\) to \(B_\bot\), where \(B_\bot\) is the pointed set equal to \(B + \{\bot\}\), \(\bot\) meaning undefined.

Definition functional (P : Nat -> Nat -> Prop) : Prop := forall (x y z : Nat), (P x y) /\ (P x z) -> (y = z).
Inductive Pointed (E : Set) : Set := Emb : E -> (Pointed E) | Bot : (Pointed E).

Second, the computational model is described from an abstract point of view, which essentially corresponds to a semantic perspective rather than a syntactic one. Each computation is interpreted as a sequence of reductions, either infinite, which means that the computation does not terminate, or finite, which means that the computation produces a result. The reduction function is defined over an abstract set of states, denoted by \(\Sigma\). The only property that we require is the decidability of the equality relation over \(\Sigma\).

Parameter State : Set.
Hypothesis StateEqualityIsDecidable : forall (s t : State), (decidable (s = t)).

More precisely, a computation over natural numbers is represented by three functions, given a set \(\Sigma\) of states:

  • an input function \(\alpha\) from \(\mathbb{N}\) to \(\Sigma\), which generates the initial state of the computation from the input,
  • a partial reduction function \(\rho\) over the state set \(\Sigma\),
  • a partial output function \(\beta\) from \(\Sigma\) to \(\mathbb{N}\), which gives the result.

A finality condition completes the definition: \(\rho\) is undefined if and only if \(\beta\) is defined.

Record Computation : Set :=
   buildComputation {
    input : Nat -> State;
    next : State -> (Pointed State);
    output : State -> (Pointed Nat);
    final : forall (s : State), ((next s) = (Bot State)) <-> (exists (y : Nat), (output s) = (Emb Nat y))

Convergence and divergence

The evaluation function induced by the reduction function \(\rho\) is inductively defined. A judgment \((\rho : s_1\ \Rightarrow_n\ s_2)\) means that state \(s_1\) reduces to final state \(s_2\) after \(n\) steps of reduction \(\rho\).

\[\small \begin{array}{lcllc} \text{[Last]} & \begin{array}{c} \rho(s) = \bot \\ \hline (\rho : s \ \Rightarrow_0\ s) \end{array} & \quad & \text{[Red]} & \begin{array}{c} (\rho(s_1) = s_2) \quad (\rho : s_2 \ \Rightarrow_n\ s_3)\\ \hline (\rho : s_1 \ \Rightarrow_{n+1}\ s_3) \end{array}\\ \end{array} \]
Inductive Eval (c : Computation) : State -> State -> Nat -> Prop :=
| Last : forall (s : State), ((c. (next) s) = Bot State) -> Eval c s s Zero
| Red : forall (s1 s2 s3: State) (n : Nat), ((c. (next) s1) = (Emb State s2)) -> (Eval c s2 s3 n) -> (Eval c s1 s3 (Succ n)).

Whereas the inductive interpretation of the preceding inference system expresses convergence, divergence requires a coinductive interpretation: in the following inference system expressing divergence judgments, infinite proofs become admissible, which is denoted by \(\nabla\) on the right side of the rule. A judgment \((\rho : s\ \Rightarrow_{\omega})\) means that state \(s\) diverges, that is indefinitely reduces following reduction \(\rho\).

\[\small \begin{array}{lcl} \text{[Co-Red]} & \begin{array}{c} (\rho(s_1) = s_2) \quad (\rho : s_2 \ \Rightarrow_{\omega})\\ \hline (\rho : s_1 \ \Rightarrow_{\omega}) \end{array} & \nabla \\ \end{array} \]
CoInductive Div (c : Computation) : State -> Prop :=
| CoRed : forall (s1 s2 : State), ((c. (next) s1) = (Emb State s2)) -> (Div c s2 ) -> (Div c s1).

Convergence and divergence are exclusive.

\[\small \forall s \in \Sigma. \neg ((\exists n \in \mathbb{N}, t \in \Sigma.(\rho : s\ \Rightarrow_n\ t)) \wedge (\rho : s\ \Rightarrow_{\omega})). \]

Moreover, the absence of convergence entails divergence.

\[\small \forall s \in \Sigma. \neg(\exists n \in \mathbb{N}, t \in \Sigma.(\rho : s\ \Rightarrow_n\ t)) \rightarrow (\rho : s\ \Rightarrow_{\omega}). \]
Lemma ConvergenceDivergenceExclude: forall (c : Computation), forall (s1 : State),
   ~((exists (n : Nat) (s2 : State), Eval c s1 s2 n) /\ (Div c s1)).
Lemma NoConvergenceImpliesDivergence: forall (c : Computation), forall (s1 : State),
   ~ (exists (n : Nat) (s2 : State), Eval c s1 s2 n) -> Div c s1.

Note that the second proposition requires a proof by coinduction. Indeed, the infinite divergence proof must be built as a solution to the following guarded system of equations, with variables \((X_s)_s\), where \(s\) ranges over states that are not convergent.

\[\small \begin{array}{rcll} X_s & = & \begin{array}{c} X_t \\ \hline (\rho : s\ \Rightarrow_{\omega}) \end{array} & (\rho(s) = t) \end{array} \]

A crucial observation sets a link between the limited principle of omniscience and the decidability of convergence, which paves the way towards the refutation. Assume LPO; then:

\[\small \forall s \in \Sigma. (\exists n \in \mathbb{N}, t \in \Sigma.(\rho : s\ \Rightarrow_n\ t)) \vee (\rho : s\ \Rightarrow_{\omega}). \]
Lemma LimitedOmniscienceImpliesConvergenceDecidability: LimitedOmniscience ->
   (forall (c : Computation) (s1 : State), (exists (n : Nat) (s2 : State), Eval c s1 s2 n) \/ ( Div c s1)).

The enumerability axiom

A computation \((\alpha, \rho, \beta)\) determines a relation \(R_{(\alpha, \rho, \beta)}\) that is functional as follows.

\[ R_{(\alpha, \rho, \beta)}(x, y) = \exists n \in \mathbb{N}, s \in \Sigma. (\rho : \alpha(x) \ \Rightarrow_n\ s) \wedge (\beta(s) = y). \]
Definition computedRelation (c : Computation) (x y : Nat) : Prop :=
   exists (n : Nat) (s : State), (Eval c (c. (input) x) s n) /\ ((c. (output) s) = (Emb Nat y)).
Lemma ComputationsDefineFunctions : forall (c : Computation), functional (computedRelation c).

The enumerability axiom can be formalized in two steps. First, a countable family of triplets \((\alpha, \rho, \beta)\) is assumed. It corresponds to a particular computational model, for instance Turing machines, \(\lambda\)-calculus or a language for generalized recursive functions. Thanks to the state abstraction, other models are possible.

\[\small \text{Computational model: } (m_i)_{i \in \mathbb{N}} \text{ such that } m_i = (\alpha_i, \rho_i, \beta_i). \]

Second the enumerability axiom asserts that any functional predicate \(P\) can be computed by some triplet \((\alpha_i, \rho_i, \beta_i)\) belonging to the computational model.

\[\small \text{Enumerability: } \forall P \text{ functional predicate}. \exists i \in \mathbb{N}. \forall x, y \in \mathbb{N}. P(x, y) \leftrightarrow R_{(\alpha_i, \rho_i, \beta_i)}(x, y). \]
Parameter model : Nat -> Computation.
Axiom Enumerability: forall (P : Nat -> Nat -> Prop),
   (functional P) -> exists (i : Nat), forall (x y : Nat), (P x y) <-> ((computedRelation (model i)) x y).

Refutation via the undecidability of the halting problem

Since the limited principle of omniscience entails the decidability of convergence, there is a close relationship between its refutation and the well-known undecidability of the halting problem, a problem defined as follows:

  • given partial function \(f_i\) (associated to \(R_{(\alpha_i, \rho_i, \beta_i)}\)) and natural number \(n\), decide whether \(f_i(n)\) terminates or not.

Actually, the refutation proceeds with a reduction to the halting problem.

First, we show the undecidability of the halting problem, stated as follows. Assume that for any \(i\) and any input \(x\), we can decide the termination of reductions \(\rho_i\) at \(\alpha_i(x)\). Then we get a contradiction.

\[ \small \neg( \forall i \in \mathbb{N}. \forall x \in \mathbb{N}. (\exists n \in \mathbb{N}, t \in \Sigma. (\rho_i : \alpha_i(x)\ \Rightarrow_n\ t)) \vee (\rho_i : \alpha_i(x)\ \Rightarrow_{\omega}) ). \]
Lemma ConvergenceDecidabilityIsAbsurd : ~(forall (i x : Nat),
   (exists (n : Nat) (s2 : State), Eval (model i) ((model i). (input) x) s2 n) \/ (Div (model i) ((model i). (input) x))).

The proof uses a standard diagonal argument. Define a functional relation \(\delta\) as follows. \[\small \delta(x, y) =( (\rho_x : \alpha_x(x)\ \Rightarrow_{\omega}) \wedge (y = 0)). \]

Definition diagonal (x y : Nat) : Prop := (Div (model x) ((model x). (input) x)) /\ (y = Zero).

Diagonal argumentInput \(d\)
\((\rho_d : \alpha(d)\ \Rightarrow_{*})\ /\ \delta(d, -)\)\(\bot / \top\) or \(\top / \bot\)

Termination of \((\rho_d : \alpha(d)\ \Rightarrow_{*})\) versus termination of \(\delta(d, -)\) (\(\top\) = termination, \(\bot\) = non termination).


  • CONV_DEC: Assume the decidability of convergence for the computational model \((m_i)_i\):

    \[ \small \forall i \in \mathbb{N}. \forall x \in \mathbb{N}. (\exists n \in \mathbb{N}, t \in \Sigma.(\rho_i : \alpha_i(x)\ \Rightarrow_n\ t)) \vee (\rho_i : \alpha_i(x)\ \Rightarrow_{\omega}). \]

    intro CONV_DEC.
  • ENUM: By the enumerability axiom and the definition of \(\delta\), there exists \(i\) such that for all \(x\) and \(y\) in \(\mathbb{N}\), we have

    \[\small ((\rho_x : \alpha_x(x)\ \Rightarrow_{\omega}) \wedge (y = 0)) \leftrightarrow (\exists n, s.((\rho_i : \alpha_i(x)\ \Rightarrow_n\ s) \wedge (\beta_i(s) = y))). \]

    assert (exists (i : Nat), forall (x y : Nat), (diagonal x y) <-> ((computedRelation (model i)) x y)) as ENUM.
    apply Enumerability.
    apply DiagonalIsFunctional.
    destruct ENUM as [i ENUM].
    unfold computedRelation in ENUM.
    unfold diagonal in ENUM.
  • Consider two cases, for convergence and divergence respectively on the diagonal (\(m_i\) with input \(i\)).
    destruct (CONV_DEC i i) as [TERM | NOTERM].
  • For each case, by using ENUM and the fact that convergence and divergence are exclusive, we get a contradiction. See the script for details.


Conclusion: the limited principle of omniscience is false in Russian constructive mathematics. Indeed, the principle implies the decidability of convergence, which implies the decidability of convergence for the computational model \((m_i)_i\): we get a contradiction by the preceding lemma.

Lemma LimitedOmniscienceIsAbsurd : ~LimitedOmniscience.
intro HLPO.
apply ConvergenceDecidabilityIsAbsurd.
apply LimitedOmniscienceImpliesConvergenceDecidability.

Conclusion: The limited principle of omniscience as a refined logical divide

Finally, Bishop's limited principle of omniscience is

  • accepted in classical mathematics, as the law of excluded middle, which is stronger,
  • rejected in Russian constructive mathematics, as the law of excluded middle, where it is compensated with Markov's principle.

Markov's principle can be stated as follows, for all predicates over natural numbers.

\[\small (\forall x. (p(x) \vee \neg p(x))) \rightarrow (\neg(\forall x. \neg p(x)) \rightarrow (\exists x. p(x))). \]
Definition constructiveExistenceDecidability (p : Nat -> Prop) : Prop :=
   (forall (n : Nat), (decidable (p n))) -> ~(forall (n : Nat), ~(p n)) -> exists (n : Nat), (p n).
Definition MarkovPrinciple : Prop :=
   forall (p : Nat -> Prop), (constructiveExistenceDecidability p).

It corresponds to a weak version of Bishop's limited principle of omniscience, as explained by the following table.

Intuitionistic tautology:
\(\neg(\exists x.p(x)) \rightarrow (\forall x.\neg p(x))\)
LPOIntuitionistic contrapositive:
\((\exists x.p(x)) \vee (\forall x.\neg p(x))\)\(\neg(\forall x.\neg p(x)) \rightarrow \neg\neg(\exists x.p(x))\)
Markov's principle (classical contrapositive) :
\(\neg(\forall x.\neg p(x)) \rightarrow \exists x.p(x)\)

(Implication from left to right)

These relations correspond to the following ones for convergence and divergence.

Intuitionistic tautology:
no convergence implies divergence
LPO:Intuitionistic contrapositive:
convergence or divergenceno divergence implies no non-convergence
Classical contrapositive :
no divergence implies convergence

(Implication from left to right)

More formally, assume Markov's principle. Then:

\[\small \forall s \in \Sigma. \neg(\rho : s\ \Rightarrow_{\omega}) \rightarrow (\exists n \in \mathbb{N}, t \in \Sigma.(\rho : s\ \Rightarrow_n\ t)). \]
Lemma MarkovPrincipleImpliesNoDivergenceEntailsConvergence: MarkovPrinciple ->
   (forall (c : Computation) (s1 : State), ~(Div c s1) -> (exists (n : Nat) (s2 : State), Eval c s1 s2 n)).

To conclude, there is also a third way, Bishop-style constructive mathematics, which follows a minimalist compromise:

  • no principle of omniscience, neither maximal, limited nor restricted as in the Markov's principle, be it in a positive form or a negative one,
  • and no other axioms, like the enumerability axiom that generates inconsistencies.

In this formal system, the limited principle of omniscience is nor proved nor disproved, as the law of excluded middle. Since it is based on a subset of the axioms of the other systems, all the propositions that are provable in this system are also provable in the other systems. Purely based on intuitionistic logic, Bishop-style constructive mathematics resort to new formulations of many concepts to get constructive proofs. Bishop's limited principle of omniscience is then used to relate constructive propositions to corresponding classical ones.



The article describes a formalization of computability theory without recourse to the irrelevant details of a computational model. This is the way that we have tried to follow in our formalization in COQ.

Constructive mathematics

  • Varieties of Constructive Mathematics, by Bridges and Richman (1987).

The article gives a complete overview of the different varieties of constructive mathematics, beyond the two species mentioned in the post (Bishop's school and Russian school).

Bishop-style constructive mathematics

  • Foundations of Constructive Analysis, by Bishop (1967).
  • A course in constructive algebra, by Mines, Richman and Ruitenburg (1988).

Both books contain an introductory chapter about constructive mathematics.


  • Two Security Criteria for Executing Mobile Code (your servitor's doctoral dissertation, 2003, in french)

    Chap. 1 deals with coinduction, from the construction of infinite proofs with guarded systems of recursive equations to the relationship with fixed points.

  • Coinductive Big-Step Operational Semantics, Information and Computation, by Leroy and your servitor (2009).

    Sect. 2 deals with coinduction and adds the relationship with COQ.

See my publications'page for details.


1 Bishop, in "Foundations of Constructive Analysis (1967)", p. 9.

2 This definition clearly sums up the opposition between constructive mathematics and classical mathematics.

  • Mines et al. in "A course in constructive algebra" (p. 1): "Following Hao Wang we may say that constructive mathematics is a "mathematics of doing" while classical mathematics is a "mathematics of being."
  • Kreisel in his review of "Wittgenstein's Remarks on the Foundations of Mathematics" (The British Journal for the Philosophy of Science, Vol. 9, No. 34 (1958), p. 146): "constructive aspects of Mathematics which Bernays calls, epigrammatically, a mathematics of doing (cf. also p. 118, §15) in contrast to a mathematics of being, or, more formally, an idealization of process as against an idealization of what is the case."
  • Wittgenstein (mentioned in Kreisel's citation): "For these people [having an applied mathematics without any pure mathematics] the centre of gravity of mathematics is found wholly in doing." (p. 118, §15).

3 Brouwer is the founder of intuitionism and one of the authors of the constructive interpretation of intuitionistic logic, with Heyting and Kolmogorov.

Last Updated 2015-08-19T18:08+0200. Comments or questions: Send a mail.