## 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.10 will present both main quantifiers. Finally 2.1 and 2.2 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.

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
• 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 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).

 Set theory and Foundations of Mathematics 1. First foundations of mathematics 1.8. Binders in set theory ⇨ 1.9. Axioms and proofs 2. Set theory - 3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : 1.8. Symboles liants en théorie des ensembles