# 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.

- Brouwerian counterexamples: to show that a proposition has no constructive proof, it suffices to constructively prove that it implies the principle, which has no constructive proof.
- Development of a constructive theory replacing a classical theory:
for each classical theorem \(P\), develop "a constructive substitute
\(Q\), which is a constructively valid theorem \(Q\) implying \(P\) in the
classical system by a more or less simple argument based on the […]
principle of omniscience"
^{1}.

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?

- First method: show that the proposition has no proof.
- Second method: prove that the proposition is false.

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 Brouwer^{3}, 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 \]### Limited principle of omniscience

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

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.

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

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.

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} \]| 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} \]| 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}). \]~((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:

(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). \]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). \]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}) ). \](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)). \]

Diagonal argument | Input \(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).

**Proof**

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

**Qed.**

**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.

Proof.

intro HLPO.

apply ConvergenceDecidabilityIsAbsurd.

intros.

apply LimitedOmniscienceImpliesConvergenceDecidability.

auto.

Qed.

## 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))). \](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))\) | ||

LPO | Intuitionistic 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 divergence | no 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)). \](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.

## Bibliography

### Computability

- Church's Thesis Without Tears, by Richman. The Journal of Symbolic Logic (Vol. 48, No. 3, 1983), pp. 797-803.

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.

### Coinduction

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

## Footnotes:

^{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.