Formalized Formal Logic

3.1. Axioms and Schemata of Set Theory

We define basic 7 axioms and 2 axiom schemata.

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

Axiom of empty set.

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

Axiom of extentionality.

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

Axiom of pairing.

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

Axiom of union.

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

Axiom of power set.

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

Axiom of infinity.

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

Axiom of foundation.

🔗def
LO.FirstOrder.SetTheory.Axiom.separationSchema
  (φ : SyntacticSemiformula ℒₛₑₜ 1) : Sentence ℒₛₑₜ
LO.FirstOrder.SetTheory.Axiom.separationSchema
  (φ : SyntacticSemiformula ℒₛₑₜ 1) :
  Sentence ℒₛₑₜ

Axiom schema of separation (Aussonderungsaxiom).

🔗def
LO.FirstOrder.SetTheory.Axiom.replacementSchema
  (φ : SyntacticSemiformula ℒₛₑₜ 2) : Sentence ℒₛₑₜ
LO.FirstOrder.SetTheory.Axiom.replacementSchema
  (φ : SyntacticSemiformula ℒₛₑₜ 2) :
  Sentence ℒₛₑₜ

Axiom schema of replacement.

The theory obtained by excluding replacement schema from the above axioms and axiom schemata is called Zermelo set theory 𝗭.

🔗inductive predicate
LO.FirstOrder.SetTheory.Zermelo : Theory ℒₛₑₜ
LO.FirstOrder.SetTheory.Zermelo :
  Theory ℒₛₑₜ

Zermelo set theory.

Constructors

axiom_of_equality (φ : Sentence ℒₛₑₜ) : φ ∈ 𝗘𝗤 → 𝗭 φ

Axiom of equality.

axiom_of_empty_set : 𝗭 Axiom.empty

Axiom of empty set.

axiom_of_extentionality : 𝗭 Axiom.extentionality

Axiom of extentionality.

axiom_of_pairing : 𝗭 Axiom.pairing

Axiom of pairing.

axiom_of_union : 𝗭 Axiom.union

Axiom of empty union.

axiom_of_power_set : 𝗭 Axiom.power

Axiom of power set.

axiom_of_infinity : 𝗭 Axiom.infinity

Axiom of infinity.

axiom_of_foundation : 𝗭 Axiom.foundation

Axiom of foundation.

axiom_of_separation (φ : SyntacticSemiformula ℒₛₑₜ 1) :
  𝗭 (Axiom.separationSchema φ)

Axiom schema of separation.

The theory of all the above axioms and axiom schemata is called Zermelo-Fraelkel set theory 𝗭𝗙.

🔗inductive predicate
LO.FirstOrder.SetTheory.ZermeloFraenkel : Theory ℒₛₑₜ
LO.FirstOrder.SetTheory.ZermeloFraenkel :
  Theory ℒₛₑₜ

Zermelo-Fraenkel set theory.

Constructors

axiom_of_equality (φ : Sentence ℒₛₑₜ) : φ ∈ 𝗘𝗤 → 𝗭𝗙 φ

Axiom of equality.

axiom_of_empty_set : 𝗭𝗙 Axiom.empty

Axiom of empty set.

axiom_of_extentionality : 𝗭𝗙 Axiom.extentionality

Axiom of extentionality.

axiom_of_pairing : 𝗭𝗙 Axiom.pairing

Axiom of pairing.

axiom_of_union : 𝗭𝗙 Axiom.union

Axiom of union.

axiom_of_power_set : 𝗭𝗙 Axiom.power

Axiom of power set.

axiom_of_infinity : 𝗭𝗙 Axiom.infinity

Axiom of infinity.

axiom_of_foundation : 𝗭𝗙 Axiom.foundation

Axiom of foundation.

axiom_of_separation (φ : SyntacticSemiformula ℒₛₑₜ 1) :
  𝗭𝗙 (Axiom.separationSchema φ)

Axiom schema of separation.

axiom_of_replacement (φ : SyntacticSemiformula ℒₛₑₜ 2) :
  𝗭𝗙 (Axiom.replacementSchema φ)

Axiom schema of replacement.