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 21st 2012

    I have reorganised set theory and spun off material set theory.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeJul 21st 2012

    (Between the two pages, nothing has been removed.)

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeJul 21st 2012

    I’ve now removed stale discussions from material set theory. One may view them at the original version.

    • CommentRowNumber4.
    • CommentAuthorRodMcGuire
    • CommentTimeJul 21st 2012

    As someone who still thinks often in material set theory I sometimes get confused about when I need to index. I think it would be worthwhile to add the below paragraph to set theory to mention indexing and give an example of the undefined notion of “type casting”. I am asking rather than doing because while I think this is the best top level place to introduce this I’m not sure, I may be wrong, or there is a better way to introduce the issues.

    Anyway, after the paragraph:

    A structural set theory, on the other hand, looks more like type theory. Here, the elements of a set have no existence or structure apart from their identity as elements of that set. In particular, they are not themselves sets, and cannot be elements of any other set, at least not without invoking some explicit type-casting operator. Similarly, elements of different sets cannot be compared (by default).

    Add the paragraph:

    One basic casting mechanism is the notion of “indexed set” which is just a function between two sets. Elements aa in AA and bb in BB might be considered the same if indexes map both to an element cc in CC. This is how the notion of subsets and their sharing of common elements can be defined by inclusion functions. Conversely if the indexes are from CC to AA and BB and map cc to aa and bb then aa and bb might be considered the same.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeJul 21st 2012

    I added something shorter right after the clause that refers to type casting. But you could add more if you like. What you say is correct, except that I would leave out the last sentence; while that does allow aa and bb to be considered the same in a way, it’s not an equivalence relation.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJul 23rd 2012

    Thanks Toby! We’ve needed this for a while.

    I wouldn’t refer to a cospan as a type-casting, but rather as two type-castings – I edited the page to clarify this. I don’t think that that bullet point is the right place for a more detailed discussion of type-casting; what we want there is a very concise overview of the differences. If we want to discuss type-casting in more detail, then maybe a section at structural set theory would be a good idea. Feel free to make one!

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeJul 23rd 2012

    Yes, technically an arbitrary cospan is two type castings, but that’s only because the default meaning of ‘type casting’ is the simplified case of a cospan where one leg is an identity. But the purpose of type casting to compare items is met in general with a cospan. I’ll change ‘would’ to ‘could’ and become happy.

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 31st 2017

    I’ve wasted at least half an hour trying to find the right discussion thread to place this, so now screw it.

    There’s a MathOverflow question which could reasonably be directed to Mike, although I’m adding a preliminary comment.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJan 31st 2017

    Thanks Todd!

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 21st 2017

    Mostly heat being generated at Hamkins’ g+ discussion of material set theory, but maybe we’ll need to adjust something here when the dust settles. Are the concerns not largely a distraction from what I sense really worries some set theorists, namely, that not everyone agrees with:

    It is a huge and vibrant field, with hundreds of active researchers and many exciting developments, some deeply connected with other parts of mathematics.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeFeb 21st 2017
    • (edited Feb 21st 2017)

    I expect that instead of the discussion of philosophical sentiments, which is unlikely to be fruitful, there is a precise formal point here which could be and should be stated as a theorem on which then everybody may agree, irrespective of personal philosophies.

    Namely the real point of the “structuralists” is that in some sense, which I bet could easily be made precise, structural set theory is “more fundamental” than material set theory, in the fairly evident sense that one gets from structural to material by adding axioms, and from material to structural by removing axioms (or by “forgetting” structures, as Mike says in the comments).

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 21st 2017

    I certainly don’t disagree with the statement quoted in #10. And I wouldn’t say that structural set theory is more fundamental than material set theory either. I just want terminology to distinguish them.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeFeb 21st 2017

    I wouldn’t say that structural set theory is more fundamental than material set theory

    Is it just the word “fundamental? Choose a different word. Besides terminology, there must be a precise sense in which material set theory is obtained from structural set theory by adding axioms/rules. No?

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 21st 2017

    It's not so much adding axioms/rules as adding to the language, specifically by adding the universal membership relation \in. Then you naturally add some axioms to go with it. (Thus, we're adding structure, not just properties.)

    But what makes material set theory elegant is that this one new added structure is now the only structure that you need! Everything else can be defined in terms of it. (And it's not like we added axioms to ensure this; the extra axioms are almost entirely written in terms of \in only.)

    Structural set theory is elegant too, of course, but in an entirely different way. Since \in need never be referred to directly in ordinary mathematics, structural set theory is the precise structure needed for mathematical foundations.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeFeb 21st 2017
    • (edited Feb 21st 2017)

    Okay, sure, not just axioms, but language. Whatever it is, I feel that logicians ought to be able to make a formal uncontroversial statement about how the two flavors of set theories relate, instead of having fruitless philosophical discussions about them.

    Recall the recent discussion with Richard Williamson, where various regulars here felt there was too much informal chat and too little precise formalized statements. Now with these fights over material and structural set theory it*s rather similar, and ought to be improved on.

    In pure philosophy there are many fights among practitioners, namely whenever it is impossible to find unambiguous agreement. In mathematics it should be different. It ought not to be the case that a top level logician feels that the distinction between material set theory and structural set theory is a cause for lengthy informal debate. There ought to be a precise theorem that completely clarifies how they are related, and that’s it then.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 21st 2017

    There are formal uncontroversial statements about how they relate, like in https://arxiv.org/abs/1004.3802. The philosophical questions don’t turn on that.

    • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 21st 2017

    The G+ discussion is already moving from philosophical chitchat to precise statements.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeFeb 21st 2017
    • (edited Feb 21st 2017)

    There are formal uncontroversial statements about how they relate, like in https://arxiv.org/abs/1004.3802.

    Thanks for reminding me. Re-reading the introduction, it sounds as if there is an axiom to be added to go from structural to material set theory: your “autology” axiom.

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 22nd 2017

    Autology strengthens the theory of an elementary topos to make it equiconsistent with strong axioms of material set theory such as replacement or collection. But the formal relationship between the theories is the same as it is for weaker theories, namely from each of them you can construct a model of the other. In no case can you simply add an axiom to one theory to get the other.

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 22nd 2017

    We claim that there is some kind of idempotent material-structural adjunction which establishes equiconsistency.

    As to why Hamkins might have the impression that those on the structural side believe in the superiority of their approach, perhaps the feelings behind comments like the following at structural set theory have something to do with it:

    Structural set theory provides a foundation for mathematics which is free of this “superfluous baggage” attendant on theories such as ZF

    Sounds like a value judgement to me.

    As for the value of current (material) set theory (#10), one question you can pose is where you think the future legendary moments of the story of mathematics are currently likely being worked out. We have enough advantage of hindsight to believe that what Gauss did with number theory, Galois did with equations, Riemann did to space, etc. were seminal moments. Some set theory up to Cohen and the independence of CH will likely count as seminal too from the 20th century, but how much of the past, say, 30 years?

    To return to safer waters, some of the buzz in current material set theory is provided by Hamkins’ geology. So a couple of questions:

    1. Is there anything to stop structural set theory doing similar work, or does the ’materiality’ matter?
    2. Could there be anything comparable to consider for a ’\infty-groupoid theory’? Is it possible to have a ’material \infty-groupoid theory’?
    • CommentRowNumber21.
    • CommentAuthorDavidRoberts
    • CommentTimeFeb 22nd 2017

    The big difference between material and structural set theories as far as results go is that there doesn’t seem to be an inner model theory for structural sets, say in ETCS. How could we define the analogue of L, for instance? It’s not an internal/small category, so perhaps something fibred over the base category of sets, but I have no good ideas.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 22nd 2017

    Personally, I’m not all that interested in structural set theory any more now that I’ve been converted to type theory. Of course, one big reason for that is HoTT. In particular, the answer to question 2 is probably no: I’ve never been able to imagine quite what a “material \infty-groupoid theory” would look like.

    It might be worth softening those value judgments at structural set theory.

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 22nd 2017

    Or at least cite pros as well as cons. For example, one use of material sets is the notion of rank, which occurs in technical tricks like Scott’s trick. (And of course David already mentioned things like inner models and the constructive universe, whose structural analogueso I have little idea about.)

    • CommentRowNumber24.
    • CommentAuthorRichard Williamson
    • CommentTimeFeb 22nd 2017
    • (edited Feb 22nd 2017)

    Recall the recent discussion with Richard Williamson, where various regulars here felt there was too much informal chat and too little precise formalized statements. Now with these fights over material and structural set theory it*s rather similar, and ought to be improved on.

    In pure philosophy there are many fights among practitioners, namely whenever it is impossible to find unambiguous agreement. In mathematics it should be different. It ought not to be the case that a top level logician feels that the distinction between material set theory and structural set theory is a cause for lengthy informal debate. There ought to be a precise theorem that completely clarifies how they are related, and that’s it then.

    Hi Urs, this is your point of view, it is not a universal truth. You have a nice formal box in which it appears you’d like to fit everything in mathematics, physics, philosophy, etc, into. That is fine, and it is a worthy endeavour. But as much as you may feel a sense of frustration in seeing discussion outside of your box, so others may feel that this box is a bit too narrow or unnatural to immediately try to squeeze everything into it. There are many worthy endeavours.

    All of the participants in the discussion you referred are perfectly able to write formal mathematics, and perfectly competent in so doing. If some of us chose to engage in a philosophical discussion, we did so presumably because we felt there might be something interesting to be had in trying to understand one another. There was plenty of mathematics in the discussion. I made clear several times that I had no intention of launching any kind of philosophical discussion or of providing a clear presentation of my philosophical views, and tried to withdraw several times; again, we must presume that the other participants felt there might be something to be gained from engaging in further discussion.

    So by all means pursue fitting everything into your box, but do try to avoid pejorative language such as ’too much’, ’too little’, and ’ought to be improved on’. The formalism which you advocate is essentially an orthodoxy, and it is a typical reaction of orthodoxy to dismiss ideas which might not (yet at least) be able to be expressed and hence understood well within it. This does not necessarily mean that consideration of those ideas is worthless. The reception of many to Brouwer’s ideas in his time, which are a principal root of the formalism you now espouse, would be a classic example.

    • CommentRowNumber25.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 23rd 2017

    Re #15, I was put in mind of the Vienna Circle’s manifesto - WISSENSCHAFTLICHE WELTAUFFASSUNG: DER WIENER KREIS, (The Scientific Conception of the World: The Vienna Circle):

    The scientific world conception is characterised not so much by theses of its own, but rather by its basic attitude, its points of view and direction of research. The goal ahead is unified science. The endeavour is to link and harmonise the achievements of individual investigators in their various fields of science. From this aim follows the emphasis on collective efforts, and also the emphasis on what can be grasped intersubjectively; from this springs the search for a neutral system of formulae, for a symbolism freed from the slag of historical languages; and also the search for a total system of concepts. Neatness and clarity are striven for, and dark distances and unfathomable depths rejected. In science there are no ‘depths’; there is surface everywhere: all experience forms a complex network, which cannot always be surveyed and, can often be grasped only in parts. Everything is accessible to man; and man is the measure of all things. …The scientific world-conception knows no unsolvable riddle. Clarification of the traditional philosophical problems leads us partly to unmask them as pseudo-problems, and partly to transform them into empirical problems and thereby subject them to the judgment of experimental science. The task of philosophical work lies in this clarification of problems and assertions, not in the propounding of special ‘philosophical’ pronouncements. The method of this clarification is that of logical analysis; of it, Russell says (Our Knowledge of the External World, p. 4) that it “has gradually crept into philosophy through the critical scrutiny of mathematics… It represents, I believe, the same kind of advance as was introduced into physics by Galileo: the substitution of piecemeal, detailed and verifiable results for large untested generalities recommended only by a certain appeal to imagination.”

    and

    …this much is certain: there is no such thing as philosophy as a basic or universal science alongside or above the various fields of the one empirical science; there is no way to genuine knowledge other than the way of experience; there is no realm of ideas that stands over or beyond experience. Nevertheless the work of ‘philosophic’ or ‘foundational’ investigations remains important in accord with the scientific world-conception. For the logical clarification of scientific concepts, statements and methods liberates one from inhibiting prejudices. Logical and epistemological analysis does not wish to set barriers to scientific enquiry; on the contrary, analysis provides science with as complete a range of formal possibilities as is possible, from which to select what best fits each empirical finding (example: non-Euclidean geometries and the theory of relativity).

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeFeb 23rd 2017
    • (edited Feb 23rd 2017)

    David wrote in #20:

    perhaps the feelings behind comments like the following at structural set theory have something to do with it:

    Structural set theory provides a foundation for mathematics which is free of this “superfluous baggage” attendant on theories such as ZF

    Sounds like a value judgement to me.

    Mike wrote in #22:

    It might be worth softening those value judgments at structural set theory.

    It would be more worthwhile not to have value judgements at all, soft or not, but to replace them with precise facts. There is a good reason to say that material sets is like structural sets “with something extra”, which is why you added this in revision 8, and hence there should be a way to state this as a precise undisputable fact. I am not surprised that my feeble attempts at guessing how to say this are easily shot down, but I would hope that for logic/foundations experts this would be easy to do. It would be worthwhile!

    • CommentRowNumber27.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 23rd 2017
    • (edited Feb 23rd 2017)

    Isn’t whatever is being claimed at material-structural adjunction a good place to start? I provided the link there to Mitchell’s article. It’s hard for me to extract from that article the background to what the page is claiming. Was this supposed adjunction written up somewhere else? Nobody but ourselves seems to refer to it as ’material-structural adjunction’.

    • CommentRowNumber28.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 23rd 2017

    It would be more worthwhile not to have value judgements at all

    If the mood is to go all Wiener Kreis, one is still allowed to express judgments as to the pragmatic features of different systems, whether one system is more convenient than another, etc. So saying that a feature is superfluous to the function of the system is fine.

    Re “Brouwer’s ideas in his time” (#24), carrying on with the Manifesto, there is:

    Certain difficulties …remained in this attempt at overcoming the foundation crisis of arithmetic (and set theory) and have so far not found a definitively satisfactory solution. At present three different views confront each other in this field; besides the ‘logicism’ of Russell and Whitehead, there is Hilbert’s ‘formalism’ which regards arithmetic as a playing with formulae according to certain rules, and Brouwer’s ‘intuitionism’ according to which arithmetic knowledge rests on a not further reducible intuition of duality and unity [Zwei-einheit]. The debates are followed with great interest in the Vienna Circle. Where the decision will lead in the end cannot yet be foreseen; in any case, it will also imply a decision about the structure of logic; hence the importance of this problem for the scientific world-conception. Some hold that the three views are not so far apart as it seems. They surmise that essential features of all three will come closer in the course of future development and probably, using the far-reaching ideas of Wittgenstein, will be united in the ultimate solution.

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeFeb 23rd 2017
    • (edited Feb 23rd 2017)

    Isn’t whatever is being claimed at material-structural adjunction a good place to start?

    Thanks, yes, that looks good. Sorry for not catching this when you first said it in #20.

    If the mood is to go all Wiener Kreis

    Wait, what I am asking for is not something fancy, but something that we usually all agree on: For example we don’t say that a discrete group is a Lie group without the extra baggage of a smooth structure, we don’t even say this in a softened form which would be more polite to the supporters of Lie groups. Instead we explain that one may add this extra structure, and what it is used for. That’s just mathematics. Should be the same for set theories.

    • CommentRowNumber30.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 23rd 2017

    Yes, but those kinds of groups clearly have different roles. As soon as we have alternative systems most of whose purposes overlap, there will be issues concerning the relative importance of any purpose, how well (or naturally) a role is carried out, etc.

    What is expressed with the ’excess baggage’ comment is the judgement that the membership-relation incurs many inconvenient costs and little or no benefit. Now perhaps the membership set theorists think that there are benefits (maybe that you can do that set theoretic geology (#20)). Since we don’t want to multiply systems for their own sake, there is pressure not to expand unnecessarily. It is even of practical value not to have people too dispersed over different systems. (Carnap was a fan of Esperanto, incidently.)

    There was something of this kind of debate in the early days of groupoids. Were they worth adding to the repertoire if we already have groups (chap 9 of my book covers that)?

    However calmly statements are made about System X doing A and B, and System Y doing A as well, not B, but also C and D, you can be sure the emotions will be running along somewhere. One’s personal commitment to research projects relies on this (see Polanyi).

    • CommentRowNumber31.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 23rd 2017

    It might be worth softening those value judgments at structural set theory.

    In the nLab, we have the nn-point of view, and I think that there is no doubt from that perspective that structural set theory is better than material set theory as a foundation of mathematics. It is certainly interesting that all of mathematics can be encoded within the sparse language of material set theory, and even useful for some things (such as constructing models like LL), much as it is also interesting and useful that logic can be encoded within the language of arithmetic (Gödel numbering). But just as I wouldn't want to write my logic directly in arithmetic, so I also wouldn't want to write my mathematics directly in material set theory. I write it in structural set theory, and ignore the material set theory that could be taken to underly it. (For example, I write (a,b)(a,b) instead of {{a},{a,b}}\{\{a\}, \{a, b\}\}, and that is just the beginning. Of course, material set theorists do the same, defining the former to mean the latter, but this is just encoding structural set theory into material set theory.)

    None of this is to say that ‘material set theory’ is a pejorative term. It was apparently invented independently by a material set theorist and by a type theorist (or whatever Steve Awodey was then), and is suitable for neutral discussion. But we can still have opinions about it.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 23rd 2017

    While I’ve in the past made the “excess baggage” argument, I don’t any more think that it is a very good one. Any foundational system will always include stuff and details that are irrelevant to mathematics. Whether or not (a,b)(a,b) is defined as {{a},{a,b}}\{\{a\},\{a,b\}\} is an irrelevant detail; even in structural set theory there are many other places where we define things in a particular way and then forget about the details of the definition, so I don’t see how the fact that we do this for ordered pairs in material set theory is any substantial disadvantage. In certain ways, structural set theory certainly matches mathematical practice (at least, my mathematical practice) better than material set theory does — that is, I never use a global membership relation, and everything I do is isomorphism-invariant. But in other ways, material set theory matches my practice better — for instance, I talk about subsets UXU\subseteq X rather than injective functions, and use the same notation xUx\in U for an element of the subset and xXx\in X an element of the superset. (Unless I’m explicitly working in a different system like HoTT, of course.)

    More to the point, I think — and more worth mentioning as the nnPOV — are the mathematical advantages of structural set theory and type theory to a higher category theorist, such as:

    1. Structural set theory and type theory can be internalized in any topos. Material set theory can only be internalized by means of interpreting it into structural set theory or type theory, and in general the result fails to “see” the entire topos (at least, without going through substantial contortions).

    2. Type theory, at least, and perhaps structural set theory, can be generalized to a theory like HoTT whose basic objects are higher-categorical. No one, to my knowledge, has ever proposed such a generalization of material set theory.

    • CommentRowNumber33.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 24th 2017
    • (edited Feb 24th 2017)

    And all this is written out in that great post of yours, Mike, which could be brought over to the nLab. The relevant pages structural set theory, material set theory, etc should point this other option.

    So I’m left with the question of what it is that makes the traditional set theorist tick. It can’t be to do with looking for a language that better serves the working mathematician. Surely what set theory could contribute there has long been achieved. Given that set geology is well-received, it must be that kind of exploration of the set multiverse that’s attractive. So to a n-POV, HoTT exponent is there anything valuable being found in set geology, and if there is, is it something that would be very difficult to reach from HoTT tools?

    In #12 you were agreeing to set theory being a vibrant field where exciting discoveries are being made. What are these?

    [Or is there a constructivist dodge where “I don’t disagree…” means something different from “I agree…”?]

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 24th 2017

    One slick way to say describe material set theory from a structural standpoint is that it is the study of the initial ZF-algebra. A ZF-algebra is a (large) partial order with all small suprema equipped with an endomorphism called “singleton”. This was the starting point of Joyal-Moerdijk’s original “algebraic set theory”. Studying the initial algebra of a given sort is a perfectly respectable thing to do (e.g. “number theory” is the study of the initial “Lawvere algebra”, i.e. a set equipped with a chosen element and an endomorphism called “successor”). Moreover, I think it’s not surprising even a priori that the structure of the initial ZF-algebra is very rich and tells us a lot about the boundary between small and large, and I think any interesting part of material set theory should be doable in a structural theory by studying the initial ZF-algebra.

    I am not a material set theorist, and I don’t follow its developments very closely. In particular, I don’t really have much understanding of “geology”. But in general I see no reason to doubt what material set theorists say about their own subject, any more than I doubt what other mathematicians say about their own subjects, except if what they say happens to contradict something I do know something about (such as if they say “ZFC is the foundation of mathematics”, or if they spend their time wondering whether the Continuum Hypothesis is “true”).

    • CommentRowNumber35.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 24th 2017

    I guess the days of the grandees of mathematics openly steering people away from one branch to another are over. Someone told me how in the 70s Atiyah would steer people away from point-set topology to algebraic topology since he viewed the latter as more important for the life of mathematics. Perhaps better to rely on the invisible hand than the Five-year plan.

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 24th 2017

    I would like to think so, but I wouldn’t be surprised if there are still “grandees” who behave like that. For instance, I expect some of the more vocal ZFC-ists would steer people away from HoTT if they had the chance.

    • CommentRowNumber37.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 24th 2017

    Are Harvey Friedman and Stephen Simpson at FOM behaving like that? They have in the past.

    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeFeb 24th 2017

    And Michael Harris, on his unapologetic blog.

    • CommentRowNumber39.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 24th 2017
    • (edited Feb 26th 2017)

    Any foundational system will always include stuff and details that are irrelevant to mathematics.

    Yes, but that material set theory requires more of this than structural set theory is telling us something. When we use sets in mathematical practice, we deal with elements, subsets, functions, and relations pretty directly, and structural set theories tend to either have these as primitive notions or treat them with minimal encoding. Although less common, I like to deal with disjoint unions and quotient sets equally directly, even though common structural foundations (such as ETCS, SEAR, and the imprecisely defined naive set theory of the ordinary mathematician) require encoding for those. But material set theory, being a theory of a global membership relation and nothing else, requires a great deal more encoding to capture all of this. In some respects, we are just lucky that ZFC is sufficient to encode structural set theory; the similarly motivated (and even simpler) material set theory NF, for example, is not.

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2017

    It tells us something, but I’m not sure that it tells us that structural set theory is “better” as a foundation for mathematics. Once that encoding has been done (and it’s not really that much encoding, relatively speaking), is there any real disadvantage to the fact that we had to do it?

    • CommentRowNumber41.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 26th 2017

    in mathematical practice, we deal with elements, subsets, functions, and relations pretty directly, and material [my emphasis] set theories tend to either have these as primitive notions or treat them with minimal encoding.

    Toby, did you mean to say “structural” there?

    I assume so, and it seems to be the main point. Recall that Lawvere introduced ETCS for pedagogical purposes, when he was teaching an undergraduate course: it connects directly with practice.

    And by golly, I think structural set theory does promote a right set of values for modern practice (invariance with respect to isomorphism), that even very fine mathematicians occasionally forget when they think in terms of a membership-based set theory with an extensionality axiom. I’ll give two examples. The first is quoting Lawvere (the full quote can be found here:

    The possibility of rejecting the rigid epsilon chains as a ‘foundation’ for mathematics occurred to many around 1960. But for me the necessity for doing so became clear at a 1963 debate between Montague and Scott. Each had tried hard to find the right combination of tricks which would permit a correct definition of the fundamental concept of a model of a higher-order theory (such as topological algebra). Each found in turn that his proposal was refuted by the other’s counter example (involving of course unforeseen ambiguities between the given theory and global epsilon in the recipient set theory).

    The whole difficulty Montague and Scott were having seemed in utter contrast with what I had learned about the use of mathematical English and what we try to make clear to students: in a given mathematical discussion there is no structure nor theorem except those which follow from what we explicitly give at the outset. Only in this way can we accurately express our knowledge of real situations. A foundation for mathematics should allow a general definition of model for higher-order theories which would permit that crucial feature of mathematical English to flourish, confusing matters as little as possible with its own contaminants. We are constantly passing from one mathematical discussion to another, introducing or discharging given structures and assumptions, and that too needs to be made flexibly explicit by a foundation.

    Now of course I have no idea what specifically transpired in the debate, but if difficulties of that sort exist for professional logicians, then that too is telling. (Again Lawvere brings the discussion back to practical usage and to students.)

    The second example comes from a brief MO comment thread, where one participant (with a solid reputation) says, “But the point is that there is no universally agreed upon definition of what the “disjoint union” of two nondisjoint sets is. Or is there? (I suppose if you forced me to give one, I would put AB=A×{0}B×{1}A \coprod B = A \times \{0\} \cup B \times \{1\}, but surely not everyone agrees with this?)”.” I can’t think of a realistic scenario where that should be the point, but the reflex to pin down a notion or structure up to equality does seem to be a long-ingrained habit that I think is further promoted by working with membership-based frameworks where equality of sets is absolute (not contextual).

    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2017

    There’s some sense to that. But I still can’t imagine trying to teach ETCS to undergraduates. Maybe I’m an old hidebound fuddy-duddy, but I can’t imagine anyone really understanding the idea that “mathematics should be invariant with respect to isomorphism” until after learning some abstract algebra or point-set topology or some kind of abstract mathematics where you get to work with isomorphisms, whereas students need some kind of understand of what a “set” is before they can learn such a subject in the first place.

    • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2017

    (Also, I’m amused that your comment on that MO thread has more upvotes than the answer itself.)

    • CommentRowNumber44.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 27th 2017

    So I think Lawvere’s instructions (as a young instructor at Reed College circa 1964) were to teach a year-long foundationally-oriented course building to the basic theory of real analysis, meaning that it was to introduce students to some set theory before starting in on analysis proper. Apparently Reed had a departmental tradition of emphasizing “foundations”. Naturally I don’t know how successful Lawvere’s experiment was, although I think in his ETCS paper, he says it was.

    But yeah, circumstances in which one would teach ETCS per se to undergraduates might be a tad unusual. Even in the best universities, it would be somewhat unusual to have students lining up to learn ETCS (when so much else is on offer). But I could see doing it as an independent study.

    All that said, I do think it’s viable to promote a structuralist spirit in an introductory courses in modern mathematics (abstract algebra, topology, real analysis) where sets are treated as bags of dots with names, and universal mapping properties are introduced although not necessarily by that name. Certainly I tried that type of thing when I was teaching; I figured that sooner or later they’re going to have to learn this if they want to pursue mathematics. Mostly though it was not formal, more like on-the-job training with the idea it eventually it seeps in with enough gentle repetition.

    I don’t see comparable advantages to teaching sets in terms of a cumulative hierarchy conception, unless it was to prepare students who wanted to go into set theory as mathematicians (and who should therefore learn the traditional points of view).

    • CommentRowNumber45.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 27th 2017

    When I was a graduate student, I taught a discrete mathematics course in the summers, and this included an introduction to set theory. There was no formal axiomatization, but I taught the set theory structurally.

    For example, I said that you should only consider ABA \cup B or ABA \cap B when AA and BB are given as subsets of an ambient set XX. Otherwise, the concept may appear meaningful, but the apparent result may depend on arbitrary coincidences of notation. Relatedly, I introduced the disjoint union as a basic operation on sets, on a par with the Cartesian product. The course also included some combinatorics, and I taught |AB|=|A|+|B|{|A \uplus B|} = {|A|} + {|B|} as the basic sum rule for cardinality of (finite) sets, on a par with |A×B|=|A||B|{|A \times B|} = {|A|} \,{|B|} as the product. That |AB|=|A|+|B|{|A \cup B|} = {|A|} + {|B|} when AA and BB are disjoint subsets of some ambient set is just a corollary.

    And related to the disjoint union, I taught quotient sets as a fundamental concept too. Given a set XX and an equivalence relation RR, there is a set X/RX/R, called the quotient of XX modulo RR such that:

    • an element of X/RX/R has the form [a] R[a]_R, called the equivalence class of aa modulo RR, for some element aa of XX;
    • [a] R=[b] R[a]_R = [b]_R (in X/RX/R) if and only if RR holds of aa and bb.

    (This specifies a set by explaining what form its elements take and when two of these elements are equal, which I got straight out of Bishop's Constructive Analysis.) As a side note, I explained the terminology ‘equivalence class’:

    • given aa in XX, the equivalence set of aa modulo RR is the subset of XX consisting of those bb in XX such that RR holds of aa and bb;
    • ‘class’ is an archaic synonym for ‘set’ or ‘subset’ (that now has another meaning, related but somewhat technical);
    • if you identify the equivalence class of aa (the axiomatic [a] R[a]_R) with the equivalence set of aa (the subset of XX, or element of the power set of XX), then the set of equivalence sets modulo RR has the defining properties of X/RX/R.

    But you do not normally think about these equivalence sets when working with the quotient set.

    I never used the word ‘isomorphism’, at least not precisely. But we had ‘bijection’, and I emphasized that a bijection between two sets allows us to use either for the purposes of the other. So for example, if you have a set PP of people and you wish to record some information about them, then you might want to use a bijection between PP and {1,2,,n}\{1, 2, \ldots, n\} (or {0,1,,n1}\{0, 1, \ldots, n - 1\}, since the students were mostly CS majors) for some natural number nn, then refer to each person by the corresponding number. This well-known idea illustrates the power of isomorphism.

    • CommentRowNumber46.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 27th 2017

    Toby, how did you define “subset”? That’s one area where I feel like material set theory has the pedagogical advantage: it’s much easier to think about a set all of whose elements are also elements of AA than about an injective function. Generally when I teach this kind of course I want to introduce subsets before having talked about functions at all.

    Also, after conversations with others who teach this course, I’ve also partially come around to the idea that there is some value in defining a function as a total functional relation. Yes, it’s difficult at first, but that very difficulty forces students to come to grips with the idea that a function can be absolutely anything satisfying the definition, whether or not it is defined by an equation like most of the functions they’ve ever encountered before.

    • CommentRowNumber47.
    • CommentAuthorNikolajK
    • CommentTimeFeb 28th 2017
    • (edited Feb 28th 2017)

    Yes, it’s difficult at first, but that very difficulty forces students to come to grips with the idea that a function can be absolutely anything satisfying the definition, whether or not it is defined by an equation like most of the functions they’ve ever encountered before.

    Given that they probably know piecewise definitions already, an explicit list of equations like

    f(a) = u

    f(b) = v

    f(c) = w

    corresponds to that set of pairs and should make it clear that it can be “anything” as well.

    • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 28th 2017

    Well, perhaps, if you allow a “list” to be uncountable…

    • CommentRowNumber49.
    • CommentAuthorTobyBartels
    • CommentTimeMar 3rd 2017
    • (edited Mar 3rd 2017)

    @Mike #46:

    I defined ‘subset’ in much the same way as I defined ‘quotient set’ in comment #45. (Nothing about surjective functions there, either.) Say what the elements are and when they are equal.

    The week on set theory came right after a week on first-order logic. So even when you see ‘[binary] relation [on XX]’ in #45, you should be thinking ‹22-place predicate about elements of XX that respects equality in XX›. So given a set XX and a 11-place predicate PP about elements of XX that respects equality in XX, you get a subset {xX|P[x]}\{x \in X \;|\; P[x] \}, such that:

    • an element of {xX|P[x]}\{x \in X \;|\; P[x] \} is an element aa of XX such that P[a]P[a] is true;
    • assuming that P[a]P[a] and P[b]P[b] are both true, a=ba = b in {xX|P[x]}\{x \in X \;|\; P[x] \} if and only if a=ba = b in XX.

    (The latter fact justifies the abuse of notation that the same symbol is used for aa as an element of {xX|P[x]}\{x \in X \;|\; P[x] \} as is used for aa as an element of XX.)

    I don't think that I ever wrote any of this down, by the way. (And if I did, then it was ephemeral writing on a baord; I'm certainly not copying this stuff out of lecture notes. I'm dredging up 10-year-old memories of how I thought about things back then and what I was trying to explain.) But I'm pretty sure that I said all of this. For practical purposes, the students got the idea from examples.

    • CommentRowNumber50.
    • CommentAuthorTobyBartels
    • CommentTimeMar 3rd 2017

    It is maybe cheating to say that a subset is defined by a predicate, just as it may be to say that a function is defined by a formula. Certainly you can get yourself to say some wrong things if you go too far down that road (such as if you identify the uncountably many subsets of \mathbb{N} with the countably many 11-place equality-respecting predicates of natural numbers in the otherwise empty context of a particular language). But it's still true, since

    A={xX|xA}, A = \{x \in X \;|\; x \in A\} ,

    where AA is any subset of XX, and

    f=(xXf(x)Y), f = (x \in X \;\mapsto\; f(x) \in Y) ,

    where ff is any function from XX to YY. (Of course, this predicate and this formula are not in the empty context.)

    It's examples that show students the wide variety of possible subsets and functions. Examples like

    {n|nA n}, \{ n \in \mathbb{N} \;|\; n \notin A_n \} ,

    where AA is any infinite sequence of subsets of \mathbb{N}, and

    (x{0 x 1 x}). \left(x \in \mathbb{R} \;\mapsto\; \left\{\array {0 &x \in \mathbb{Q}\\ 1 &x \notin \mathbb{Q}} \right\} \in \mathbb{N}\right) .

    (These are mere curiosities in the course that I was teaching, but I tried to mention something like them.)

    • CommentRowNumber51.
    • CommentAuthorTobyBartels
    • CommentTimeMar 3rd 2017

    I think that what material set theory gets you pedagogically is that it makes some abuses of notation no longer abuses. Once you prove the soundness of the interpretation of structural set theory within material set theory, you know that you can make these abuses of notation (even if you think structurally and admit that they are abuses) without any fear of confusion.

    Of course, the biggest abuse of notation is the use of xAx \in A as both a typing declaration (when AA is a set and xx is a new variable) and a proposition (when AA is a subset of some set XX and xx is an element of XX). Actually, we abuse a lot of things this way; for example, knk \leq n is normally a proposition, but it's a typing declaration in

    kn(nk) \sum_{k \leq n} \left(n \atop k\right)

    Ultimately, you only know which it is based on whether the variable is new or not; in

    i+jna i,j, \sum_{i + j \leq n} a_{i,j} ,

    the meaning depends greatly on which of ii or jj (or both) is new. Another abuse of notation is to use the same notation for an element of XX and for an element of XYX \oplus Y whenever XX and YY are materially disjoint (which guarantees that there is no overlap between the notations used for elements of XX and for elements of YY if you don't make any other abuses).

    There are a lot of similar abuses of notation that are not justified by material set theory. For example, people often write (a,b,c)(a,b,c) for both ((a,b),c)((a,b),c) and (a,(b,c))(a,(b,c)); not only does material set theory not justify this, it forbids it, since ((a,b),c)(a,(b,c))((a,b),c) \neq (a,(b,c)) (and in a meaningful way, not just by a typing mismatch) when aa, bb, and cc are taken from 2\mathbb{N} \cup \mathbb{N}^2. (If we properly used 2\mathbb{N} \uplus \mathbb{N}^2 instead, then there would be no danger, but then we couldn't use the usual abuse of notation for elements of a disjoint union, even though \mathbb{N} and 2\mathbb{N}^2 are materially and notationally disjoint.) So while it may be nice to say that some notations (structurally abuses) are justified materially, in the end, you're still either going to have to reject all of the other common abuses or just resolve to be careful.

    • CommentRowNumber52.
    • CommentAuthorMike Shulman
    • CommentTimeMar 4th 2017

    an element of {xX|P[x]}\{x \in X \;|\; P[x] \} is an element aa of XX such that P[a]P[a] is true

    My point is that whenever you define a set by saying what its elements are, then you’re not using a formal structural set theory like ETCS or SEAR, since in such a system the elements of a set have no internal structure; there is nothing that they “are”. So while I am all for teaching students how to do mathematics structurally, I don’t think a formal system like ETCS is going to help. Type theory is a little better than both material and structural set theory in this regard, because it is structural in an informal sense but still allows the elements of types to “be” things (e.g. the elements of a product type are pairs, the elements of a function type are functions), but it’s not perfect.

    • CommentRowNumber53.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 5th 2017

    since in such a system the elements of a set have no internal structure

    But I thought the question was about defining subsets by specifying properties PP that the elements satisfy. This is certainly possible for elements x:1Xx: 1 \to X in a structural set theory like ETCS. For example, it’s perfectly acceptable to specify a subset as consisting of elements x:1 2x: 1 \to \mathbb{R}^2 satisfying x 2=1x^2 = 1.

    • CommentRowNumber54.
    • CommentAuthorMike Shulman
    • CommentTimeMar 5th 2017

    No, the question I asked in #46 was not “how do you define a subset?” but rather “how do you define ’subset’?” And the original question back in #40-42 was whether there is a pedagogical advantage to ETCS, or whether it’s actually useful to teach ETCS to undergraduates. I expressed doubt, and right now I’m not being convinced by your example because it doesn’t seem to me that you are actually teaching them ETCS; you’re teaching them some other kind of (informal) structural foundation that seems more like type theory than ETCS to me.

    • CommentRowNumber55.
    • CommentAuthorTobyBartels
    • CommentTimeMar 6th 2017

    @Mike #52:

    whenever you define a set by saying what its elements are, then you’re not using a formal structural set theory

    No, I'm not using a formal structural set theory, and that was so even back in #49 with quotient sets.

    • CommentRowNumber56.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2017

    Okay, I was misled by your saying “I taught the set theory structurally”, and by the context that made me think your comment was intended as a rebuttal to my contention that ETCS doesn’t seem useful for teaching to undergraduates.

    • CommentRowNumber57.
    • CommentAuthorTobyBartels
    • CommentTimeMar 7th 2017

    Yeah, I didn't use ETCS (nor could I reasonably have used ZFC had I been so inclined). I just thought about things and explained things structurally, in particular not saying things like xAx \in A, x=yx = y, A=BA = B, ABA \cap B, and ABA \cup B outside of appropriate contexts.

    • CommentRowNumber58.
    • CommentAuthorMike Shulman
    • CommentTimeMar 7th 2017

    It’s frustrating that there doesn’t seem to be a formal system that exactly matches ordinary mathematical practice in this simple regard.

    • CommentRowNumber59.
    • CommentAuthorTobyBartels
    • CommentTimeMar 9th 2017

    If you can come with a consistent system of abuses of notation that you can argue covers ordinary mathematical practice, then maybe we can formalize that.

    • CommentRowNumber60.
    • CommentAuthorMike Shulman
    • CommentTimeMar 10th 2017

    Hmm, that’s an interesting challenge. Here are two specific desiderata; can we reconcile these in a formal system?

    • Sets can be introduced “higher inductively” by giving a way to construct their elements and a condition for their elements to be equal. This covers products, disjoint unions, quotient sets, and so on. The elements of a set constructed in this way are “new” and don’t belong to any other previously defined set.
    • Sets can also be defined as subsets of an existing set, by separation on a predicate. The elements of such a set are particular elements of the previous set.
    • CommentRowNumber61.
    • CommentAuthorTobyBartels
    • CommentTimeMar 11th 2017

    Perhaps some programming language with subtyping [Wikipedia] would be useful.

    Here's another possible desideratum, not justified by material set theory (at least as usually practised) and not how I did things in my classes a decade ago, but which is nevertheless implicit in Bishop's treatment of sets: quotient sets, rather than having all new elements (like products and disjoint unions have), have the same elements as the original set (like subsets have), just with more equations. To avoid ambiguity, you would need to have some decoration on the equals sign, at least whenever you're not working in the set where the symbols you're putting it between were originally introduced. Thus, 2 Z62 \ne_{\mathbf{Z}} 6 (and this subscript could possibly be left off), but 2= Z/462 =_{\mathbf{Z}/4} 6. Except that in practice, if you already have a symbol for the equivalence relation on the old set, then you can just use that, so instead of 2= Z/462 =_{\mathbf{Z}/4} 6, you just write 2 462 \equiv_4 6 (or even 4624 \mid 6 - 2).

    • CommentRowNumber62.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2017

    Interesting idea. But if the primary motivation is pedagogical, then I’m not sure that would be helpful; quotient sets are already confusing enough without changing the meaning of “equality”. And also, considering the elements of a quotient to be elements of the original set in Bishop-style has a tendency to justify some choice axioms, as Bishop did, but which shouldn’t be baked into foundations.

    • CommentRowNumber63.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2017

    On the other hand, there is of course formally speaking a nice duality between subsets and quotient sets, and they could potentially be combined into one operation with a construction applying to partial equivalence relations…

    • CommentRowNumber64.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2017

    And there are other interesting questions to decide about the behavior of subtyping, such as if A 1A 2A_1\subseteq A_2 and B 1B 2B_1\subseteq B_2, then do we have A 1×B 1A 2×B 2A_1\times B_1 \subseteq A_2\times B_2 and A 1B 1A 2B 2A_1 \sqcup B_1 \subseteq A_2 \sqcup B_2? Do we have B 1 AB 2 AB_1^{A} \subseteq B_2^{A}? We certainly shouldn’t have B A 2B A 1B^{A_2}\subseteq B^{A_1} although some subtyping disciplines do allow such a coercion. But a related question is, if A 3A_3 is a quotient of A 2A_2, is B A 3B A 2B^{A_3} \subseteq B^{A_2}?

    • CommentRowNumber65.
    • CommentAuthorTobyBartels
    • CommentTimeMar 12th 2017
    • (edited Mar 12th 2017)

    And then B A 1B^{A_1} can be a quotient type of B A 2B^{A_2} (when A 1A 2A_1 \subseteq A_2), rather than a supertype. It's just as well that way, since A 1A_1 is the secondary concept.

    • CommentRowNumber66.
    • CommentAuthorMike Shulman
    • CommentTimeMar 12th 2017

    I thought of that too, but then I realized that it’s only true when BB is injective.

    • CommentRowNumber67.
    • CommentAuthorTobyBartels
    • CommentTimeMar 12th 2017

    Oh, right, it fails when BB and A 1A_1 are empty but A 2A_2 is not (and can fail in additional cases constructively.) I meant to check that but must have forgotten.

    • CommentRowNumber68.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2017

    I think there are other problems with allowing the elements of a quotient to be elements of the original set. For instance, suppose ABCA \subseteq B \twoheadrightarrow C and we have x= Cyx=_C y. How do we prevent the substitution law of equality from allowing us to conclude xAyAx\in A \to y\in A?

    • CommentRowNumber69.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2017

    Thinking about it some more, I’m having trouble imagining how we could prevent non-structurality errors without somehow having a notion of “typing” separate from membership. For instance, if we only want to consider ABA\subseteq B when AA and BB are given as subsets of some ambient set XX, then what is it that justifies our considering (in order to be “given” them) the statements AXA\subseteq X and BXB\subseteq X, unless they are a sort of “typing judgment” with a different status?

    • CommentRowNumber70.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2017

    By the way, I just stumbled across this comment by Andreas Blass in which he says

    Mathematicians generally reason in a theory T which (up to possible minor variations between individual mathematicians) can be described as follows. It is a many-sorted first-order theory. The sorts include numbers (natural, real, complex), sets, ordered pairs and other tuples, functions, manifolds, projective spaces, Hilbert spaces, and whatnot. There are axioms asserting the basic properties of these and the relations between them. For example, there are axioms saying that the real numbers form a complete ordered field, that any formula determines the set of those reals that satisfy it (and similarly with other sorts in place of the reals), that two tuples are equal iff they have the same length and equal components in all positions, etc.

    There are no axioms that attempt to reduce one sort to another. In particular, nothing says, for example, that natural numbers or real numbers are sets of any kind. (Different mathematicians may disagree as to whether, say, the real numbers are a subset of the complex ones or whether they are a separate sort with a canonical embedding into the complex numbers. Such issues will not affect the general idea that I’m trying to explain.) So mathematicians usually do not say that the reals are Dedekind cuts (or any other kind of sets), unless they’re teaching a course in foundations and therefore feel compelled (by outside forces?) to say such things.

    So maybe what we are doing is trying to formalize Blass’s theory T (which I think is not nearly so “large and unwieldy” as he seems to think it is).

    • CommentRowNumber71.
    • CommentAuthorNikolajK
    • CommentTimeMar 13th 2017
    • (edited Mar 14th 2017)

    Sounds like a category with types with* XAxioms(X)\sum_X Axioms(X) as objects and embeddings as arrows.

    *edited

    • CommentRowNumber72.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2017

    What?

    • CommentRowNumber73.
    • CommentAuthorNikolajK
    • CommentTimeMar 14th 2017

    It is a many-sorted first-order theory. The sorts include numbers (natural, real, complex), sets, ordered pairs and other tuples, functions, manifolds, projective spaces, Hilbert spaces, and whatnot. There are axioms asserting the basic properties of these and the relations between them. … There are no axioms that attempt to reduce one sort to another. In particular, nothing says, for example, that natural numbers or real numbers are sets of any kind.

    I imagine a collection of types, with the axioms hard coded via a sum type, and the relations between those types also being explicitly realized, so I add a selections of arrows between the types.

    • CommentRowNumber74.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2017

    I suppose you could represent at least some of the structure in that way, but it doesn’t seem to me like how we would want to approach formalizing it. The complaint about structural set theory is, roughly, that sometimes we want more than just functions between sets.

    • CommentRowNumber75.
    • CommentAuthorTobyBartels
    • CommentTimeMar 15th 2017

    I think there are other problems with allowing the elements of a quotient to be elements of the original set. For instance, suppose ABCA \subseteq B \twoheadrightarrow C and we have x= Cyx=_C y. How do we prevent the substitution law of equality from allowing us to conclude xAyAx\in A \to y\in A?

    Back in #49, I wrote things like

    a 11-place predicate PP about elements of XX that respects equality in XX

    I wasn't trying to formalize a system with a flexible notion of equality when I wrote that (it was a follow-up to #45, after all, in which I used [x] RX/R[x]_R \in X/R to distinguish this from xXx \in X). But clearly that was in the back of my mind somewhere.

    Anyway, the substitution rule of equality does not allow you to conclude P[x]P[y]P[x] \to P[y] from x= Xyx =_X y for any 11-place predicate PP about elements of XX, but only for a predicate that respects equality in XX. Which is hardly even a rule, since the validity of this conclusion is what it means for PP to respect equality in XX. (An example of a predicate about rational numbers that does not respect equality is ‹has an odd numerator›. Note that \mathbb{Q} is a subquotient of ×\mathbb{Z} \times \mathbb{Z}, where that predicate does respect equality.)

    To make math easy, you don't want to be checking all the time that your predicates respect equality. This is similar to how in analysis you don't always want to have to check that your functions are measurable. In both cases, you can rely on metatheorems saying that anything that you can write down in a particular language must have the desired property. We're not used to even thinking about this when it comes to equality, but we do often have to think about it at higher levels, with isomorphism in groupoids or equivalence in higher groupoids. (One thing that's great about HoTT is that it's a language that handles all of those.)

    But there's a trade-off between using a restricted language that only lets you write down well-behaved things and using abuses of notation that let you write down all kinds of crazy whatever. In a formal system in which the abuses are legitimized, the rules of inference have to get more fiddly to compensate.

    • CommentRowNumber76.
    • CommentAuthorTobyBartels
    • CommentTimeMar 15th 2017
    • (edited Mar 30th 2017)

    Thinking about it some more, I’m having trouble imagining how we could prevent non-structurality errors without somehow having a notion of “typing” separate from membership. For instance, if we only want to consider ABA\subseteq B when AA and BB are given as subsets of some ambient set XX, then what is it that justifies our considering (in order to be “given” them) the statements AXA\subseteq X and BXB\subseteq X, unless they are a sort of “typing judgment” with a different status?

    Right, if xAx \in A does double duty as x:Ax\colon A (the judgement that the term xx is an element of the set AA) and as x XAx \in_X A (the proposition that the element xx of the set XX belongs to the subset AA of XX), so ABA \subseteq B also does double duty as A:𝒫BA\colon \mathcal{P}B (the judgement that the term AA is a subset of the set BB) and as A XBA \subseteq_X B (the proposition that the subset AA of the set XX is contained in the subset BB of XX). Somewhere around here, there's a discussion where somebody introduced :\colon\subseteq (which should be \joinrel\colon\subseteq, but iTeX won't parse \joinrel) for the typing judgement. (I thought that it might be at SEAR#SEPS, but it's not.)

    In practice, you can usually tell which is meant. If xx is a term that has appeared before in the context and whose type you already know, then xAx \in A should be the proposition (and you should also already know the type of AA and it should be the case that xx is an element of some set XX and that AA is a subset of XX). On the other hand, if xx is a new variable, then xAx \in A serves to enrich the context with a new variable xx for an element of the set AA (and you should already know the type of AA and it should be the case that AA is a set). Similar remarks apply to ABA \subseteq B. It gets trickier when xx is a term whose type you haven't yet established but which is more than just a new variable. In #51, I mentioned an ambiguous example with \leq (rather than \in or \subseteq).

    • CommentRowNumber77.
    • CommentAuthorTobyBartels
    • CommentTimeMar 15th 2017

    Blass’s theory T

    That's more or less what I meant by

    the imprecisely defined naive set theory of the ordinary mathematician

    in #39.

    • CommentRowNumber78.
    • CommentAuthorTobyBartels
    • CommentTimeMar 15th 2017

    Treating \mathbb{Z} as a subtype of \mathbb{Q} as a subtype of \mathbb{R} as a subtype of \mathbb{C} (and treating 22, for example, as simultaneously an element of all of them) can lead to confusion even in something as basic as the College Algebra classes that I teach. Consider this instruction:

    Factor 2x 4+x 212 x^4 + x^2 - 1.

    This actually has a different answer in each context:

    (2x 21)(x 2+1), (2 x^2 - 1) (x^2 + 1) , 2(x 21/2)(x 2+1), 2 (x^2 - 1/2) (x^2 + 1) , 2(x2/2)(x+2/2)(x 2+1), 2 (x - \sqrt{2}/2) (x + \sqrt{2}/2) (x^2 + 1) , 2(x2/2)(x+2/2)(xi)(x+i). 2 (x - \sqrt{2}/2) (x + \sqrt{2}/2) (x - \mathrm{i}) (x + \mathrm{i}) .

    The first (factoring over the integers) is what one normally does in Algebra; the second (factoring over the rational numbers) doesn't really come up, but I included it for the sake of the transition; the next two (factoring over the real numbers and factoring over the complex numbers) are things that the students are asked to do, but only in special cases.

    Obviously, the problem is that the instruction ‘Factor’ is incomplete, and one should add ‘over the integers’ or whatever. But leaving that bit out is exactly the same kind of abuse as writing ‘22’ without specifying what system this 22 is taken from.

    • CommentRowNumber79.
    • CommentAuthorMike Shulman
    • CommentTimeMar 16th 2017

    Re: #76, I think that — especially for pedagogical purposes — I would prefer to come down on the side of using a language that makes all predicates respect equality. If that means that we can’t formalize the abuse of notation where by the elements of a quotient set are literally elements of the original set, then I’m okay with that; I was dubious about such an abuse already.

    • CommentRowNumber80.
    • CommentAuthorMike Shulman
    • CommentTimeMar 23rd 2017

    How about this as a basic framework?

    • Every mathematical object has a type, which is another mathematical object. We write x:Ax:A. “Being a type” is a property of mathematical objects.
    • There is an operation taking every type AA to a type PAP A that is its type, i.e. A:PAA:P A.
    • The objects of type PAP A are called subsets of AA, and there is a specified relation \in between them and objects of type AA, which satisfies the separation axiom. Moreover, for every x:Ax:A we have xAx\in A; the latter is well-typed since A:PAA:P A.
    • There is a monoid structure (,)(-,-) on all mathematical objects, and a monoid structure ×\times on all sets (i.e. objects whose type is of the form PAP A) that preserves types (i.e. if AA and BB are types, so is A×BA\times B). If x:Ax:A and y:By:B, then (x,y):A×B(x,y):A\times B; and if S:PAS:P A and T:PBT:P B then S×T:P(A×B)S\times T : P(A\times B). Note that these are associative, so that S×(T×U)=(S×T)×US\times (T\times U) = (S\times T)\times U (and is written S×T×US\times T\times U), and (x,(y,z))=((x,y),z)(x,(y,z)) = ((x,y),z) (and is written (x,y,z)(x,y,z)). The elements of S×TS\times T (for any sets S,TS,T, including but not restricted to types) are exactly those of the form (x,y)(x,y) for a unique xSx\in S and yTy\in T, and ()() is the unique element of 1\mathbf{1} (the unit of ×)\times).
    • Mathematical objects are equipped with three partial binary operations ++, inlinl and inrinr. The object S+TS+T is defined iff SS and TT are sets, preserves types, and if S:PAS:P A and T:PBT:P B then S+T:P(A+B)S+T:P(A+B). The object inl T(x)inl_T(x) is defined iff TT is a set, and if x:Ax:A and T:PBT:P B then inl T(x):A+Binl_T(x):A+B and moreover inl T(x)=inl B(x)inl_T(x)=inl_B(x). Similarly, inr S(y)inr_S(y) is defined iff SS is a set, and if S:PAS:P A and y:By:B then inr S(y):A+Binr_S(y):A+B and inr S(y)=inr A(y)inr_S(y)=inr_A(y). For any sets S:PAS:P A and T:PBT:P B, the elements of S+TS+T are exactly those of the form inl B(x)inl_B(x) or inr A(y)inr_A(y) (but not both) for a unique xSx\in S or yTy\in T. In addition, ++ has a two-sided unit \emptyset. (I suppose we could consider making ++ associative too.)
    • Mathematical objects are equipped with two partial binary operations denoted by S,TPF(S,T)S,T \mapsto PF(S,T) (“the set of partial functions”) and application f,xf(x)f,x \mapsto f(x). The object PF(S,T)PF(S,T) is defined iff SS and TT are sets, preserves types, and if S:PAS:P A and T:PBT:P B then PF(S,T):P(PF(A,B))PF(S,T):P(PF(A,B)). If application f(x)f(x) is defined, then f:PF(A,B)f:PF(A,B) and x:Ax:A and f(x):Bf(x):B for some types A,BA,B. Moreover, for any sets S:PAS:P A and T:PBT:P B, the elements of PF(S,T)PF(S,T) are precisely those f:PF(A,B)f:PF(A,B) such that if f(x)f(x) is defined, then xSx\in S and f(x)Tf(x)\in T. Partial function comprehension holds: for any property ϕ(x,y)\phi(x,y) relating elements x:Ax:A with y:By:B such that for any xx there is at most one yy such that ϕ(x,y)\phi(x,y), there exists a unique f:PF(A,B)f:PF(A,B) such that f(x)f(x) is defined iff there exists a yy such that ϕ(x,y)\phi(x,y) in which case ϕ(x,f(x))\phi(x,f(x)). We write T ST^S for the subset of PF(S,T)PF(S,T) consisting of the total functions.

    You get the idea. I haven’t written out quotient sets in this style yet, but you can guess how they would go; they could take as input either an equivalence relation on a set, or a partial equivalence relation on a type (both defined as a particular subset of a cartesian product).

    • CommentRowNumber81.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 24th 2017

    Looks nice, but I can’t make any mathematically informed comments/criticism.

    • CommentRowNumber82.
    • CommentAuthorMike Shulman
    • CommentTimeMar 24th 2017

    FWIW, this wasn’t intended to be a rigorous presentation of any formal system, just an informal description of how such a system might look.

    • CommentRowNumber83.
    • CommentAuthorTobyBartels
    • CommentTimeMar 30th 2017

    @Mike #79:

    Re: #76

    I assume that you mean #75.

    I think that — especially for pedagogical purposes — I would prefer to come down on the side of using a language that makes all predicates respect equality.

    This is probably sound. Treating quotient sets similarly to subsets would be interesting to try but more difficult for the beginner.

    But notice that a lot of math at the pre-undergraduate level is written in such a way that the substitution property of equality is not taken as a logical tautology but rather as a series of more specific properties. Thus Algebra textbooks will speak of the Additive Property of Equality separately from the Multiplicative Property of Equality and in essentially the same way that they treat the Additive Property of Inequality (but the Multiplicative Property of Inequality is more complicated). So somewhere there is this idea that, pedagogically, you have to point out whenever a predicate respects equality.

    • CommentRowNumber84.
    • CommentAuthorTobyBartels
    • CommentTimeMar 30th 2017

    Re #80:

    That looks very elegant. Everything has a type, but that type is a sort of ambient set out of which we may carve smaller subsets. As the ambient set is a subset of itself, it is both a set and a type; but on the other hand, not every set is a type, some of them are just subsets of something larger.

    For the sorts of math classes that I teach now (remedial Algebra through multivariable Calculus for engineers), I take \mathbb{R} as a type, with \mathbb{Z} and \mathbb{Q} merely sets (subsets of, in this case, \mathbb{R}), while fancier sets such as \mathbb{C} and 3\mathbb{R}^3 must be constructed from \mathbb{R} (and so are also types). But in my Discrete Math courses from a decade ago, the only primitive type would have been \mathbb{N}, which everything else constructed from that.

    • CommentRowNumber85.
    • CommentAuthorMike Shulman
    • CommentTimeMar 30th 2017

    somewhere there is this idea that, pedagogically, you have to point out whenever a predicate respects equality.

    I would rather teach students the idea that all predicates respect equality.

    For the sorts of math classes that I teach now (remedial Algebra through multivariable Calculus for engineers), I take \mathbb{R} as a type, with \mathbb{Z} and \mathbb{Q} merely sets (subsets of, in this case, \mathbb{R}), while fancier sets such as \mathbb{C} and 3\mathbb{R}^3 must be constructed from \mathbb{R} (and so are also types). But in my Discrete Math courses from a decade ago, the only primitive type would have been \mathbb{N}, which everything else constructed from that.

    Yes, this is an interesting issue. I wonder whether there could be some formal “abstraction mechanism” to define new types, like \mathbb{R}, which we eventually definitely want to treat as a type, but foundationally we want to construct as a subset or quotient of something or other else.

    • CommentRowNumber86.
    • CommentAuthorTobyBartels
    • CommentTimeMar 30th 2017

    I would rather teach students the idea that all predicates respect equality.

    The problem is that this is just not true, or at least not true until you've defined ‘predicate’ sufficiently narrowly. Take the example of the numerator of a rational number (or the whether the numerator is odd to make it truth-value-valued). Besides teaching them that all predicates respect equality, you also have to teach them why that is not a predicate (in the narrow sense). And to my mind, the reason why it's not is ultimately that it doesn't respect equality! (That's how you define a predicate on a quotient set: define a predicate on the original set, and then check that it preserves equality in the quotient set.)

    I wonder whether there could be some formal “abstraction mechanism” to define new types, like \mathbb{R}, which we eventually definitely want to treat as a type, but foundationally we want to construct as a subset or quotient of something or other else.

    Although you didn't write it down, it seems as if you wanted to make quotient sets new types. You can do that with subsets too, and indeed did, with the concept of tabulations in SEAR. But if we do that all of the time, then we've lost some of the automatic simplification of notation. It needs to be something that we can choose to do or not according to how we want to think about things.

    • CommentRowNumber87.
    • CommentAuthorMike Shulman
    • CommentTimeMar 30th 2017

    I have no quarrel with your comments about predicates, except that I would argue that the “narrow” definition of “predicate” is the correct one. So I would rather teach students that all predicates respect equality, and thereby why certain things that seem like predicates are not actually predicates. That’s the same thing we do with functions, after all; a predicate is just a truth-value-valued function.

    Yes, I did want to make quotient sets new types, and in particular to take quotients of sets that might not be types. It didn’t occur to me at the time, but now I guess that that already entails the ability to make subsets into new types as well, by quotienting by the identity equivalence relation on a subset (or equivalently by a coreflexive PER on a type).

    • CommentRowNumber88.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 3rd 2018

    I added a mention of the axiom of extensionality.

    diff, v5, current

    • CommentRowNumber89.
    • CommentAuthoratmacen
    • CommentTimeJan 22nd 2020

    Wow, I really missed a good conversation (starting at around #60) in which to plug Nuprl-style systems. Better late than never? Conveniently, I had put up a bunch of stuff on prototype CLF last year, which is my work-in-progress Nuprl-style system. Informally, I distinguish between “members” and “elements” of types. Members are (relatively) intensional, while elements are extensional. Quotient types have the same members as the original type, but typed functions can only distinguish members when they denote the same element. (That is, they need to respect typed equality.) Membership reasoning is also allowed, subject to the constraint that a membership predicate is a typed function, so it needs to respect equality of some “prior” type. This does not preclude materialish subset types B{x:A|P[x]}B \coloneqq \{x:A\,|\,P[x]\} so that given a:Aa\,:\,A, aBa \in B means P[a]P[a].

    I put some discussion on the difference from material set theory at PER theory.

    Bishop-like choice principles don’t seem to pop up. I think those are due to the interaction between Bishop-style quotients and Bishop-style universal quantifiers, whose proofs aren’t required to respect typed equality.

    • CommentRowNumber90.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 23rd 2020

    Philosophy gets itself very confused by this quotienting, how to switch between the groupoid of an equivalence relation and the set of equivalence classes. So you say ’this direction’ pointing to a line, and it seems hard to realise that you can point to a specific line but as existing in a type where identity is parallelism.

    • CommentRowNumber91.
    • CommentAuthoratmacen
    • CommentTimeJan 23rd 2020

    What confused me about it at first was not so much using an example to denote an equivalence class, but the consequences for the rest of the type system of not explicitly passing to an equivalence class. Every open term actually refers to an equivalence class, and while you can always ask if an object is self-related by a PER (membership), there is generally not a meaningful membership question for an equivalence class. The result is that Nuprl is mostly like extensional type theory, but with clever additions based on a theory of membership which is AFAIK completely unique.