2.1. First axioms of set theory

Let us start presenting the axioms of our set theory, whose basic notions and language were introduced in part 1: more precisely a theory of sets and functions (or: of elements, sets and functions).

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.

We may use the same notation EF as abbreviation for the inclusion of a set E in a class F (and similarly for other formulas defined from this):

EF ⇔ ∀xE, F(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 as possible definitions of predicates (what predicate symbols abbreviate). Open quantifiers will be only allowed in statements (declarared true as axioms or theorems).
In set theory, a statement is a ground formula which can combine the symbols of first-order logic with the regular ones of set theory as follows: it must be made of a chain of open quantifiers, usually all ∀ and often written in words ("for all"), followed by a bounded formula. Proofs will naturally use the deduction rules for open quantifiers (introduction and elimination) by common language articulations.
The above definition of ⊂, basically claiming the predicate symbol ⊂ to abbreviate the bounded formula (∀xE, xF), can also be seen as an example of statement with open quantifiers (∀SetE,F, ) taken as an axiom.

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.

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))

Classification of 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).

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(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)) ⇒

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, 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 (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 ∧ ∀xE, f(x) = t(x)) as [f : E, t], to shorten the above as
  1. ∀(t,E), ∀Fnc f, f = (Ext(x)) ⇔ [f : E, t]
  2. ∀(t,E), [Ext(x) : E, t]
1. ⇔ (2. ∧ 1b.) where

1b. ∀(t,E), ∀Fnc f, [f : E, t] ⇒ f = (Ext(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 = (Exg(x))
[g : E, g] ∴ g = (Exg(x))
Fnc f, [f : E, g] ⇒ f = g
Proof of (2.∧(=Fnc)) ⇒ 1b.
∀(t,E), ∀Fnc f, ([f : E, t] ∧ [Ext(x) : E, t]) ⇒ f = (Ext(x)). ∎
Note: (Fc) ∧ 1. can also be written

1'. ∀(t,E), ∀f, f = (Ext(x)) ⇔ (Fnc f ∧ Dom f = E ∧ ∀xE, f(x) = t(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. Graphs
2.7. Products and powerset
2.8. Injections, bijections
2.9. Properties of binary relations
2.10. 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