On the issue of Replacement

[David Roberts <david.roberts@adelaide.edu.au>]

Dear all,

I have been thinking lately about the uses of Replacement in ordinary
mathematics, viewed from the lens of ETCS. In particular, I wanted to
clear up what one might do to circumvent assuming Replacement (or an
equivalent) on top of ETCS, for instance. Key examples of what
Replacement allows us to do include forming colimits of 'diagrams'
specified by logical formulas (for instance the sequence where the
n^th term is the coproduct of the P^k(N) for k < n, together with
inclusions). I write 'diagrams' since these are not internal diagrams,
as is usual in topos theory, nor diagrams (as far as I can tell) in an
expanded vocabulary that allows us to talk of functors D --> Set
(please correct me if I'm wrong!).

In my naivety, I asked a question on MathOverflow [1] asking what is
wrong with the suggestion of having some sort of cocompletion of Set
(in an external sense) around that allows careful and guarded use of
formal colimits, as encoded by diagrams (or 'diagrams' in the above
sense).

Discussion there didn't proceed as I imagined, but led me to realise
(thanks to Zhen Lin and Francois Dorais) that the distinction between
internal and external indexing is what is going on. For instance, with
the 'diagram' involving iterated powersets above, one must distinguish
between the internal natural numbers and the natural numbers in the
metalogic.

So my question might now be approached in various ways

1) Asking if there a sensible way to talk about cocompletion (or other
such constructions) under 'diagrams'. This is somewhat analogous to
talking about proper classes in ZFC, which "do not exist", but are
handy stand-ins for first-order formulas -- and in fact one might as
well work with the category of classes defined as such, or in the
"model" of NBG so arising (conservative over ZFC, a desideratum since
we are primarily interested in sets)

2) Asking that internal and external natural numbers coincide - this
is analogous to \omega-models in material set theory. Of course, this
merely copes with 'diagrams' indexed by N (and possibly countable
'diagrams'). This should be enough for cases of the small object
argument that only use \omega-many arrows. Obvious generalisations for
other ordinals hold, but I suspect that assuming this works for all
ordinals implies Replacement (cf [2]). There are obviously analogues
for any fixed class of shape of 'diagram': I'm fairly sure that if the
diagram exists corresponding to any 'diagram', then any colimit of
that shape exists.

Any thoughts, comments, or existing work exploring these issues?

Thanks,

David

=References=
[1] http://mathoverflow.net/questions/208711/who-needs-replacement-anyway
[2] http://jdh.hamkins.org/transfinite-recursion-as-a-fundamental-principle-in-set-theory/

-- 
Dr David Roberts
Visiting Fellow
School of Mathematical Sciences
University of Adelaide
SA 5005
AUSTRALIA

"When I consider what people generally want in calculating, I found
that it always is a number."
-- al-Khwārizmī


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]