1.10. Formalization of set theory

The inclusion predicate

The inclusion predicate ⊂ between two sets E and F, is defined by
EF ⇔ (∀xE, xF).
It is read: E is included in F, or E is a subset of F, or F includes E.
We always have EE (as it means: ∀x, xExE).
Implications chains also appear as inclusion chains:
(EFG) ⇔ (EFFG) ⇒ EG.

Translating the definer into first-order logic

The translation of set theory into a generic theory converts the function definer into an infinity of operator symbols: for each term t with one argument (and parameters), the whole expression (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.
This way, the axioms list of set theory can be regarded as the axioms list of the generic theory into which set theory is converted. All axioms which depend on an expression (a term for the definer, or a formula for the set builder) are schemas of axioms. (A schema of claims, i.e. axioms or theorems, is an infinite list of claims, usually obtained by replacing an extra structure symbol by any possible defining expression).

First axioms

x,
Fnc x,
¬(Set(x) ∧ Fnc(x))
Set(Dom x)
E, ∀(parameters),
SetE, ∀SetF,
Fnc(Ext(x)) for any term t
EFEE=F (Axiom of Extensionality).
The latter redefines equality between sets from their equivalence as classes (letting elements in bulk): EFE means that E and F have the same elements (∀x, xExF) so that for any predicate R,

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

and similarly for ∃.

Axioms for functions. For any functor t (to be replaced by all terms that can define it), we have the following axioms, where the first one sums up the other 3 : for all values of parameters of t, any set E included in the definiteness class of t (this condition ∀xE, dt(x) is the definiteness condition for (Ext(x))), and all functions f and g,

f = (Ext(x)) ⇔ ( Dom f = E ∧ (∀xE, f(x) = t(x)))
Dom (Ext(x)) = E
xE, (Eyt(y)) (x) = t(x)
(Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ f = g

A general principle for the formalization of set theory

For any kind of meta-objects indirectly expressible and usable like objects in expressions, set theory will be enriched with tools to directly present them as objects. Namely, classes behaving as sets will be convertible into sets (1.11), and indirectly specified elements will become directly specified (2.4). But when the indirect expression of meta-objects (here, functors) may run over an infinity of possible expressions (here, any term), another reason is needed to see all these meta-objects as definite objects of a single kind (functions): the reason here is that the domains of these functors are sets, given as an argument to the definer. Otherwise, there cannot be a class of all functors, nor of all classes: naively trying to insert this in the same universe might lead to contradictions by reasonings like the proof of Russell's paradox.

Meta-objects behaving as objects with another role beyond sets and functions, will be represented as another kind of objects (operations, relations, tuples), and the conversion tools from roles (meta-objects) to objects will be completed by new conversion tools from objects into their roles. But this can be done inside the same set theory (just by developing it), as already present objects (sets or functions) can be found to naturally play the roles of these new objects. So, the new notions can be defined as classes of existing objects (that will offer their expressible features to the new objects), while the tools of interpretation and definition of objets (converting objects into their roles of meta-objects and inversely) are defined as abbreviations of some fixed expressions. Then, the only needed functors of conversion between objects playing the role of the same meta-object by different methods (expressions), will relate the different objects of old kinds that usefully represent in different ways the same object of the new kind.

Formalization of operations and currying

The notion of n-ary operation, objects acting as n-ary operators between n sets, would be formalized by: The notion of operation can be represented as a class of functions, in the following way called currying. The role of operation definer (binding n variables) is played by the succession of n uses of the function definer (one for each bound variable); and similarly as an evaluator, n uses of the function evaluator. For example (n=2), the binary operation f defined by the term (binary predicate) t with arguments x in E and y in F, may be formalized by

f ≈ (Ex ↦ (Fyt(x,y))) = g
f
(x,y) = g(x)(y) = t(x,y)

The intermediate function g(x) = (Fyt(x,y)) with argument y, sees x as fixed and y as bound. But this breaks the symmetry between arguments, and loses the data of F when E is empty but not the other way round. A formalization without these flaws will be possible using tuples (2.1.).

The formalization of n-ary relations involves an (n+1)-ary predicate of evaluation, and a definer binding n variables on a formula. We may either see n-ary relations as particular cases of n-ary operations (representing Booleans as objects), or see n-ary operations as particular cases of (n+1)-ary relations (see 2.3). And just like operations, relations can be reduced to the unary case in 2 ways : by currying (with n−1 uses of the function definer and 1 use of the set-builder, as will be done in 2.3 with n=2), or using tuples (2.1).

Set theory and Foundations of Mathematics
1. First foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions, objects, meta-objects
1.4. Formalizing types and structures
1.5. Expressions and definable structures
1.6. Connectives
1.7. Classes in set theory
1.8. Binders in set theory
1.9. Quantifiers

1.10. Formalization of set theory
1.11. Set generation principle
Philosophical aspects
Time in model theory
Time in set theory
  ⇨ Interpretation of classes
Concepts of truth in mathematics
2. Set theory (continued) 3. Model theory
Other languages:
FR : 1.10. Formalisation de la théorie des ensembles