Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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 ETCSETCS 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 ETCSETCS 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 ETCSETCS 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 BSEARBSEAR or BZ BZ^\circlearrowleft, as you know.)

    • CommentRowNumber6.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 4th 2011

    @Toby,

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

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeAug 4th 2011

    Bounded unfounded Zermelo. Take a normal version of ZFCZFC, 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:sVf: s \to V, where ss 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 nP n(X)\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 nP n(X)n \mapsto P^n(X) when XX 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 ETCSETCS.

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