Basic axioms of set theory

This is BST (basic set theory), which is Zermelo set theory minus replacement. TODO: Find a citation for the name of this set theory.

Basic set theory

inductive FFL.FirstOrder.SetTheory.BasicSetTheory : SetTheory

Basic set theory (Zermelo minus separation).

• equality (φ : Sentence ℒₛₑₜ) : φ ∈ 𝗘𝗤 ℒₛₑₜ → 𝗕𝗦𝗧 φ

  Axiom of equality.

• empty_set : 𝗕𝗦𝗧 (∃¹ isEmpty/[Semiterm.bvar 0])

  Axiom of empty set.

• extensionality : 𝗕𝗦𝗧 (“∀¹ ∀¹ (!!(Semiterm.bvar 1) = !!(Semiterm.bvar 0) ↔ ∀¹ (!!(Semiterm.bvar 0) ∈ !!(Semiterm.bvar 2) ↔ !!(Semiterm.bvar 0) ∈ !!(Semiterm.bvar 1)))”)

  Axiom of extensionality.

• pairing : 𝗕𝗦𝗧 (“∀¹ ∀¹ ∃¹ ∀¹ (!!(Semiterm.bvar 0) ∈ !!(Semiterm.bvar 1) ↔ !((“!!(Semiterm.bvar 0) = !!(Semiterm.bvar 3)”) ⋎ (“!!(Semiterm.bvar 0) = !!(Semiterm.bvar 2)”)))”)

  Axiom of pairing.

• union : 𝗕𝗦𝗧 (“∀¹ ∃¹ ∀¹ (!!(Semiterm.bvar 0) ∈ !!(Semiterm.bvar 1) ↔ !(Semiformula.bexsMem (Semiterm.bvar 2) (“!!(Semiterm.bvar 1) ∈ !!(Semiterm.bvar 0)”)))”)

  Axiom of empty union.

• power_set : 𝗕𝗦𝗧 (“∀¹ ∃¹ ∀¹ (!!(Semiterm.bvar 0) ∈ !!(Semiterm.bvar 1) ↔ !(isSubsetOf/[Semiterm.bvar 0, Semiterm.bvar 2]))”)

  Axiom of power set.

• infinity : 𝗕𝗦𝗧 (∃¹ (∀¹ (isEmpty/[Semiterm.bvar 0] 🡒 (“!!(Semiterm.bvar 0) ∈ !!(Semiterm.bvar 1)”))) ⋏ Semiformula.ballMem (Semiterm.bvar 0) (∀¹ (isSucc/[Semiterm.bvar 0, Semiterm.bvar 1] 🡒 (“!!(Semiterm.bvar 0) ∈ !!(Semiterm.bvar 2)”))))

  Axiom of infinity.

• foundation : 𝗕𝗦𝗧 (∀¹ (isNonempty/[Semiterm.bvar 0] 🡒 Semiformula.bexsMem (Semiterm.bvar 0) (Semiformula.ballMem (Semiterm.bvar 1) (∼(“!!(Semiterm.bvar 0) ∈ !!(Semiterm.bvar 1)”)))))

  Axiom of foundation.

def FFL.FirstOrder.SetTheory.«term𝗕𝗦𝗧» : Lean.ParserDescr

Equations

• FFL.FirstOrder.SetTheory.«term𝗕𝗦𝗧» = Lean.ParserDescr.node `FFL.FirstOrder.SetTheory.«term𝗕𝗦𝗧» 1024 (Lean.ParserDescr.symbol "𝗕𝗦𝗧")

instance FFL.FirstOrder.SetTheory.instWeakerThanSentenceSetTheoryEqAxiomBasicSetTheory : 𝗘𝗤 ℒₛₑₜ ⪯ 𝗕𝗦𝗧