Audit classical reasoning

4/4 ~20 minlean

Prove excluded middle and include the command that reports its axioms.

4 lines · Lean 4

theorem em_local (P : Prop) : P ∨ ¬P := by
  sorry

-- add an axiom audit command here

Objectifs

Indices

Voir la solution

theorem em_local (P : Prop) : P ∨ ¬P := by
  classical
  exact Classical.em P

#print axioms em_local