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 "nonuniverse". 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 firstorder 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 firstorder 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) :
 The technical axioms give to the primitive notions and symbols their correct
roles : the notions of sets and functions,
symbolized in 1.7, are axiomatized
here in 2.1 : axioms for notions ; axiom of Extensionality ; axioms for functions. More
technical axioms will come in 2.4 (unique element) and 5.3 (foundation);
 Axioms from the set generation principle (2.2, 2.6) ;
 Strengthening axioms, introduced in 1.A ;
 The axiom of choice (2.10) might be seen as an optional technical specification
for the powerset.
Converting the binders
When converting set theoretical expressions into firstorder 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
(E ∋ x ↦ t(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 setbuilder, which will
come as a particular case in 2.2.
The conversion of quantifiers comes by expressing
their domains as classes :
(∃x∈E,
A(x)) → (∃x, x ∈ E ∧ A(x))
(∀x∈E, A(x)) → (∀x, x
∈ E ⇒ A(x))
Formulas vs statements
Most set theories (except mainly FST and some strong versions) will only accept
bounded formulas as subformulas of terms (by the setbuilder, 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 
(Fc) ∀(t,E), Fnc(E ∋ x ↦ t(x))

: any definite (E ∋ x ↦ t(x)) is a function

Here and in the below axioms for functions, ∀(t,E) is meant as declaring
an axiom schema by secondorder 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
(E ∋ x ↦ t(x))). Thus for each
term defining t we have an axiom where ∀(t,E) is replaced by
∀parameters, ∀_{Set}E,
(∀x∈E, dt(x, parameters)) ⇒
The inclusion predicate
The binary predicate ⊂ of inclusion
between sets is defined by : for all sets E and F,
E ⊂ F ⇔
(∀x∈E, x ∈ F)
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.
E ⊂ E is logically valid.
Implications chains
also appear as inclusion chains:
(E ⊂ F ⊂ G) ⇔ (E ⊂ F
∧ F ⊂ G) ⇒ E ⊂ G.
Axiom of Extensionality
This axiom lets sets be determined by their role (either as ranges for quantifiers, or
as the classes they define by ∈), saying that any two sets playing the same
role are equal :
∀_{set} E,F, E ⊂ F ⊂ E ⇒ E = F.
Indeed, E ⊂ F ⊂ E means that E and F have the
same elements (∀x, x ∈ E ⇔ x ∈ F),
and for any predicate R, (∀x∈F,
R(x)) ⇔ (∀x∈E, 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:
 ∀(t,E), ∀_{Fnc} f, f = (E ∋
x ↦ t(x)) ⇔ (Dom f = E ∧ ∀x∈E,
f(x) = t(x))
 ∀(t,E), Dom(E ∋ x ↦ t(x)) = E
∧ ∀x∈E, (E ∋ y ↦ t(y))(x)
= t(x)
Indeed (Fc) ⇒ (1.⇔(2.∧(=_{Fnc}))).
The proof can be taken as an exercise (click to show)
Assume (Fc) for 2. to be definite.
Abbreviate (Dom f = E ∧ ∀x∈E, f(x) = t(x)) as
[f : E, t], to shorten the above as
 ∀(t,E), ∀_{Fnc} f, f = (E ∋
x ↦ t(x)) ⇔ [f : E, t]
 ∀(t,E), [E ∋ x ↦ t(x) : E, t]
1. ⇔ (2. ∧ 1b.) where
1b. ∀(t,E), ∀_{Fnc }f, [f : E, t] ⇒
f = (E ∋ x ↦ t(x))
Proof of 1b. ⇒ (=_{Fnc})
∀_{Fnc} g,
applying 1b. to (g, E) where E = Dom g as
∀x∈Dom g, dg(x) :
∀_{Fnc} f, [f : E, g] ⇒
f = (E ∋ x ↦ g(x))
[g : E, g] ∴ g = (E ∋ x ↦ g(x))
∀_{Fnc} f, [f : E, g] ⇒ f = g
Proof of (2.∧(=_{Fnc})) ⇒ 1b.
∀(t,E), ∀_{Fnc} f, ([f : E, t]
∧ [E ∋ x ↦ t(x) : E, t]) ⇒
f = (E ∋ x ↦ t(x)).
∎
Note: (Fc) ∧ 1. can also be written
1'. ∀(t,E), ∀f,
f = (E ∋ x ↦ t(x)) ⇔ (Fnc f ∧ Dom f =
E ∧ ∀x∈E, f(x) = t(x)).
Other languages:
FR : 2.1.
Premiers axiomes de
théorie des ensembles