1.8. Binders in set theory

The syntax of binders

This last kind of symbol can form an expression by taking a variable symbol, say here x, and an expression F which may use x as a free variable (in addition to the free variables that are available outside), to give a value depending on the unary structure defined by F with argument x. Thus, it separates the «inside» subexpression F having x among its free variables, from the «outside» where x is bound. But in most cases (in most theories...), binders cannot keep the full information on this unary structure, which is too complex to be recorded as an object as we shall see below.

We shall first review both main binders of set theory : the set-builder and the function definer. Then 1.9 will present both main quantifiers. Finally 1.10 and 1.11 will give axioms to complete this formalization of the notions of sets and functions in set theory.

The syntax differs between first-order logic and set theory, which manage the ranges of variables differently. In first-order logic, ranges are types, implicit data of quantifiers. But the ranges of binders of set theory are sets which, as objects, are designated by an additional argument of the binder (a space for a term not using the variable being bound).

Set-builder

For any unary predicate A definite on all elements of a set E, the subclass of E defined by A is a set : it is the range of a variable x introduced as ranging over E, so that it can be bound, from which we select the values satisfying A(x). It is thus a subset of E, written {xE | A(x)} (set of all x in E such that A(x)): for all y,

y ∈ {xE | A(x)} ⇔ (yEA(y))

This combination of characters { ∈ | } forms the notation of a binder named the set-builder: {xE | A(x)} binds x with range E on the formula A.

Russell's paradox

If the universe (class of all elements) was a set then, using it, the set builder could turn all other classes, such as the class of all sets, into sets. But this is impossible as can be proven using the set-builder itself :

Theorem. For any set E there is a set F such that FE. So, no set E can contains all sets.

Proof. F={xE | Set(x) ∧ xx} ⇒ (FF ⇔ (FEFF)) ⇒ (FFFE). ∎

This will oblige us to keep the distinctions between sets and classes.

The function definer

The function definer ( ∋ ↦ ) binds a variable on a term, following the syntax Ext(x), where Being definite if t(x) is definite for all x in E, it takes then the functor t and restricts its domain (definiteness class) to the set E, to give a function with domain E. So it converts functors into functions, reversing the action of the function evaluator (with the Dom functor) that converted (interpreted) functions into their role (meaning) as functors whose definiteness classes were sets.
The shorter notation xt(x) may be used when E is determined by the context, or in a meta description to designate a functor by specifying the argument x of its defining term.

Relations

A relation is a role playing object of set theory similar to an operation but with Boolean values : it acts as a predicate whose definiteness classes (ranges of arguments) are sets (so, predicates could be described as relations between interpreted types).

Now unary relations (functions with Boolean values), will be represented as subsets S of their domain E, using the set-builder in the role of definer, and ∈ in the role of evaluator interpreting S as the predicate x ↦ (xS). This role of S still differs from the intended unary relation, as it ignores its domain E but is definite in the whole universe, giving 0 outside E. This lack of operator Dom does not matter, as E is usually known from the context (as an available variable).

As the function definer (resp. the set-builder) records the whole structure defined by the given expression on the given set, it suffices to define any other binder of set theory on the same expression with the same domain, as made of a unary structure applied to its result (that is a function, resp. a set).

Structure definers in diverse theories

Let us call structure definer any binder B which, used on diverse expressions A, faithfully records the unary structure defined by A on some range E (type or class defined by an argument here implicit), i.e. its result S = (Bx, A(x)) can restore this structure by an evaluator V (symbol or expression) : V(S, x) = A(x) for all x in E. Admitting the use of negation and the possibility to interpret Booleans by objects (in a range with at least 2 objects, which is often the case), Russell's paradox shows that adding both following requirements on a structure definer in a theory would lead to contradiction :
  1. All such S belong to E
  2. V can occur in the expression A and use x anyhow in its arguments, namely V(x, x) is allowed, which makes sense as 1. ensures the definiteness of any V(S, S).
Let us list the remaining options. Set theory rejects 1. but keeps 2. But since 1. is rejected, keeping 2. may be or not be an issue depending on further details.

As will be explained in 4.9, extending a generic theory (whose ranges of binders were the types) by a new type K given as the set of all structures defined by a fixed expression A for all combinations of values of its parameters, forms a legitimate development of the theory (a construction). Indeed a binder on a variable structure symbol S with such a range K abbreviates a successive use of binders on all the parameters of A which replaces S. Here A and the system interpreting it come first, then the range K of the resulting S and their interpretations by V are created outside them : A has no sub-term with type K, thus does not use V (which has an argument of type K).

The notion of structure in first-order logic (as a one-model theory) has this similarity with the notion of set in set theory : for each given symbol type beyond constants, the class of all structures of that type is usually not a set, calling "sets" such ranges K (of structures defined by a fixed expression with variable parameters), or subclasses of these.
The fully developed theory with the infinity of such new types constructed for all possible expressions A, can become similar to set theory by gathering to a single type U all constructed types K of variable structures of the same symbol type (structures over the same sets), interpreted by the same symbol V (which could be already used by A). This merely packs into V different structures without conflict since they come from different types K of the first argument. This remains innocent (re-writing what can be done without it) as long as in the new theory, the binders of type U stay restricted to one of these "sets" K (or covered by finitely many of them, which are actually included in another one).

In set theory, the ranges of binders are the sets. Thus, beyond the simplifying advantage of removing types, set theory will get more power when accepting more classes as sets.

Other theories, which we shall ignore in the rest of this work, follow more daring options:
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. Structures of mathematical systems
1.5. Expressions and definable structures
1.6. Logical 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. Algebra - 4. Arithmetic 5. Second-order foundations
Other languages:
FR : 1.8. Symboles liants en théorie des ensembles