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
{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 set-builder: {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 set-builder 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 set-builder 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 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).
Other languages:
FR : 1.8. Symboles
liants en théorie des ensembles