Intuitionistic vs. Classical Logic — On the Law of Excluded Middle

Q: What is the difference between intuitionistic and classical logic

Classical logic accepts the law of excluded middle $A \lor \neg A$ and double-negation elimination $\neg\neg A \to A$ unconditionally, while intuitionistic logic generally does not. In intuitionistic logic, '$A$ holds' means giving a constructive witness for $A$, so when there is neither a witness for $A$ nor for $\neg A$, one cannot assert $A \lor \neg A$. The range of provable propositions is narrower than in classical logic.

Q: What is a constructive proof

A constructive proof is one that, when asserting existence, gives an actual method (a witness) for building the object. To prove $\exists x\,P(x)$ constructively, you must exhibit a concrete $x$ and a proof that it satisfies $P$. A proof of existence by contradiction ('assuming it does not exist leads to a contradiction') does not build the object and is generally not constructive.

Q: Why does a proof-checking kernel insist on constructive logic

Via the Curry–Howard correspondence, a constructive proof corresponds to a program, and from an existence proof one can extract a program that actually computes the object. Because proofs carry executable content, they suit machine verification and numerical computation. Also, by avoiding extra axioms like excluded middle and deriving only from explicitly stated axioms, one keeps transparent what the foundation of trust is.

Why be constructive

Basic (1st–2nd year university)

Goal of this page

Understand that the dividing line between classical and intuitionistic logic is the law of excluded middle $A \lor \neg A$, and grasp what a constructive proof is. Learn why a proof-checking kernel insists on being constructive.

1. Excluded middle as the dividing line

In classical logic, for any proposition $A$ one may unconditionally say "either $A$ or not $A$." This is the law of excluded middle. Classical logic also accepts double-negation elimination $\neg\neg A \to A$. Many mathematicians use these as a matter of course.

Definition: excluded middle and double-negation elimination

Law of excluded middle: $A \lor \neg A$.

Double-negation elimination: $\neg\neg A \to A$.

Classical logic has these as axioms (or derivable theorems). Intuitionistic logic generally does not.

Intuitionistic logic is the stance that does not accept these unconditionally. It regards "$A$ holds" as meaning: give a constructive witness for $A$. When there is as yet neither a witness for $A$ nor for $\neg A$, there is no ground to assert $A \lor \neg A$.

2. Constructive proof

Definition: constructive proof

A proof that, when asserting existence, gives an actual method (witness) to build the object is called a constructive proof. To prove $\exists x\, P(x)$ constructively, you must exhibit a concrete $x$ and a proof that it satisfies $P$. To prove $A \lor B$ constructively, you must specify which one holds.

Example: a non-constructive existence proof

The famous proof that "there exist irrationals $a, b$ with $a^b$ rational" splits on whether $\sqrt{2}^{\sqrt{2}}$ is rational or irrational, arguing by excluded middle that it must be one or the other. But it does not show which is actually true. This is a valid proof in classical logic, but since it does not pin down the object, it is not constructive.

An existence proof by contradiction — "assuming it does not exist leads to a contradiction, so it exists" — also does not build the object and is generally not constructive. The relation between constructive proof and proof by contradiction is also treated with examples in the existing article Proof: Constructive Proof.

Figure 1: The propositions provable intuitionistically form a proper subset of those provable classically. Excluded middle and double-negation elimination lie in the outer region.

3. Double negation as a bridge

Intuitionistic logic is weaker than classical logic, but not unrelated. Even intuitionistically, $A \to \neg\neg A$ is provable (the converse $\neg\neg A \to A$ is generally not). Moreover, any proposition provable classically can be "translated" into intuitionistic logic by inserting double negations appropriately (Glivenko's theorem, the Gödel–Gentzen translation). Classical logic is precisely intuitionistic logic plus excluded middle.

4. Why a proof-checking kernel insists on being constructive

Under the Curry–Howard correspondence, a constructive proof corresponds to a program. From a constructive proof of $\exists x\, P(x)$, one can extract a program that actually computes that $x$. Because the proof carries executable content, it suits machine verification and connection to numerical computation.

Another reason to be constructive is honesty of trust. By not implicitly using a strong principle like excluded middle, and deriving only from explicitly stated axioms and rules, one keeps transparent "what is taken as the foundation of trust." If needed, one can add excluded middle as an explicit axiom. This stance of "honestly making the foundation explicit" connects directly to the design philosophy of the de Bruijn criterion / TCB and constructive reals.

Summary

Key points

The dividing line is excluded middle $A \lor \neg A$ and double-negation elimination $\neg\neg A \to A$
Intuitionistically, "holds" = giving a constructive witness
A constructive proof actually builds the existing object; existence by contradiction is generally non-constructive
Classical logic = intuitionistic logic + excluded middle (translatable via double negation)
Constructive proofs correspond to programs and let you make the foundation of trust explicit

Frequently asked questions

What is the difference between intuitionistic and classical logic?

Classical logic accepts excluded middle $A \lor \neg A$ and double-negation elimination $\neg\neg A \to A$ unconditionally; intuitionistic logic generally does not. Intuitionistically, "$A$ holds" means giving a constructive witness, so without a witness one cannot assert $A \lor \neg A$. The range of provable propositions is narrower than classical.

What is a constructive proof?

One that, when asserting existence, gives an actual method (witness) to build the object. To prove $\exists x\,P(x)$ constructively you must exhibit a concrete $x$ and a proof it satisfies $P$. An existence proof by contradiction does not build the object and is generally non-constructive.

Why does a proof-checking kernel insist on constructive logic?

Via Curry–Howard, a constructive proof corresponds to a program, and from an existence proof one can extract a program that computes the object. Proofs carry executable content, suiting machine verification and numerical computation. Avoiding extra axioms like excluded middle and deriving only from explicit axioms keeps transparent what the foundation of trust is.