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

```lean
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:

```lean
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:

```lean
open Classical
```

## Using Excluded Middle

```lean
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:

```lean
¬ ¬ P -> P
```

In classical logic, you can.

```lean
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:

```lean
by_cases hp : P
```

splits the proof into:

```lean
hp : P
```

and:

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

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

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

```lean
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:

```lean
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

| Feature      | Constructive      | Classical              |
| ------------ | ----------------- | ---------------------- |
| `P ∨ ¬ P`    | Not provable      | Always available       |
| `¬ ¬ P -> P` | Not provable      | Provable               |
| Existence    | Must give witness | May be nonconstructive |
| Computation  | Preserved         | May be lost            |

## Mixing Styles

Lean allows mixing constructive and classical reasoning.

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

```lean
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:

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

```lean
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:

```lean
open Classical
```

near the proof that needs it, instead of globally.

## Common Patterns

Enable classical logic:

```lean
open Classical
```

Use excluded middle:

```lean
em P
```

Use case split:

```lean
by_cases hp : P
```

Use contradiction:

```lean
by_contra hp
```

Extract witness:

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