2.13 Classical vs Constructive Logic

Lean is constructive by default. This affects which proofs are available and what information a proof must contain. Classical reasoning can be enabled explicitly when needed.

Problem

You want to understand why some statements are easy to prove in mathematics but require additional assumptions in Lean, and how to control that boundary.

Constructive Logic

In constructive logic, a proof must provide explicit evidence.

• To prove ∃ x, P x, you must give a concrete x
• To prove P ∨ Q, you must choose which side holds
• To prove ¬ P, you must show that P leads to contradiction

This aligns with computation. A proof corresponds to a program that constructs the required object.

Example:

theorem constructive_example (P : Prop) : P -> ¬ ¬ P := by
  intro hp
  intro hnp
  exact hnp hp

This is constructive because it explicitly uses hp.

Classical Logic

Classical logic allows nonconstructive reasoning. The most important principle is the law of excluded middle:

P ∨ ¬ P

This says that every proposition is either true or false, even if no proof is known.

In Lean, classical reasoning is enabled by:

open Classical

Using Excluded Middle

open Classical

theorem excluded_middle_example (P : Prop) : P ∨ ¬ P := by
  exact em P

The constant em is the excluded middle principle.

Double Negation Elimination

Constructively, you cannot prove:

¬ ¬ P -> P

In classical logic, you can.

open Classical

theorem double_negation_elim (P : Prop) : ¬ ¬ P -> P := by
  intro hnnp
  by_cases hp : P
  · exact hp
  · exfalso
    exact hnnp hp

The step:

by_cases hp : P

splits the proof into:

hp : P

and:

hp : ¬ P

This case split relies on classical logic.

Proof by Contradiction

Constructively, to prove ¬ P, assume P and derive False.

Classically, to prove P, you may assume ¬ P and derive False.

open Classical

theorem by_contradiction_example (P : Prop) : (¬ P -> False) -> P := by
  intro h
  by_contra hp
  exact h hp

The tactic by_contra assumes ¬ P and changes the goal to False.

Classical Reasoning with Existentials

Constructive proofs of existence must provide a witness. Classical proofs may avoid constructing one.

open Classical

theorem classical_exists
    (α : Type)
    (P : α -> Prop)
    (h : ¬ ∀ x, ¬ P x) :
    ∃ x, P x := by
  by_contra hne
  apply h
  intro x
  intro hx
  apply hne
  use x

This proof extracts an existential from a double negation using classical reasoning.

Choice Principle

Classical logic also provides a choice operator.

open Classical

noncomputable def choose_example
    {α : Type}
    {P : α -> Prop}
    (h : ∃ x, P x) : α :=
  Classical.choose h

This function selects a witness from an existential statement.

The corresponding proof:

theorem choose_property
    {α : Type}
    {P : α -> Prop}
    (h : ∃ x, P x) :
    P (Classical.choose h) :=
  Classical.choose_spec h

This is noncomputable. The witness is guaranteed to exist, but no algorithm constructs it.

Constructive vs Classical Summary

Mixing Styles

Lean allows mixing constructive and classical reasoning.

You can keep most proofs constructive and only use classical logic where necessary.

theorem mixed_example
    (P Q : Prop)
    (h : P -> Q) :
    ¬ Q -> ¬ P := by
  intro hnq
  intro hp
  exact hnq (h hp)

This proof is constructive.

If you later need classical reasoning:

open Classical

theorem classical_extension
    (P : Prop) :
    ¬ ¬ P -> P := by
  intro h
  exact Classical.byContradiction (fun hp => h hp)

Decidable Propositions

Lean distinguishes between general propositions and decidable ones.

If P is decidable, Lean can compute whether it holds.

example (n : Nat) : n = 0 ∨ n ≠ 0 := by
  exact Nat.eq_zero_or_ne_zero n

This is constructive because equality on natural numbers is decidable.

Practical Guidance

Use constructive proofs when:

• You want computational content
• You need explicit witnesses
• You are building algorithms

Use classical proofs when:

• The statement is inherently nonconstructive
• The proof would be unnecessarily complex constructively
• You only care about existence, not construction

Keep classical reasoning local:

open Classical

near the proof that needs it, instead of globally.

Common Patterns

Enable classical logic:

open Classical

Use excluded middle:

em P

Use case split:

by_cases hp : P

Use contradiction:

by_contra hp

Extract witness:

Classical.choose h

Common Pitfalls

Do not assume classical principles are available without open Classical.

Do not use classical logic when constructive proofs are required for computation.

Do not rely on Classical.choose in computable definitions.

Do not mix constructive and classical reasoning without understanding where noncomputability is introduced.

Takeaway

Constructive logic requires explicit constructions. Classical logic allows reasoning without constructing witnesses. Lean supports both, but defaults to constructive reasoning. Understanding when and how to use classical principles is essential for controlling proof structure and computational content.