Responding to David Roberts contribution here (cf. infra) on the axiom of replacement, or as Paul Halmos dubs it, the axiom of substitution, I think it instructive to have a gander at the discussion centering around its appearance on page 75 of Halmos' Naive Set Theory (Springer UTM edition, ISBN 978-0-387-90092-6). The point seems to be that, with it, one can parlay a purely linguistic "bijection" between the various natural numbers, on the one hand, and the various iterated successors of the first infinite ordinal {/omega} (whose existence the axiom of infinity guarantees) into a full-fledged set, closed under successors (the successor X+ of a set X is the union of X with the singleton set whose only member is X, X+ = X {/union} {X}), with {/omega} as member, and minimal with regards to those two features, ... ... along with a bijection between that and the natural numbers. With that, one can then be assured of the existence of an ordinal whose elements include (i) all the natural numbers, and (ii) all the various finitely iterated successors of {/omega}, ordinal one would be hard pressed to know exists as a set, absent that axiom. Yes, it's a colimit of a *seeming* diagram of sets ... but it's really not a *proper* diagram: there's something distinctly not kosher, not halal, about it. It's as bad as a fibration over N, with fiber over n being the n^th iterated successor of {/omega}, but without there being any actual total space over the base N. (Thanks to Bill Lawvere for bring up this view of things.) I hope my shining a bit of light into this fog has more lit up the road ahead than merely blinded us hapless drivers. Cheers, -- Fred ------ Original Message ------ Received: Wed, 10 Jun 2015 09:08:33 AM EDT From: David Roberts <david.roberts@adelaide.edu.au> To: "categories@mta.ca list" <categories@mta.ca> Subject: categories: On the issue of Replacement
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-s...
-- 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/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]