# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTobyBartels
• CommentTimeJul 31st 2011

A term that I see sometimes in discussions of foundations: ordinary mathematics.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeAug 1st 2011

Interesting; I’ve never encountered that. Can you give some example references?

• CommentRowNumber3.
• CommentAuthorTobyBartels
• CommentTimeAug 1st 2011

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:

• Michael Beeson, Foundations of Constructive Mathematics: Metamathematical Studies;
• Douglas Bridges & Fred Richman, Varieties of Constructive Mathematics;
• Micheal Dummett, Elements of Intuitionism;
• Anne Troelstra & Dirk van Dalen, Constructivism in Mathematics.

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.

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeAug 2nd 2011

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”).

• CommentRowNumber5.
• CommentAuthorTobyBartels
• CommentTimeAug 4th 2011

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.)

• CommentRowNumber6.
• CommentAuthorDavidRoberts
• CommentTimeAug 4th 2011

@Toby,

what is $BZ^\circlearrowleft$? (Bounded Zermelo ???something)

• CommentRowNumber7.
• CommentAuthorTobyBartels
• CommentTimeAug 4th 2011

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.

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeAug 5th 2011

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?

1. 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?

• CommentRowNumber10.
• CommentAuthorZhen Lin
• CommentTimeAug 5th 2011
If you have an honest function indexing the summands, then if I'm not mistaken the separation axiom suffices: take an iterated union of the graph of the function to obtain the union over the codomain (plus junk), take the cartesian product of that set with the indexing set (using unions, power sets, and separation), then take the double power set of that, and separate out a set of functions.
• CommentRowNumber11.
• CommentAuthorTodd_Trimble
• CommentTimeAug 5th 2011

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.

• CommentRowNumber12.
• CommentAuthorTobyBartels
• CommentTimeAug 10th 2011

@ Mike #8: I regret that I can find nothing to object to in your sentence. (^_^)

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeAug 10th 2011

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.

• CommentRowNumber14.
• CommentAuthorTobyBartels
• CommentTimeAug 20th 2011

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$.

• CommentRowNumber15.
• CommentAuthorTobyBartels
• CommentTimeAug 20th 2011

I’ve added a bit to this, making it more clear that the term is informal and also linking the concept to predicativity.