Skip to content

Instantly share code, notes, and snippets.

@cppio
Last active October 2, 2024 21:12
Show Gist options
  • Save cppio/c9244f537edff6f84ceeb85a26169c44 to your computer and use it in GitHub Desktop.
Save cppio/c9244f537edff6f84ceeb85a26169c44 to your computer and use it in GitHub Desktop.
Excluded middle from the axiom of choice
theorem choice {α : Sort u} {β : α → Sort v} (h : ∀ x, Nonempty (β x)) : Nonempty (∀ x, β x) := ⟨fun x => Classical.choice (h x)⟩
theorem setext {α : Sort u} {A B : α → Prop} (h : ∀ x, A x ↔ B x) : A = B := funext fun x => propext (h x)
theorem em : P ∨ ¬ P :=
let A x := P ∨ x = false
let B x := P ∨ x = true
let ⟨f⟩ := choice fun C : { C : Bool → _ // ∃ x, C x } => let ⟨x, h⟩ := C.property; ⟨Subtype.mk x h⟩
let a := f ⟨A, false, .inr rfl⟩
have (B) : (h : A = B) → a.val = (f ⟨B, false, h ▸ .inr rfl⟩).val
| rfl => rfl
match a.property, (f ⟨B, true, .inr rfl⟩).property with
| .inl h, _ => .inl h
| _, .inl h => .inl h
| .inr h₁, .inr h₂ => .inr fun h => nomatch h₁ ▸ h₂ ▸ this B (setext fun _ => ⟨fun _ => .inl h, fun _ => .inl h⟩)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment