1.8. Binders in set theory

The syntax of binders

The last kind of symbols forming expressions is the binders (binding symbols).
Such a symbol binds one (or more) variable(s) (say x), on an expression F which may use x as a free variable in addition to the free variables that are available (with a value) outside. Thus, it separates the «inside» subexpression F using x as free, from the «outside» where x is bound. Applied to the data of the symbol x and the expression F, it gives a value depending on the unary structure defined by F with argument x (but cannot generally give a whole faithful image of this unary structure, which may be too complex to be fully recorded as a mere object).
The syntax differs between set theory and generic theories, which manage the range differently. In generic theories, ranges are types, implicit data of quantifiers. But binders of set theory make their variable range over a set, that is an object designated by an additional argument (a space for a term not using the bound variable).

An expression is ground if all its variables are bound (their occurrences are contained by binders).

Let us review both main binders of set theory : the function definer and the set builder.

Definitions of functions by terms

The function definer ( ∋ ↦ ) binds a variable on a term, following the syntax (Ext(x)), where x is the variable, E is its range, and t(x) is the abbreviation of any term, denoted as a functor t with argument x and possible implicit parameters; it may be shortened as (xt(x)) when E is determined by the context. It is definite if t(x) is definite for all x in E; it takes then the functor t and restricts its definiteness class to E, to give it as a function with domain E.
So it converts functors into functions, reversing the action of the function evaluator that converted functions into their role (meaning) as functors whose definiteness classes were sets. This uniformizes the functors (which were only indirectly available to be used as functions by their defining term that could have unlimited complexity) as a unique kind of objects.
In 1.10. we will formalize this tool, and in 1.11 see it as a particular case of a more general principle for set theory.

Relations and set-builder symbol

A relation is an object similar to an operation but with Boolean values: it acts as a predicate whose arguments range over sets (so, a predicate is a relation between interpreted types). But this does not need to be introduced as another kind of objects, as sets will suffice to play these roles.

For any unary predicate A definite in a set E, the subclass of E defined by A is a set (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)), 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))

The binder { ∈ | }, is named the set-builder: {xE | A(x)} binds x with range E on A. It will be used as a definer for unary relations on E, figured as subsets F of E, evaluated by ∈ as predicates (xF) with argument x. But these predicates are not only definite in E but in the whole universe, giving 0 outside E whose data is lost. This lack of operator Dom does not matter, as the domain E is usually determined by the context.
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 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).

Russell's paradox

Of course, if the class of all objects was a set then the set builder could use it to also convert all classes into sets. But this is not possible: the class of all sets cannot be a set (no set E can ever contain all sets), as can be shown using the set builder itself:

Theorem. For any set E there is a set F such that FE.

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

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

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. Model theory

Other languages:
FR : 1.8. Symboles liants en théorie des ensembles