## Prompt Lean4: Explain the difference between (1):Decidable P and (2):Classical.em P.  Also, provide 5 examples that illstrate the uses and the differences of (1) and (2). --- In Lean 4, `Decidable P` and `Classical.em P` represent two distinct fundamental approaches to logic and computation: `constructive computability` versus classical `non-constructive truth`. ## Core Differences - `Decidable P` **(Constructive & Computational)**: `Decidable P` is a **type class** (a computational data structure). An instance of `Decidable P` provides an algorithm (a decision procedure) that can evaluate whether `P` is true or false at runtime. If a proposition is decidable, Lean's reduction engine or compiled code can physically compute the answer (`isTrue` or `isFalse`). - `Classical.em P` **(Non-Constructive Axiom)**: `Classical.em P` is a **proof term** of the Law of Excluded Middle (`P ∨ ¬P`) asserting that `P` is logically either true or false. It operates purely at the logical/type level and contains no computational algorithm. It allows non-constructive mathematical reasoning (such as proofs by contradiction) without guaranteeing that `P` can be computed or evaluated. ## Key Distinctions |Feature|`Decidable P`|`Classical.em P`| |---|---|---| |**Nature**|Type class containing an algorithm (`Decidable P`)|Logical axiom returning a proof (`P ∨ ¬P`)| |**Computability**|Computable; can be evaluated using `#eval` or `if/then/else`|Non-computable; requires `noncomputable` keyword when used for definitions| |**Logic**|Constructive (Intuitionistic)|Classical| |**Scope**|Works only for propositions with decision algorithms (e.g., 2 + 2 = 4)|Applies to _any_ proposition P, regardless of computability| ## 5 Illustrative Examples #### 1. Conditional Branching in Computable Code vs. Non-computable Code `Decidable` allows code execution in `if/then/else` constructs. Using `Classical.em` in a function forces the function to be non-computable. ```lean -- Computable: Uses Decidable (Lean automatically finds the Decidable (n = 0) instance) def checkZero (n : Nat) : String := if n = 0 then "Zero" else "Not Zero" #eval checkZero 0 -- Outputs: "Zero" -- Non-computable: Uses Classical.em / classical decidability on an arbitrary proposition noncomputable def checkProp (P : Prop) : String := if h : P then "True" else "False" ``` #### 2. Decidability of Finite Arithmetic Simple arithmetic assertions implement `Decidable`, letting Lean prove or compute them automatically by running the decision algorithm. ```lean -- Decidable: Lean evaluates 5 < 10 directly example : Decidable (5 < 10) := inferInstance -- Classical: Asserting the law of excluded middle on arithmetic without executing it example : (5 < 10) ∨ ¬(5 < 10) := Classical.em (5 < 10) ``` #### 3. Proving Disjunctions Constructively vs. Classically To prove `P ∨ ¬P` constructively with `Decidable`, Lean pattern-matches on the decision procedure. With `Classical.em`, it is directly asserted as an axiom. ```lean -- Constructive proof given a Decidable instance theorem em_of_decidable (P : Prop) [h : Decidable P] : P ∨ ¬P := by match h with | isTrue hP => exact Or.inl hP | isFalse hnP => exact Or.inr hnP -- Classical proof without needing a Decidable instance theorem em_classical (P : Prop) : P ∨ ¬P := Classical.em P ``` #### 4. Handling Undecidable/Uncomputable Statements (e.g., Halting Problem / Arbitrary Predicates) For general predicates over infinite domains (like checking if a function terminates or if an arbitrary function f : \mathbb{N} \to \mathbb{N} has a zero), no `Decidable` instance exists, making `Classical.em` necessary. ```lean -- An arbitrary predicate on functions def HasZero (f : Nat → Nat) : Prop := ∃ n, f n = 0 -- We CANNOT synthesize `Decidable (HasZero f)` constructively. -- We MUST use Classical.em to reason about it: example (f : Nat → Nat) : HasZero f ∨ ¬HasZero f := Classical.em (HasZero f) ``` #### 5. Case Analysis Tactics (`decide` vs. `by_cases`) The `decide` tactic uses `Decidable` instances to perform computation to close a goal, whereas `by_cases` (or `Classical.byContradiction`) invokes classical reasoning to split a goal. ```lean -- Using computation via Decidable example : 100 + 200 = 300 := by decide -- Using classical case splitting via Classical.em example (P : Prop) : P → (P ∧ P) := by by_cases hCasesOfP : P · intro _P : P exact ⟨h, h⟩ · intro hP exact False.elim (h hP) ``` ## Prompt lean4: explain what Classical.em P is and expliprovide 5 examples of its uses. Also --- **`LeanNotes curator:`** [[Gemini 3.5]], [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date`**: 2026-09-05