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 setbuilder 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 firstorder logic and set theory, which manage the
ranges of variables differently. In firstorder 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).
Setbuilder
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
{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))
This combination of characters { ∈  } forms the notation of a binder
named the setbuilder: {x∈E  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 setbuilder itself :
Theorem. For any set E there is a set F
such that F ∉ E. So, no set E can contains all sets.
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.
The function definer
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,
 the notation
"t(x)" stands for any term, here abbreviated (to describe
the general case) using the functor symbol t defined by this term with
argument x (and possible parameters here kept implicit).
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 x ↦ t(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 setbuilder in the role of definer, and ∈
in the role of evaluator interpreting S as the predicate
x ↦ (x ∈ S).
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 setbuilder) 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 :
 All such S belong to E
 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 subterm with type K, thus does
not use V (which has an argument of type K).
The notion of structure in firstorder logic (as a onemodel 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 (rewriting 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:
 Keeping 1. and rejecting 2. will be shown consistent by
Skolem's Paradox (4.6)
but would be quite unnatural.

Even weirder is NF
("New Foundations", so called as it was new when first published in 1937),
combining 1. with a lighter version of 2. restricting the possible syntax of
A to forbid occurrences of (x∈x) or any way to define it.
 The most extreme is lambda
calculus, that keeps both points but
tolerates the resulting contradiction by ignoring Boolean logic with its
concept of "contradiction". This "theory" does not describe any object but
only its own terms, seen as computable functions. As a computation system,
its contradictions are computations which keep running, never giving any
results.
Other languages:
FR : 1.8. Symboles
liants en théorie des ensembles