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 complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric 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).

nLab > Latest Changes: foundation of mathematics

Bottom of Page

1 to 29 of 29

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeSep 5th 2012
    • (edited Sep 5th 2012)

    at foundation of mathematics I have tried to start an Idea-section.

    Also, I am hereby moving a bunch of old discussion boxes from there to here:

    [ begin forwarded discussion ]

    +– {: .query} Urs asks: Concerning the last parenthetical remark: I suppose in this manner one could imagine (n+1)(n+1)-categories as a foundation for nn-categories? What happens when we let n→∞n \to \infty?

    Toby answers: That goes in the last, as yet unwritten, section. =–

    +– {: .query} Urs asks: Can you say what the problem is?

    Toby answers: I'd say that it proved to be overkill; ETCS is simpler and no less conceptual. In ETCC (or whatever you call it), you can neatly define a group (for example) as a category with certain properties rather than as a set with certain structure. But then you still have to define a topological space (for example) as a set with certain structure (where a set is defined to be a discrete category, of course). I think that Lawvere himself still wants an ETCC, but everybody else seems to have decided to stick with ETCS.

    Roger Witte asks: Surely in ETCC, you define complete Heyting algebras as particular kinds of category and then work with Frames and Locales (ie follow Paul Taylor’s leaf and apply Stone Duality). You should be able to get to Top by examining relationships between Loc and Set. I thought Top might be the the comma category of forgetful functor from loc to set op and the contravariant powerset functor. Thus a Topological space would consist of a triple S, L, f where S is a set, L is a locale and f is a function from the objects of the locale to the powerset of S. A continuous function from S, L, f to S’, L’, f’ is a pair g, h where g is a function from the powerset of S’ to the powerset of S and g is a frame homomorphism from L’ to L and (I don’t know how to draw the commutation square). However I think this has too many spaces since lattice structures other than the inclusion lattice can be used to define open sets.

    Toby: It's straightforward to define a topological space as a set equipped with a subframe of its power set. So you can define it as a set SS, a frame FF, and a frame monomorphism f:F→P(S)f\colon F \to P(S), or equivalently as a set SS, a locale LL, and an epimorphism f:L→Disc(S)f\colon L \to Disc(S) of locales, where Disc(S)Disc(S) is the discrete space on SS as a locale. (Your ’However, […]’ sentence is because you didn't specify epimorphism/monomorphism.) This is a good perspective, but I don't think that it's any cleaner in ETCC than in ETCS.

    Roger Witte says Thanks, Toby. I agree with your last sentence but my point is that this approach is equally clean and easy in both systems. The clean thing about ETCC is the uniformity of meta theory and model theory as category theory. The clean thing about ETCS is that we have just been studying sets for 150 years, so we have a good intuition for them.

    I was responding to your point ’ETCC is less clean because you have to define some things (eg topological spaces) as sets with a structure’. But you can define and study the structure without referring to the sets and then ’bolt on’ the sets (almost like an afterthought).

    Mike Shulman: In particular cases, yes. I thought the point Toby was trying to make is that only some kinds of structure lend themselves to this naturally. Groups obviously do. Perhaps topological spaces were a poorly chosen example of something that doesn’t, since as you point out they can naturally be defined via frames. But consider, for instance, a metric space. Or a graph. Or a uniform space. Or a semigroup. All of these structures can be easily defined in terms of sets, but I don’t see a natural way to define them in terms of categories without going through discrete categories = sets.

    Toby: Roger, I don't understand how you intend to bolt on sets at the end. If I define a topological space as a set SS, a frame FF, and a frame monomorphism from FF to the power frame of SS, how do I remove the set from this to get something that I can bolt the set onto afterwards? With semigroups, I can see how, from a certain perspective, it's just as well to study the Lawvere theory of semigroups as a cartesian category, but I don't see what to do with topological spaces.

    Roger Witte says If we want to found mathematics in ETCC we want to work on nice categories rather than nice objects. Nice objects in not nice categories are hard work (and probably ’evil’ to somke extent). Thus the answer to Toby is that to do topology in ETCC you do as much as possible in Locale theory (ie pointless topology) and then when you finally need to do stuff with points, you create Top as a comma like construction (ie you never take away the points but you avoid introducing them as long as possible). Is it not true that the only reason you want to introduce points is so that you can test them for equality/inequality (as opposed to topological separation)?

    Mike, I spent about two weeks trying to figure out how to get around Toby’s objection ’topology’ and now you chuck four more examples at me. My gut feeling is that the category of directed graphs is found by taking the skeleton of CAT, that metric locales are regular locales with some extra condition to ensure a finite basis, that Toby can mak

    [ to be continued in next comment ]

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeSep 5th 2012

    [ continuation of forwarded discussion ]

    +– {: .query} Urs says: I like categorial. If we think we can improve on existing terminology we should feel free to introduce it here.

    Toby responds: Once you use ’categorial’ when discussing logic, it's hard to justify using ’categorical’ in other contexts. I suppose that I could go through the whole wiki and change ’categorical’ to ’categorial’ ….

    Urs says: with respect to optimal terminology I think that one problem is that the very term “category” is not optimal.

    Toby responds: I think that it's too late to play Bourbaki with that. Or do you want to say ’semigroupoid’? (which occasionally appears in groupoid literature but most properly would not have identity morphisms). I got a lot of stares over dinner at Groupoidfest when I said that that might be a better term after all (for categories as algebraic objects).

    Mike comments: I think it is probably too late to play Bourbaki with “categorical” as well; too many people are using it who don’t care about logic. However, there is another option here: I like to call ETCS-like theories structural set theories rather than “categori(c)al foundations”. As Lawvere and others have pointed out, ETCS is still a theory of sets; it merely differs from traditional set theories such as ZF in its lack of a global membership predicate and in what notions it takes as basic.

    Toby: Can we at least say ’category-theoretic’ instead of ’categorical’? It can be very disconcerting to read, for example on tensor product, ’More categorically, this can be constructed as the coequalizer of the two maps […]’. (If anything, this is less categorical than the explicit previous construction by modding out relations, since the previous can be formalised in a membership-based set theory in which it is defined up to set-theoretic identity, while the other, however formalised, is defined only up to unique isomorphism. Of course, that should not really be considered less categorical, but it's still hardly more categorical.) To be unambiguous, this should be ’More categorially, […]’ or, if you don't like that word, ’More category-theoretically […]’. (Or do you think that ’More structurally […]’ will work here?)

    Mike: At some point, I think one just has to accept that some words have more than one meaning, and learn to deal with it. I appreciate that it can be disconcerting to a logician or philosopher to read “categorical” used to mean “category-theoretic,” but it is of course just as confusing to a category-theorist when it is used to mean “having a unique model.” Undoubtedly the logicians were there first, but the time to have that argument was back when Eilenberg and Mac Lane chose the word “category.” And although I am of course biased, I think that “category-theoretic” is a more important notion in mathematics than “having a unique model.” And “categorial” looks to me like a misspelling.

    Toby: Erm, no, while the term ’category’ may have some problems that one might have objected to in 1945, that was not the time to anticipate that people might later apply it to logic and then use the adjective ’categorical’. I understand why you don't like ’categorial’, so what's wrong with ’category-theoretic’ or ’structural’? (when discussing logic, that is).

    Mike: I didn’t mean to say that anyone should have been able to anticipate the conflict of “categorical” related to categories with its use in logic back in 1945. I just meant that by now, when “category” has a universally established meaning, I don’t think it’s reasonable to object to the use of “categorical” to mean “related to categories.” I like “structural” when it applies, but to me it has a different meaning than “categorical”—this is the point I’m trying to make with SEAR, that structural set theory doesn’t depend on category theory. Finally, “category-theoretically” has almost twice as many syllables and letters as “categorically,” and sounds awkward.

    I am sort of starting to soften towards “categorial,” at least when talking to logicians or about logic. There’s enough antagonism towards category theory in the logic/foundations community without adding to the perception that we’re stealing established terminology. But I’m not yet convinced that it’s worth going on a crusade to eliminate “categorical” referring to category theory from everyday mathematical speech.

    Toby: I don't feel on a crusade, but I avoid using ’categorical’. I often used ’categorial’, or I'll use ’category-theoretic’ or ’structural’ if that seems more appropriate. (In the case of the tensor product, for example, I think that using ’structural’ gets across the idea perfectly well; if someone has already written ’categorical’ on the wiki and its seems disconcerting, then I wouldn't change it to ’categorial’ but might change it to ’category-theoretic’.) =–

    [ end of forwarded discussion ]

    • CommentRowNumber3.
    • CommentAuthorzskoda
    • CommentTimeSep 5th 2012
    • (edited Sep 5th 2012)

    Thanks, Urs. I have added to the foundation of mathematics (under references) backpermalink to this archived version of the old discussion. IMHO we should always keep at entries backlinks to the archived versions of removed discussions, unless they are extremely obsolete or nonsubstantial. Otherwise the discussion is lost in nnForum.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeSep 5th 2012
    • (edited Sep 5th 2012)

    I think entries should only point to relevant information, not to every discussion vaguely related. I don’t think my questions to Toby from years ago in the above are relevant enough. I’d rather have them not linked from the entry. I’d rather find 5 minutes to add to the entry a nice and polished paragraph that contains the outcome of these discussions.

    • CommentRowNumber5.
    • CommentAuthorzskoda
    • CommentTimeSep 5th 2012
    • (edited Sep 5th 2012)

    I do not know. Here is about 4 pages of discussion among several people, some of which is interesting and not absorbed in the entry. The purpose of references is not to point to the material identical to the entries nor necessary central to the entry but to point to expansions and further directions and related items. I do not know, I had the impression that it was not obsolete.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeSep 5th 2012

    I just think that none of those people over the years felt that any of this was relevant or polished enough to put it into an nLab entry as usual. It sure stayed there only because everybody forgot about those discussion boxes.

    Which is not to say that we should not work on that entry. That entry deserves to be improved! But it improves by adding contentful focused paragraphs, not random and unfocused chitchat. That is better had here in a discussion forum.

    • CommentRowNumber7.
    • CommentAuthorzskoda
    • CommentTimeSep 5th 2012
    • (edited Sep 5th 2012)

    But it is lost if not backlinked. I think that when I get into such a discussion it absorbs about half an afternoon, so it is often a pity to loose it, from my subjective perspective. Having something idle for one year is little in comparison to the timespan of idle logs of most unfinished mathematical thoughts I usually have (I understand it might look much longer time for superquick, focused and superefficient people like you) including unfinished circles ofnnLab entries. Backlink is about half a line, and if one has further discussion boxes in the same entry later it is likely that the person who removes that one will than archive it in the same nnForum spot what will once be useful. Otherwise, in long term, during the many years, the accumulated queries from one entry will be in many nnForum threads (( I am just talking now the matter of the principle. ))

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 5th 2012

    I think I’m with Zoran here. Such discussions can be of both scientific and historical interest (providing inner thoughts and motivations which are a stimulus to many), and an unobtrusive backlink wouldn’t mar an otherwise fine (or polished) article.

    The Lab-book analogy would seem to support the idea of keeping information which is useful to researchers like Zoran accessible.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeSep 5th 2012

    I don’t think that all discussions should be linked from the page. Often, a discussion reaches some definite conclusion, which can then be incorporated into the page in a way that a future reader can obtain exactly the same information as the discussion would have provided, more easily and with less effort. However, when a discussion is not about some mathematical point and/or doesn’t reach a definite conclusion, then I think it may be valuable for a reader to be pointed to it. Probably these particular discussions are in the latter category.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 5th 2012
    • (edited Sep 5th 2012)

    I am thinking two things:

    1. the nForum is to the nLab as what the talk-pages are on Wikipedia. On Wikipedia you’d be irritated if the Literature-section pointed you to the page’s talk-page! You want the literature section to point you to stable, relevant information.

    2. The number of seconds it takes to choose one point of that old discusison and turn it into a short useful paragraph on the entry is comparable to the seconds it takes to link to that discussion here and then discuss that move. But the former seconds would be better invested! ;-)

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 5th 2012

    Urs, with regard to point 1, my own thinking is that we should not be comparing the nLab to WP. This is not only with regard to NPOV/nPOV, but also in the idea of this being a public Lab book where we record our notes and sometimes rough thoughts (although if we are moved to work on polishing and making things look more like an encyclopedia, that can be fine as well).

    Please reread the first standout box on the Home Page!

    I agree with Mike that we need not indiscriminately link to every old discussion, especially those that seem like a beginner is floundering around, but more substantive discussions which did not reach a firm conclusion can be linked to in an unobtrusive way (with a flag which indicates tentativeness of the discussion, if need be). This is desirable in view of the avowed value such discussions have for researchers like Zoran.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeSep 5th 2012
    • (edited Sep 5th 2012)

    What is the value of the discussion in this case? If it is valuable, why does nobody extract the punchline?

    I think, instead, the discussion above is not valuable. I think it is confused and uninformed. Back when we had that discussion, we were all lacking the crucial insights needed to anwer that question with which I started the discussion.

    I already found it embarrassing to copy that old discussion over to here. I did this only to stick to the rules. I would just entirely delete that old discussion, if I felt it was socially acceptable.

    These questions: “what is the right foundation for directed homotopy theory?”, we have discussed in an informed and actually useful way elsewhere.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeSep 5th 2012

    The value of the discussion in this case lies in the discussion itself. There is not, as far as I can see, a “punchline” which can be “extracted” from it.

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 5th 2012

    Urs, as far as I can tell, there are several query boxes you removed. The first one, where you asked the question about nn-categories, got a very brief reply from Toby. I have no issue with not linking to that.

    The second was also started by you, but it seems to have to do with Lawvere’s ETCC. There the discussion does not seem confused and uninformed (strong words!) – at least participants like Toby and Mike seem not to be uninformed. How important the discussion is, that’s something we each have to decide individually, but it was probably written close to around the same time as a long discussion at the Cafe which involved Arnold Neumaier, which was of some significance I believe, and it might be useful as a way of jogging memories for people like Zoran.

    The third was a discussion about ’categorial’ vs. ’categorical’, which I personally find tiresome and not very interesting. I personally wouldn’t care if that wasn’t linked back to.

    But I think the real issue is this:

    If it is valuable, why does nobody extract the punchline?

    Well, because for one we’re busy and maybe don’t feel like dropping other work to extract punchlines! Until such time as we’re ready to break all links to an earlier discussion which may yet contain food for thought for some, why do you so strenuously object to a little unobtrusive link??

    I have to go now, and not sure how much time I want to argue about this…

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeSep 5th 2012

    The third was a discussion about ’categorial’ vs. ’categorical’, which I personally find tiresome and not very interesting.

    Regardless of how tiresome it is, I think there is some use in keeping it around in case someone new comes along and wants to have the same discussion. That way they can read the old discussion first and hopefully feel as though everything they wanted to say was already brought up and doesn’t need to be said again.

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 5th 2012

    @Mike #15: sure, I can see that (and wouldn’t object to a link!). And I mean no disrespect who find the topic to be of interest.

    • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeSep 6th 2012

    I’m inclined to say that a link is warranted iff somebody thinks that a link is warranted. If Urs doubted that anybody would find the link useful, then I don’t blame him for leaving it out. If Zoran wants the link only as a matter of principle, then I wouldn’t put it in. But if Zoran (or anybody else) finds the link useful, then it should stay.

    • CommentRowNumber18.
    • CommentAuthorzskoda
    • CommentTimeSep 6th 2012
    • (edited Sep 6th 2012)

    I clearly stated in post 3 “unless they are extremely obsolete or nonsubstantial” in accordance with 17. Hence I never meant that every query which is archived should be linked and I even think that they are such rare queries which do not even warrant nnForum archiving. Here I thought that it is substantial because it has a discussion of EETC and alike, which I have no time to comprehend at the moment but would like to relate to when in this subject next time. I also do not feel particularly strong about how to handle this or that particular entry.

    • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeSep 7th 2012

    Here I thought that it is substantial because it has a discussion of EETC and alike, which I have no time to comprehend at the moment but would like to relate to when in this subject next time.

    So this meets the requirement in my

    if Zoran (or anybody else) finds the link useful, then it should stay.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeAug 4th 2020
    • (edited Aug 4th 2020)

    Added pointer to univalent foundations for mathematics under “Related concepts”. But this entry should really have a (small, at least) subsection on that topic.

    diff, v93, current

  21. added section on deductive systems used in the foundations of mathematics

    Anonymous

    diff, v97, current

    • CommentRowNumber22.
    • CommentAuthorGuest
    • CommentTimeNov 18th 2022

    I plan on broadening the scope of this article to talk about foundations of mathematics in general. This includes not only approaches such as ETCS which are based in category theory, but also traditional material set theories such as ZFC and Mostowski set theory, and dependent type theories like Martin-Löf type theory which do not have a separate notion of proposition from sets or types. Important concepts that should be added to this article include descriptions of the foundational notions of collection and object, the notion of membership/typing, the notion of equality of objects and equality and equivalence of collections, the notion of definition, and the basic metatheoretical foundations and deductive systems on which each foundations of mathematics are based in (natural deduction, sequent calculus, lambda-calculus, et cetera).

  23. adding section on universes, classes, and size issues

    Anonymous

    diff, v100, current

    • CommentRowNumber24.
    • CommentAuthorGuest
    • CommentTimeNov 19th 2022

    When I try to add a∈Aa \in A to the article, I get the following message:

    No mapping available for Tex symbol: in

    I don’t seem to have any issues on any other article, just this article.

  25. updating old link

    http://nforum.mathforge.org/discussion/4172/foundation-of-mathematics/?Focus=33992#Comment_33992

    to

    http://nforum.ncatlab.org/discussion/4172/foundation-of-mathematics/?Focus=33992#Comment_33992

    Anonymous

    diff, v102, current

  26. moved material about category theory and foundations over to its own page at category theory and foundations.

    Anonymous

    diff, v102, current

  27. added reference

    Anonymous

    diff, v103, current

  28. Adding reference:

    • Penelope Maddy, What Do We Want a Foundation to Do? Comparing Set-Theoretic, Category-Theoretic, and Univalent Approaches, In: Stefania Centrone, Deborah Kant, Deniz Sarikaya (editors), Reflections on the Foundations of Mathematics. Synthese Library, vol 407. Springer, Cham. 12 November 2019. (ISBN:978-3-030-15654-1, doi:10.1007/978-3-030-15655-8_13, pdf)

    Anonymouse

    diff, v106, current

  29. Replaced Penelope Maddy chapter reference with full book reference since the entire book is relevant to the foundations of mathematics:

    • Stefania Centrone, Deborah Kant, Deniz Sarikaya (editors), Reflections on the Foundations of Mathematics. Synthese Library, vol 407. Springer, Cham. 12 November 2019. (ISBN:978-3-030-15654-1, doi:10.1007/978-3-030-15655-8)

    Anonymouse

    diff, v107, current

1 to 29 of 29

  1.