Law of Excluded Middle

Definition

The law of excluded middle (LEM) is a principle in classical logic stating that for any proposition $P$, either $P$ is true or its negation $\neg P$ is true.

$P\vee \neg P$

In Type Theory, this corresponds to the type:

${\prod }_{P:\text{Prop}}P+\neg P$

Status in Different Logical Systems

Classical Logic

In classical logic, the law of excluded middle is a fundamental axiom. Every proposition is decidedly either true or false.

Intuitionistic Logic

In Intuitionistic Logic, the law of excluded middle is not accepted as a general principle. A proof of $P\vee \neg P$ requires either a constructive proof of $P$ or a constructive proof of $\neg P$.

Constructive Mathematics

In Constructive Mathematics, LEM is rejected because it asserts the existence of a truth value without providing a method to compute which alternative holds.

Relationship to Other Principles

The law of excluded middle is equivalent to several other classical principles:

• Double negation elimination: $\neg \neg P\to P$
• Peirce’s Law: $((P\to Q)\to P)\to P$
• De Morgan’s laws (in their classical form)

In Homotopy Type Theory

In Homotopy Type Theory, LEM can be consistently added as an axiom without contradicting univalence, though it makes the type theory non-constructive.

Related Concepts

• Intuitionistic Logic: Logic without LEM
• Classical Logic: Logic with LEM as an axiom
• Decidable: Propositions for which LEM holds constructively
• Proposition: The objects to which LEM applies
• Constructive Mathematics: Mathematics without assuming LEM