2.1. First axioms of set theory

The role of axioms

As explained in 1.9, the role of the axioms of a generic theory, is to express its intended range of models as a selection (class) from a wider notion of "all systems" with structures named by the same language. The logical framework, which holds (describes) this wider notion, can interpret the axioms in each such system, then exclude those where it finds some axiom to be false. Excluded systems remain possible models of different theories described by the same framework. Any statement true in all systems (a logically valid statement) is useless (redundant) as an axiom.

But expressing set theory in its special logical framework not used for other theories, leaves a priori undefined the distinction between its logically valid statements, and its other basic accepted truths which need to be declared as axioms due to their falsity in some "non-universe". Now this distinction can be given sense by converting set theory into a generic theory: let us call axioms of a set theory a list of its basic "true" statements whose translated versions in first-order logic are not logically valid, but form a proper list of axioms for that generic theory to be equivalent to the intended version of set theory. From there, provability in a set theory can be defined as the one given by first-order logic with these axioms.

Axioms of set theories (sometimes with other primitive components) can be classified as follows according to their roles, ordered from the more "primitive" (necessary) components, to the more optional and debatable ones (opening a diversity of acceptable set theories) :

Converting the binders

When converting set theoretical expressions into first-order logic, the only modified symbols are the binders, as their format of use differs between both frameworks. Let us describe the rules of this conversion.
The function definer (1.8) becomes an infinity of operator symbols: for each term t with one argument and any list of parameters, the whole term (Ext(x)) is seen as the big name of a distinct operator symbol, whose arguments are E and the parameters of t. (Those where every subexpression of t without any occurrence of x is the only occurrence of a parameter, would suffice to define others).
The same goes for the set-builder, which will come as a particular case in 2.2.
The conversion of quantifiers comes by expressing their domains as classes :

(∃xE, A(x)) → (∃x, xEA(x))
(∀xE, A(x)) → (∀x, xEA(x))

Formulas vs statements

Most set theories (except mainly FST and some strong versions) will only accept bounded formulas as sub-formulas of terms (by the set-builder, and later by the conditional operator) and to define predicates. Open quantifiers will be only allowed in statements (declarared true as axioms or theorems): each statement will be made of a chain of open quantifiers, usually all ∀ and often written in words ("for all"), before a bounded formula. Proofs will naturally use the deduction rules for open quantifiers (introduction and elimination) by common language articulations.

Axioms for notions

The formalization of primitive notions by class symbols following 1.7, needs to be completed by the following axioms.

x, ¬(Set(x) ∧ Fnc(x)) : sets are not functions (though it does not matter)
Fnc f, Set(Dom f) : the domain of every function is a set
∀(t,E), Fnc(Ext(x)) : any definite (Ext(x)) is a function

Here and in the below axioms for functions, ∀(t,E) is meant as declaring an axiom schema by second-order universal elimination over the variable functor t with E included in the definiteness class of the term defining t for the given values of parameters (this is the definiteness condition for (Ext(x))). Thus for each term defining t we have an axiom where ∀(t,E) is replaced by

∀parameters, ∀SetE, (∀xE, dt(x, parameters)) ⇒

The inclusion predicate

The binary predicate ⊂ of inclusion between sets is defined by : for all sets E and F,

EF ⇔ (∀xE, xF)

and read as "E is included in F", or "E is a subset of F", or "F includes E". Properties of inclusion between classes apply.
EE is logically valid. Implications chains also appear as inclusion chains:
(EFG) ⇔ (EFFG) ⇒ EG.

Axiom of Extensionality

To conceive sets as determined by their role (either as ranges for quantifiers, or as the classes they define by ∈), this axiom says any two sets playing the same role are equal : for all sets E and F,

EFEE = F.

Indeed, EFE means that E and F have the same elements (∀x, xExF), and for any predicate R,

(∀xF, R(x)) ⇔ (∀xE, R(x))

and similarly for ∃. Informally, the elements of a set are given in bulk.

Axioms for functions

Functions are also made determined by their role, by the following axiom (=Fnc):

Fnc f,g, (Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ f = g.

The function definers are related with the function evaluator by an axiom which can be written in either way:
  1. ∀(t,E), ∀Fnc f, f = (Ext(x)) ⇔ (Dom f = E ∧ ∀xE, f(x) = t(x))
  2. ∀(t,E), Dom(Ext(x)) = E ∧ ∀xE, (Eyt(y))(x) = t(x)
Indeed 1.⇔(2.∧(=Fnc)). We can even integrate in 1. the last axiom for notions by re-writing it as

1'. ∀(t,E), ∀f, f = (Ext(x)) ⇔ (Fnc f ∧ Dom f = E ∧ ∀xE, f(x) = t(x)).

The proofs of these equivalences can be taken as exercises (click to show)

Recalling the axioms:

Fc. ∀t,E, Fnc (Ext(x))
1. ∀t,E, ∀Fnc f, f = (Ext(x)) ⇔ (Dom f = E ∧ (∀xE, f(x) = t(x)))
1'. ∀t,E, ∀f, f = (Ext(x)) ⇔ (Fnc f ∧ Dom f = E ∧ ∀xE, f(x) = t(x))
2. ∀t,E, Dom(Ext(x)) = E ∧ ∀yE, (Ext(x))(y) = t(y)
(=Fnc) ∀Fnc f,g, (Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ f = g

Splitting the ⇔ in 1. as a conjuction of implications, (1. ⇔ (1a. ∧ 1b.)) where

1a. ∀t,E, ∀Fnc f, f = (Ext(x)) ⇒ (Dom f = E ∧ (∀xE, f(x) = t(x)))
1b. ∀t,E, ∀Fnc f, (Dom f = E ∧ (∀xE, f(x) = t(x))) ⇒ f = (Ext(x))

Similarly (1'. ⇔ (1a'. ∧ 1b.)) where
1a'. ∀t,E, ∀ f, f = (Ext(x)) ⇒ (Fnc f ∧ Dom f = E ∧ (∀xE, f(x) = t(x)))

We can see immediately that 1a'. ⇔ (Fc. ∧ 2.) ⇒ 1a.
(We may write 2. ⇒ 1a. if not careful about definiteness).
Conversely, we can see (1a. ∧ Fc.) ⇒ 2.

Proof of 1b. ⇒ (=Fnc)
Fnc f,g, (Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ ∃SetE, Dom f = E = Dom g ∧ (∀xE, f(x) = f(x) = g(x)) ∴ f = (Exf(x)) = g.
Proof of (2.∧(=Fnc)) ⇒ 1b. : ∀t,E, ∀Fnc f,
(Dom f = E ∧ (∀xE, f(x) = t(x)))
⇒ (Dom f = Dom(Ext(x)) ∧ (∀yE, f(y) = (Ext(x))(y)))
f = (Ext(x))
Set theory and Foundations of Mathematics
1. First foundations of mathematics
2. Set theory
2.1. First axioms of set theory
2.2. Set generation principle
2.3. Tuples
2.4. Uniqueness quantifiers
2.5. Families, Boolean operators on sets
2.6. Products, graphs and composition
2.7. The powerset
2.8. Injectivity and inversion
2.9. Binary relations ; order
2.10. Canonical bijections
2.11. Equivalence relations, partitions
2.12. Axiom of choice
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : 2.1. Premiers axiomes de théorie des ensembles