Learning Classical Logic in Lean 4: The Law of Excluded Middle, Proof by Contradiction, and Axiomatic Systems

In this post, we will take a look at the logical foundations of Lean 4. While Lean fundamentally adopts intuitionistic logic, the "law of excluded middle"—which is used in classical logic—is also available in the standard library. We will explore the meaning of the law of excluded middle, its relationship with proof by contradiction, and the underlying axiomatic system that Lean relies on. We will continue using "Introduction to Lean Language from Scratch: Hands-on Formal Mathematics Library Development" as our learning material.

Differences Between Intuitionistic Logic and Classical Logic

Intuitionistic logic is a logical system based on the idea that the truth of a proposition is demonstrated by "actually constructing evidence (a witness)." If you want to assert that "a certain value exists," you must explicitly produce and show that value.

On the other hand, classical logic allows indirect reasoning, such as "assuming it does not exist leads to a contradiction." The law that creates this difference is the law of excluded middle, which is unconditionally accepted only in classical logic.

What is the Law of Excluded Middle?

The Law of Excluded Middle (LEM) states that for any given proposition P, the following holds:

P ∨ ¬P

"Every proposition is either true or false"—while this might seem obvious at first glance, from the perspective of intuitionistic logic, this claims "either one or the other" without providing any evidence. In intuitionistic logic, the law of excluded middle is treated not as a self-evident axiom, but as a proposition that requires proof.

How Proof by Contradiction Works

The law of excluded middle enables the use of a proof technique called proof by contradiction (reductio ad absurdum). It works as follows:

• To prove that "A is true," you intentionally assume the opposite, "¬A" (A is not true).
• If this assumption leads to a contradiction, the possibility of "¬A" is eliminated.
• Since the law of excluded middle guarantees "either A or ¬A," ruling out ¬A establishes that "A is true."

The Law of Excluded Middle in Lean: Classical.em

In Lean, the law of excluded middle is defined under the name Classical.em.

theorem Classical.em (p : Prop) : p ∨ ¬p

This is included in Lean's standard library and can be used whenever necessary. However, using tools from classical logic increases the number of axioms your proof depends on. You can verify this using the following command.

Checking Axioms with #print axioms

By using the #print axioms command, you can view a list of which axioms a specific theorem or definition depends on.

#print axioms Classical.em
-- 'Classical.em' depends on axioms: [propext, Classical.choice, Quot.sound]

We can see that Classical.em depends on three axioms. Let's look at the meaning of each one by one.

Understanding the Three Axioms

propext — Axiom of Propositional Extensionality

propext {a b : Prop} : (a ↔ b) → a = b

This axiom states that "equivalent propositions are equal." It asserts that if a ↔ b (a and b are equivalent), then they can be considered equal (a = b). Since Lean treats propositions as types, being "equal as types" means they are completely identical.

Classical.choice — Axiom of Choice

Classical.choice.{u} {α : Sort u} : Nonempty α → α

This axiom states that "given a non-empty type α, we can retrieve an element from it." The crucial point here is that this is permitted not only for finite types but also for infinite types.

Since a procedure to "explicitly retrieve" an element from an infinite type cannot be implemented, any definition using Classical.choice cannot be executed as a program. Such definitions require the noncomputable modifier (explained below).

Quot.sound — Axiom of Soundness for Quotients

Quot.sound.{u} {α : Sort u} {r : α → α → Prop} {a b : α} : r a b → Quot.mk r a = Quot.mk r b

This axiom states that "elements a and b related by an equivalence relation r are equal in the quotient type." This axiom is necessary for incorporating the mathematical concept of quotient sets into Lean, and it supports the construction of Lean's quotient types (Quot).

The noncomputable Modifier

Definitions that use choice principles like Classical.choice have no guarantee of being "actually computable." Therefore, if you try to define a function or similar entity using Classical.choice, Lean will require the noncomputable modifier.

noncomputable def myFunc : ... := ...

This is an explicit declaration stating, "I am writing this knowing that this definition is non-computable." While it works perfectly fine within the realm of proofs, it cannot be used as an executable program. This is an interesting aspect of Lean, as conventional programming languages do not have modifiers to denote non-computability.