[FOM] Fwd: Re: Replacement

[Alex Simpson]

Two further comments on Replacement.

1. Thomas Forster asks

> I know there are lots of people who dislike the axiom scheme of
> replacement.  They say things like ``it has no consequence for
> ordinary mathematics'' and the like.  Unfortunately i have none
> of them handy at the moment, so i have to ask:  do any of them
> think that the axiom scheme is actually *false*?  Or do they
> merely think that it shouldn't be a core axiom?

One can give many reasons for questioning the axioms of set theory,
but Replacement need not necessarily be the first target.
Constructive mathematics, for example, provides an interesting view on 
which axioms of set theory are unreasonable. Constructive set theories 
(for example, Aczel's CZF) typically retain full Replacement (usually 
as a consequence of intuitionistically stronger collection axioms), but 
drop/weaken other axioms instead (in CZF, Powerset is replaced by a 
"subset collection" axiom; Separation, which is not intuitionistically 
a consequence of Replacement, is weakened to bounded formulas). As 
Aczel showed, this can all be constructively justified via an 
interpretation of CZF in Martin-Lof type theory.

So, indeed, why doubt Replacement?


2. On the classical Z vs. ZF distinction, Andrej Bauer writes:

> Isn't replacement required for construction of initial algebras (and
> final coalgebras) of functors? This is certainly "ordinary math" as 
> such constructions are used in
> topology, algebra and theoretical computer science, at least.

A precise result in this direction is that the following theorem
(an instance of Dana Scott's approach to solving "recursive domain 
equations") is provable in ZF but not in Z:

    For every directed-complete pointed (i.e. with least element)      
partial order (dcppo) A, there exists a dcppo D satisfying
    the "isomorphism equation":

           D   \isomorphic-to   A \oplus [D -> D]

    where [D -> D] is continuous function space of dcppo's and \oplus
    is coalesced sum (disjoint sum with least elements identified)

The argument that this is not provable in Z follows from Example 
9.6.15(e) of Taylor's "Practical Foundations of Mathematics".
(One can find a countable dcppo A such that any suitable D has 
cardinality at least \beth_\omega.)

In response to Andrej Bauer's message, Harvey Friedman writes,

> This is certainly not ordinary mathematics, although some ordinary
> mathematicians might sometimes choose to cast things this way for
> expositional purposes. I.e., you can choose to set things up with heavy
> doses of generality and abstraction, and make use of unusual axioms.

Well, the example above is a rather concrete statement in domain theory
and the axiom systems are Z and ZF. Of course, people will differ on 
whether or not domain theory should count as "ordinary mathematics". 
Perhaps it should be considered extraordinary mathematics instead.

Alex

-- 
Alex Simpson, LFCS, School of Informatics, Univ. of Edinburgh, UK
Email: Alex.Simpson at ed.ac.uk             Tel: +44 (0)131 650 5113
Web: http://homepages.inf.ed.ac.uk/als   Fax: +44 (0)131 667 7209