Formalized Formal Logic

3.2. Axiom of Choice

And the axiom of choice (𝗔𝗖).

🔗def
LO.FirstOrder.SetTheory.Axiom.choice : Sentence ℒₛₑₜ
LO.FirstOrder.SetTheory.Axiom.choice :
  Sentence ℒₛₑₜ

Axiom of choice.

🔗def
LO.FirstOrder.SetTheory.AxiomOfChoice : Theory ℒₛₑₜ
LO.FirstOrder.SetTheory.AxiomOfChoice :
  Theory ℒₛₑₜ

AC: Axiom of choice.

By adding 𝗔𝗖 to the previously defined theories, the theories 𝗭𝗖 and 𝗭𝗙𝗖 are defined.

🔗def
LO.FirstOrder.SetTheory.ZermeloChoice : Theory ℒₛₑₜ
LO.FirstOrder.SetTheory.ZermeloChoice :
  Theory ℒₛₑₜ

Zermelo set theory with axiom of choice.

🔗def
LO.FirstOrder.SetTheory.ZermeloFraenkelChoice : Theory ℒₛₑₜ
LO.FirstOrder.SetTheory.ZermeloFraenkelChoice :
  Theory ℒₛₑₜ

Zermelo-Fraenkel set theory with axiom of choice.