## 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 the main binders in set theory.
### Definitions of functions by terms

The *function definer* ( ∋ ↦ ) binds a variable on a term,
following the syntax (*E* ∋ *x* ↦ *t*(*x*)),
where *x* is the variable, *E* is its range, and *t*(*x*)
is the term (here abbreviated as a unary predicate with possible
implicit parameters); it may be shortened as (*x* ↦
*t*(*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 defined by *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 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. 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
{*x*∈*E* | *A*(*x*)}
(set of all *x* in *E* such that *A*(*x*)): for
all *y*,
*y* ∈ {*x*∈*E* | *A*(*x*)}
⇔ (*y* ∈ *E* ∧ *A*(*y*))

The binder { ∈ | }, is named the *set-builder*: {*x*∈*E* | *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 (*x* ∈ *F*)
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).
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 F ∉ *E*.

Proof. *F*={*x*∈*E* | Set(*x*) ∧ *x* ∉ *x*}
⇒ (*F* ∈ *F* ⇔ (*F* ∈ *E* ∧ *F* ∉ *F*))
⇒ (*F* ∉ *F* ∴ *F* ∉ *E*). ∎
This will oblige us to keep the distinctions between sets and
classes.

Other languages:

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