Formalized Formal Logic

3. Set Theory🔗

In this formalization, we use same approach as formalizations for arithmetic theories.

The language of set theory \mathcal{L}_\mathrm{set} is defined as a relationnal theory with two relational symbols \in and =, denoted as ℒₛₑₜ.

🔗def
LO.FirstOrder.Language.set : Language
LO.FirstOrder.Language.set : Language

Language of set theory

  1. 3.1. Axioms and Schemata of Set Theory
  2. 3.2. Axiom of Choice