[FOM] Replacement in mathemaical practice and in predicative math

[Arnon Avron]

As Forster noted in a recent message to FOM, the replacement
axiom is notorious among many as "being unnatural",
"having no consequence for ordinary mathematics" and "responsible
for the unreasonable strength of ZF" (where in this one usually
means the availability in ZF of high cardinals like 
\aleph_{aleph_\omega} which indeed are never used in 
ordinary mathematics). Most of these claims are simply
false (as I shall shortly demonstrate). The last one
becomes true only in the presence of the most problematic
axiom of ZF: the powerset axiom. Only the *combination*
of powerset and replacement makes it possible to 
prove the existence of big cardinals which are far remote
from mathematical practice. As is well known, replacement
alone, without powerset, is not sufficient for proving 
the existence of any set which is not at most countable.
In contrast, powerset alone, even without replacement,
(but with separation) suffices for proving the existence
of infinitely many infinite cardinals. This makes it
clear that the unreasonable strength of ZF should mainly
be attributed to the powerset axiom, not to replacement.

 Let us turn now to the role of replacement in "ordinary
mathematics". In general, set-theoretical language and principles
are indispensable in modern mathematical practice. This is evident
from the fact that almost any modern textbook in almost every
area of mathematics starts with some review of set-theoretical
concepts, notations, and principles. However, except for
professional logicians and set-theorists, nobody who
practices mathematics (be it a student or a professor)
makes it explicit what axioms of set-theory s/he is using.
In a lot of cases the same argument or construction
can be justified in two different ways, either using
replacement, or by using separation together with powerset
(this fact is what makes it possible for some people to
claim that replacement is never used in ordinary mathematics).
How are we to tell which of the two options was (implicitly,
perhaps unconsciously) used in a given case? This might
seem to be a difficult question, but actually
in most cases the answer is very simple: just look at
the *notation* that was employed!

  In addition to very basic notations for simple operations
like union, intersection, and Cartesian product, there are
in mathematical texts two main methods for denoting sets (and 
thereby implicitly proving the existence of those sets). They
have the following forms:

[SEP]: {x\in s: A} 
                   (where x is a variable, s is a set term in
                    which x is not free, and A is a formula)
[REP]: {t: x\in s} 
                   (where x is a variable, s is a set term in
                    which x is not free, and t is a term)

Using notation of the form [SEP] is the way the principle of
separation is used in ordinary mathematics, while using
notation of the form [REP] is the way the principle of
replacement is used in ordinary mathematics. The two forms
indeed exactly represent the essence of these principles, and
with strong-enough means for introducing terms or formulas
they actually provide the full power of these principles.
(At this point it might be appropriate to explain  why I am referring
to [SEP] and [REP] above as *principles* rather than as axioms
or even axiom-schemas. The reason is that they become
axiom schemas only when the language is precisely specified,
in particular: when it is clearly defined what terms are legitimate
and what are the wffs. This is usually left implicit in 
normal mathematical discourse, and may vary significantly.
The principle may (and are) used  for different languages,
and their strength varies accordingly).

Returning to the main question, an examination
of the notations used in normal mathematical texts should leave
no doubt that the replacement principle is by far used more
in mathematical practice than the combination of powerset and 
separation.  Take a simple example: when asked to write a term 
denoting the set of singletons of elements of N, I bet that at least
999 mathematicians (either in the broad sense, including first-year 
students, or in a narrower sense) out of 1000 would write:

                           {{n}: n\in N}
and not
                 {x\in P(P(N)):\exist n\in N. x={n}}

This is not only because the former is shorter, but because it directly
translates the definition in words of this set, and precisely
reflects our intuition how this set is formed/constructed. In contrast,
one has to think for a while in order to get the second definition
correctly (and for many students it is even difficult at first
to understand why this term is a correct description of this set. Anyone
who have taught a basic course in set theory or discrete mathematics
has experienced this). It is clear therefore that practically everyone
relies on replacement for getting this set, and not on the powerset axiom
(indeed, the set {{n}: n\in N} is much simpler than P(P(N)), and much,
much less problematic than the later. It makes therefore no sense to base
the existence of {{n}: n\in N} on that of P(P(N))!).

Take another example. In the official formulation of ZF, the union
axiom says that $\bigcup X$ exists for every set X. However, 
the notation $\bigcup X$ is practically never used in
normal mathematical texts. What is used instead is the notation
$\bigcup_{i\in I} A_i$, which is an abbreviation for
$\bigcup(\{A_i: i\in I\})$. Needless to say, referring to {A_i: i\in I}
(which is usually called "an indexed family of sets") and using it 
is a direct application of [SEP]. Now in the important case
where all the A_i's are subsets of some accepted set E
one again may replace the use of replacement by a combination
of separation and two applications of powerset - and again, mathematicians
never think in this way, because it makes little sense to justify the
existence of $\bigcup(\{A_i: i\in I\})$ by relying on the
acceptance of P(P(E)). Can anybody seriously claim 
that a mathematician who mentions the set of closed intervals
 {[1/n,1-1/n]: n\in N} (noting e.g. that its union is the open 
interval (0,1)) is implicitly assuming the existence of P(P(R))??
Yes, the use of replacement can in principle be avoided here (if one 
has no troubles with P(P(R))), but this does not change the fact that
in practice it is replacement which is really used!

  Let me finally mention the role of these three set-theoretical 
principles in predicative mathematics. The powerset axiom is of course
totally rejected there (except for finite sets). [REP], in turn,
is only partially accepted: not every formula A can be used
in a term of the form {x \in t: A}, but only special types
of formulas (e.g. \delta_0 formulas). In contrast, the principle
[SEP] is fully accepted in the way it is formulated above
(which is the way it is used in mathematical practice):
whenever $t$ and $s$ are legitimate terms so is {t: x\in s}
(provided x is not free in s). This of course does not
mean that the axiom of replacement  of ZF is predicatively valid:
the practice of ZF allows to introduce a new function symbol
F_A (and then apply [REP] to terms that use it) whenever the formula
$\forall x \exist \! x. A$ has been proved - and not for every 
formula A is this procedure legitimate in predicative mathematics 
(for some it is, for some it is not). However, the problem here is not
with [REP] itself, which is completely unproblematic, but
with the use (for forming terms) of *other* platonistic principles. 

   Thus in predicative mathematics the existence of {{n}: n\in N}
or of {[1/n,1-1/n]: n\in N} can be justified *only* by replacement -
exactly what the notations used by mathematicians reflect. This
is another demonstration of Weaver's thesis (put forward
in several postings to FOM and in his papers) concerning the 
remarkable match that exists between predicatively acceptable mathematics 
and normal mathematical practice.