Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
A term that I see sometimes in discussions of foundations: ordinary mathematics.
Interesting; I’ve never encountered that. Can you give some example references?
The only one that I know that defines the term at all precisely is the Wikipedia article (which itself has no references, but at least it wasn’t written by me, unlike Wikipedia: Universe (mathematics), which also discusses this issue, but that proves nothing since I wrote it).
I’m not sure which books used this phrase (however imprecisely), but probably something from this list:
I list because they’re the things on foundations that I was reading when I must have encountered the term; as you can see, they’re all about constructivism, so the term might not be used outside there.
It seems a shame to take a nice vague phrase like that and give it some precise meaning that already has another name (like “formalizable in ETCS”).
I think that a good case can be made, however, that this is the kind of mathematics that most mathematicians deal with (or at least that this was so in the bulk of the 20th century). After all, the constructions of structured sets involving power sets, functions, etc, all live here. The practical value of pointing to $ETCS$ as a worthwhile categorial foundation of mathematics is that it really is sufficient for the mathematics that people do. (To quote a title of one of Lawvere’s books, the objects of a model of $ETCS$ are ‘sets for mathematicians’, as opposed to philosophers, logicians, or metamathematicians.)
However, I don’t think that it really is supposed to have a precise meaning. Thus, I write ‘One might define it as’, not ‘It is defined as’. That $ETCS$ is a foundation for such mathematics is a useful empirical discovery, not a definition or even a theorem. (And of course, it has nothing in particular to do with categorial foundations, as one could just as easily define it as mathematics formalisable in $BSEAR$ or $BZ^\circlearrowleft$, as you know.)
@Toby,
what is $BZ^\circlearrowleft$? (Bounded Zermelo ???something)
Bounded unfounded Zermelo. Take a normal version of $ZFC$, remove choice (but keep classical logic), replace replacement/collection and separation with bounded separation, and remove foundation (but keep infinity in a form that doesn’t require foundation to justify induction).
The directed circle is supposed to indicate the possibility of loop in the membership graph of the von Neumann universe, since foundation is gone.
Toby 5: I wouldn’t argue with that case; I was just arguing against assigning any particular meaning to such a generally applicable phrase. I’ve added a sentence to ordinary mathematics along the lines of the meaning I’d like to be able to use it with; any objection?
I’m a bit surprised to see replacement named an extraordinary axiom. Don’t you need replacement to form infinitary coproducts in ZFC? Or is there a clever construction that lets you avoid it?
Neel: I can’t be sure what your worry is, but this question was raised by arsmath (Walt Pohl) at MO. I thought the accepted answer (by Peter Le Fanu Lumsdaine) was excellent and very much to the point: it depends on how you understand a function $f: s \to V$, where $s$ is a set. Here is a relevant remark made in the comments before the answer appeared –
Andreas Blass: Rephrasing for emphasis what Carl Mummert said above: The problem with $\bigcup_n P^n(X)$ in the absence of replacement is not the coproduct but the iteration of the power set. It is provable in Zermelo set theory (ZF without replacement) that any set-indexed family of sets has a coproduct that is a set. (Limits and colimits of small-indexed diagrams of sets are OK too.) But Zermelo set theory does not prove the existence of the sequence of iterated power sets $n \mapsto P^n(X)$ when $X$ is, for example, the set of natural numbers.
There is some related discussion also at cocomplete well-pointed topos.
@ Mike #8: I regret that I can find nothing to object to in your sentence. (^_^)
Neel: I agree with Todd. The point is that one can do most of category theory without replacement, as long as one is willing to define “family of sets” in the appropriate way. In fancy language, this amounts to working with Set-indexed categories, and in particular using the codomain fibration to represent Set itself, rather than its “naive indexing”.
I believe that replacement is used rather more irreplaceably in some other places in category theory, such as the small object argument and other transfinite colimit constructions.
One should add to Zhen Lin #10: Not just separation suffices, but bounded separation. So it really is ordinary mathematics, in the sense that it can be formalised in $ETCS$.
I’ve added a bit to this, making it more clear that the term is informal and also linking the concept to predicativity.
1 to 15 of 15