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 first-order 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 first-order logic.
The function definer becomes an infinity of operator symbols: for each term t with one argument (and 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 1.11.
The conversion of quantifiers comes by expressing their domains as classes :

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

Open quantifiers, formulas vs statements

Set theory only admits quantifiers ranging over sets (of the form ∃xE and ∀xE), called bounded quantifiers, in its formulas (also called bounded formulas for insistence) that define predicates and can be used as sub-formulas of terms by the set-builder. 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

EF ⇔ (∀xE, xF).

Properties of inclusion between classes apply. EE is always true (meaning ∀x, xExE).
Implications chains also appear as inclusion chains:
(EFG) ⇔ (EFFG) ⇒ EG.

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 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 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(Ext(x)) : any definite (Ext(x)) is a function

Axiom of Extensionality

It says : For all sets E and F, EFEE = 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, 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

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:

  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.

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 meta-objects as objects : "definer" symbols will convert these meta-objects into objects. This can only apply to meta-objects which are "object-like" 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 "set-like" classes will be converted into sets (2.2), and indirectly specified elements will become directly specified (2.6).

Meta-objects 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 meta-objects. 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).

Set theory and Foundations of Mathematics
1. First foundations of mathematics
2. Set theory
2.1. Formalization of set theory
2.2. Set generation principle
2.3. Tuples, families
2.4. Boolean operators on families of sets
2.5. Products, graphs and composition
2.6. Uniqueness quantifiers, functional graphs
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
2.13. Galois connection
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : 1.10. Formalisation de la théorie des ensembles