2.1. Formalization of set theory
The role of axioms
A list of axioms for a theory, selected among its basic accepted true statements,
normally aims to specify by their consequences the range of valid (provable)
statements of this theory, against other possible theories, expressible in the same
framework, for which these statements may be false since they are not logically valid.
But set theory being expressed in a special logical framework not used for other theories,
this leaves a priori unclear the distinction between its logically valid statements, and
its other basic accepted truths which need to be declared as axioms.
But such a distinction appears by converting set theory into a generic theory: let
us call axioms of set theory a list of those of its basic 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 set theory.
Converting binders
Binders are the only symbols whose format of
use differs between both frameworks. Let us describe the rules to convert them
from set theory into firstorder logic.
The function definer becomes an infinity of operator symbols: for each term
t with one argument (and 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 1.11.
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))
Open quantifiers, formulas vs statements
Set theory only admits quantifiers ranging over sets (of the form ∃x∈E
and ∀x∈E), called bounded quantifiers, in its formulas
(also called bounded formulas for insistence) that define predicates
and can be used as subformulas of terms by the setbuilder. But its translated
form as a generic theory allows for more formulas, with quantifiers ranging over
other classes (or the universe) we shall call open quantifiers.
In set theory, the use of open quantifiers will be reserved for the expression
of statements, declarared to be true as axioms or theorems.
Precisely, 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.
The inclusion predicate
The inclusion predicate ⊂ between two sets E and F, read as
"E is included in F", or "E is a subset of F", or "F
includes E", is defined by E ⊂ F ⇔
(∀x∈E, x ∈ F).
Properties of inclusion
between classes apply. E ⊂ E is always true
(meaning ∀x, x ∈ E ⇒ x ∈ E).
Implications chains also appear as inclusion chains:
(E ⊂ F ⊂ G) ⇔
(E ⊂ F
∧ F ⊂ G) ⇒ E ⊂ G.
Axioms for notions
The formalization of set theoretical notions as classes inside a single type, already
described in 1.7, involves the
following axioms. Here and in the below axioms for functions, the quantifier
(∀t,E) is meant as declaring a schema of axioms 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 distinction of notions is stated by the following axioms
∀x, ¬(Set(x) ∧ Fnc(x)) 
: sets are not functions 
∀_{Fnc} f, Set(Dom f) 
: the domain of every function is a set 
∀t,E, Fnc(E ∋ x ↦ t(x))

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

Axiom of Extensionality
It says : For all sets E and F,
E ⊂ F ⊂ E ⇒ E = F.
Meaning that any two sets playing the same role are equal (somehow defining
the equality between sets by that of their roles), this axiom expresses that
sets are determined by their role. This role of a set may be understood either
as a range for quantifiers, or as a class defined by ∈.
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
Here is an analogue of the axiom of extensionality for functions :
(=_{Fnc}) ∀_{Fnc} f, ∀_{Fnc} 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 1.⇔(2.∧(=_{Fnc})). We can even integrate in 1. the last axiom
for notions by rewriting it as 1'. ∀t,E, ∀f,
f = (E ∋ x ↦ t(x)) ⇔ (Fnc f ∧ Dom f =
E ∧ ∀x∈E, f(x) = t(x))
The proofs of these equivalences
can be taken as exercises.
Formalizing diverse notions in set theory
Set theory will be expanded by additional components (symbols and axioms,
which may either be primitive or obtainable as developments, namely as
definitions), to directly represent diverse kinds of metaobjects as objects :
"definer" symbols will convert these metaobjects into objects. This can
only apply to metaobjects which are "objectlike" enough, in a sense yet to
be clarified (as seen in 1.8, not all classes can be sets, while only the functors
whose domains are sets are functions).
More "setlike" classes will be converted into sets (2.2), and indirectly
specified elements will become directly specified (2.6).
Metaobjects behaving as other kinds of objects beyond elements, sets and
functions, will form other notions. But as seen for unary relations (1.8), they
need not be added as primitive notions, as their role can naturally be played by
classes of already present objects : sets or functions, that will offer their expressible
features to the new objects. Beyond definers, more symbols (evaluators) will be
needed to interpret these objects back to their roles as metaobjects.
So the notions of operation, relation and tuple will be formalized in 2.3.
If several ways to represent a new notion by a class of old objects
can be useful, which do not represent each new object by the same old
object, then functors will be needed for conversion between the
classes playing this role in the different ways (2.5, 2.10).
Other languages:
FR : 1.10. Formalisation de
la théorie des ensembles