Zermelo–Fraenkel set theory

reference: Ralf Schindler, "Set Theory, Exploring Independence and Truth"

inductive LO.ZermeloFraenkel : FirstOrder.Theory ℒₛₑₜ

• equal (φ : FirstOrder.Sentence ℒₛₑₜ) : φ ∈ 𝗘𝗤 → 𝗭𝗙 φ
• empty : 𝗭𝗙 FirstOrder.SetTheory.Axiom.empty
• extentionality : 𝗭𝗙 FirstOrder.SetTheory.Axiom.extentionality
• pairing : 𝗭𝗙 FirstOrder.SetTheory.Axiom.pairing
• union : 𝗭𝗙 FirstOrder.SetTheory.Axiom.union
• power : 𝗭𝗙 FirstOrder.SetTheory.Axiom.power
• infinity : 𝗭𝗙 FirstOrder.SetTheory.Axiom.infinity
• foundation : 𝗭𝗙 FirstOrder.SetTheory.Axiom.foundation
• separation (φ : FirstOrder.SyntacticSemiformula ℒₛₑₜ 1) : 𝗭𝗙 (FirstOrder.SetTheory.Axiom.separationSchema φ)
• replacement (φ : FirstOrder.SyntacticSemiformula ℒₛₑₜ 2) : 𝗭𝗙 (FirstOrder.SetTheory.Axiom.replacementSchema φ)

def LO.«term𝗭𝗙» : Lean.ParserDescr

Equations

• LO.«term𝗭𝗙» = Lean.ParserDescr.node `LO.«term𝗭𝗙» 1024 (Lean.ParserDescr.symbol "𝗭𝗙")

instance LO.ZermeloFraenkel.instWeakerThanSentenceSetTheoryEqAxiom : 𝗘𝗤 ⪯ 𝗭𝗙