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 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-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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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: structural set theory

Bottom of Page

1 to 34 of 34

  1.  
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeOct 2nd 2009

    In response to discussions at set theory, created structural set theory with a tentative formal definition of when a set theory is "structural."

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 15th 2011

    I have moved the notion of “structural presentation” of a set theory to its own page, structurally presented set theory.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 15th 2011

    Also, I am pasting here for future reference the discussions that have been sitting around at the bottom of structural set theory and removing them.

    Arnold Neumaier: To me this looks more like a theory of copies of cardinal numbers that like a set theory. I think you should change the name “set” to “universe” or “collection”, or so. For your sets have very different properties from Cantor’s sets, whose terminology surely has priority. Cantor’s sets allow unions and intersections, your sets don’t. You do not even have the set {0,1,2}. Thus it is impossible to rewrite standard mathematics on your alternative foundation without changing the semantics of everything.

    The name subset, on the other hand, is ok, since it shares enough properties of a set to be recognizable as a close relative. On the other hand, there are no functions from a subset to another subset, which again makes it quite cumbersome using this for ordinary mathematics.

    How would you form something that substitutes for sets of relations, or subsets of subsets? What do you say in place of “A is a subset of A∪\cupB”? I think in SEAR, expressing ordinary mathematics becomes exceedingly tedious.

    SEAR and ZF, “This process is described at pure set”. This is a sham. There it says “A pure set is a set of pure sets”. But with set understood as a SEAR-set, pure sets cannot be compared for equality. But this is an intrinsic part of ZF.

    Toby: It is very astute of you to say that this is really a theory of cardinal numbers!

    AN: I did not say that; it isn’t. I said that SEAR is a theory of copies of cardinals. For there is a unique cardinal 1 in set theory. But if A,B are two SEAR sets with exactly one element, one is not able to conclude that A and B are the same SEAR set. Thus one can have many meta-distinct copies of the same cardinal around, although it is impossible to express this on the formal level.

    • Toby: Lawvere's claim (if I understand him) is that Cantor also had a theory of copies of (what we now call) cardinal numbers. Cantor started with a set AA of real numbers, abstracted away everything except the order relation to get the (not necessarily well-)ordinal number A¯\overline{A}, then abstracted even the order (but not the equality relation) away to get the cardinal number A¯¯\overline{\overline{A}}. Of course, he said that A¯¯\overline{\overline{A}} and B¯¯\overline{\overline{B}} are equal cardinal numbers if (and only if) there is a bijection between AA and BB, but that is a definition, not an axiomatic identity.

    AN: I’d say this is abstracting away the equality relation and replace it by isomorphy.

    Toby continues: Lawvere has long said that his ’abstract sets’ and Cantor's ’Kardinalzahl’ are the same thing. But in fact the word ’set’ (’Menge’) is not only used in Cantor's original sense of a subset of some fixed universe (originally the collection of real numbers, eventually the entire von Neumann hierarchy) today. Whenever someone says ’A group is a set equipped with […]’, the only thing that matters for group theory is the abstract set, the Kardinalzahl. It is very easy to rewrite standard mathematics on this foundation;

    AN: If it were very easy, it would have been done already. I see many obstacles in actually doing that.

    • Toby: It has been done already, and has been since at least the '60s.

      AN: Then please show me the result in the form of a treatise comparable to Bourbaki’s Elements of mathematics. Its existence would mean it has been done. But there is not even a textbook on calculus that is rewritten on this foundation!

      • Toby: There is no need to rewrite an ordinary calculus textbook on this foundation, any more than we needed to rewrite elementary geometry after Hilbert. The material in basic calculus is mostly from the 19th century, after Weierstrass but before Dedekind and Cantor; more advanced material requires care (and indeed, led Dedekind and Cantor to develop set theory), but high school calculus does not. You may as well rewrite a textbook on the history of the Soviet Union for all the difference that it would make; the latter might at least mention set theory if it went deep enough. The ’sets’ of calculus are subsets of R\mathbf{R} (or R n\mathbf{R}^n); the ’functions’ are partial functions from R\mathbf{R} to R\mathbf{R}, which may be formalised as functional relations. They are not exactly the same as the ’sets’ and ’functions’ of either SEAR\mathbf{SEAR} or ZF\mathbf{ZF}, but we can understand them.

        All that said, calculus has been written down in an explicitly structural way, in Errett Bishop's book on constructive analysis. However, the book that you want is probably Sets for Mathematics, by Lawvere & Rosebrugh. Of course, it is not comparable to Bourbaki; nothing is. You will find it far too brief, but it shows how to get started.

      Toby continues: The point of SEAR\mathbf{SEAR} is to do it in a less category-inspired, hopefully more familiar, way. Show me an obstacle in applications of set theory to ordinary mathematics, if you have one.

    …

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 15th 2011

    …

    AN: The example of the exercise below shows that you need to interpret all sets of which unions or intersections are taken as subsets of a more universal set. Thus the SEAR notion of set is in fact that of a universe (and nothing like the standard concept of a set), while the notion of a SEAR subset is more or less that of an ordinary set.

    • Toby: If by ’universe’ you mean set² and by ’ordinary set’ you mean set¹, then you are right. But you are wrong about what is the standard conception among mathematicians. There are many of us structural mathematicians; we find each other on the Internet (and found each other before, but I am too young for that); how did that happen? are we suffering from a mass delusion? or perhaps we are not really mathematicians (we have a tendency to work on category theory, after all)?

      Of course, one can embed all mathematics into SEAR (with the right existence axioms) by doing everything inside a single universe (= a SEAR set whose cardinality is inaccessible). This is what I would do if I were forced to work in SEAR (which fortunately I am not); then I have materiasl equality of sets (= subsets of the universe). Then one can use standard language and standard notation without difficulty and doesn’t have to rewrite anything, except perhaps add to the strength of SEAR a condition that allows this universe to exists and the collection of its subsets to satisfy the ZF axioms.

      But you’d have to rewrite everything if you want to enforce the terminology of SEAR upon mathematics (relabel lots of sttandard sets as subsets or tabulations, etc.. I don’t believe mathematical language will take this turn.

    • Toby: No, you wouldn't! There is no need to strengthen SEAR\mathbf{SEAR} to include an uncountable inaccessible cardinal and then talk only about subsets of a universe with that cardinality; indeed, it would be foolish to, since then more things would be true than you had wanted. Instead, you just write normally, with the abuses of language being slightly different abuses. See below, where I am more radical than Mike, for more on this.

    Toby continues: while in a sense the semantics has changed, it is the claim of structural set theorists that we are getting at what was the real meaning all along. You might as well say that Dedekind changed the semantics of algebra and analysis when he identified ideal numbers and real (possibly irrational) numbers with certain sets, and in a way he did, but he also clarified those ideas. And it is not just us, coming along more than a hundred years after Cantor to change the language; people have been doing structural set theory for some time, and it pops up in many places. Errett Bishop, for example, who wanted a constructive theory (not particularly a structural theory), wrote down a structural theory in his handbook of analysis all the same, even defining a subset of XX as a set AA equipped with an injection to XX (an unfamiliarity which the point of SEAR\mathbf{SEAR} is largely to avoid). Any application of set theory in which we do not care what our sets' elements' elements are is inherently structural and translates directly into structural terms. Any time that someone says ’Relabel the element of BB if necessary so that BB will be disjoint from AA, then consider A∪BA \cup B.’, they really mean ’Consider the disjoint union of AA and BB.’ in a structural set theory. Very rarely do applications of set theory ever call for the hierarchy of pure sets.

    As for that … I'll assume that you don't know the strength of ’sham’ in English, so I won't feel insulted.

    AN: Sorry. I meant that the pure set page is a caricature of what was promised by the context of the link. (I hope this is acceptable language.) No argument was given for why the ZF axioms should hold; everything beyond the heditarily finite sets (which is the trivial part of ZF) is far too sketchy to support the strong claim that SEAR is equivalent to ZF.

    • Toby: This is all fairly well known; see (for example) Mac Lane & Moerdijk (I think Section VI.5) for details (although this does not deal with Replacement/Collection),

      AN: so it is not a verification of the ZF axioms, which is what I had claimed is missing.

      Toby continues: or Chapter 8 of Mike's paper Unbounded Quantifiers and Strong Axioms in Topos Theory (is that available yet, Mike?). Of course, these start with an explicitly categorial approach, but the equivalence of that with the approach of SEAR\mathbf{SEAR} is fairly straightforward.

      Mike Shulman: No, it’s not available yet, sorry. I got sidetracked with other things. But it’s back near the top of the to-do list.

      AN: Then this should be mentioned in the main text rather than left for the reader to discover for himself or to wonder whether this is really true. Mathematics has a healthy convention that nontrivial claims are supported either by proofs or references to such proofs. Without these one is entitled to mistrust the claim.

    …

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 15th 2011

    …

    Toby: You may mistrust it if you like. It is mentioned up top that this is all original; if there were papers to cite that we knew of, then we would cite them. If what you really want is to be certain that mathematics can be founded on a structural theory, then you should look at the established literature on ETCS\mathbf{ETCS} or the type theory of Per Martin-Löf and Thierry Coquand.

    Toby continues: But if you want precision, look at the Definition section, not the vague Idea. Equality of pure sets is also defined.
    (There's still an error in that which I haven't fixed, but it's correct for well-founded pure sets, which are the ones that ZFC\mathbf{ZFC} has.)

    AN: I only saw a definition of equivalence. Now I realize that this should substitute for the nonexistence equality. I’ll comment more on the pure set page.

    Toby continues: If you want a set of sets, you should consider whether it matters whether any of these sets happen to be equal, and how (for purposes of your application) you would know. In general, you take a family of sets (note to self: write an article there), that is an index set II and, for each element kk of II, a set S kS_k. There is a handy trick for encoding this sort of thing as a set 𝒮\mathcal{S} and a function π:𝒮→I\pi: \mathcal{S} \to I; let S kS_k be the preimage of π *(k)\pi^*(k) (which is a subset of 𝒮\mathcal{S}. The purpose of the axiom of collection is to allow you to construct this set 𝒮\mathcal{S} (maybe I should write that down there for its motivation!). If you want, say, a family of groups, then you take π:𝒮→I\pi: \mathcal{S} \to I and additionally a function M:I×𝒮×𝒮→𝒮M: I \times \mathcal{S} \times \mathcal{S} \to \mathcal{S} such that, for each kk, MM restricts to a function m k:S k×S k→S km_k: S_k \times S_k \to S_k that satisfies the group axioms. And so on.

    In this situation, you can't ask whether S k=S k′S_k = S_{k'}, or try S k∩S k′S_k \cap S_{k'}, etc. If the structural perspective is valid, then you should only ever want to do that if the various S kS_k are all subsets of some previously given ambient set TT. There are two ways to do this; either define an II-indexed family of injections S k→TS_k \to T, or skip all of the above and instead consider a binary relation on II and TT; let S kS_k be the set of elements of TT that kk is related to. This is a family of unary relations on TT; you can do a set of binary relations in a similar way. (By the way, in this case you don't need the axiom of collection to define 𝒮\mathcal{S}, since you can make it a subset of I×TI \times T. This is the idea, possibly familiar to you, that replacement/collection is not needed wherever it naïvely applies, but only for relatively high-powered stuff.)

    David Roberts: I was going to ask something about the claim that after axioms 0,1 and 2 we have a category of sets (which I think is very cool), but I convinced myself that this was a metacategory with a collection of arrows between a pair of objects and a composite for each pair of (composable) arrows one is given. However, from Mike’s reply to my question, we can use the definition of the set of functions to then define a metacategory with a set of arrows between any two objects (this I must admit requires more than just a sweeping statement) but still only a collection of objects. Once one has defined universes, then - as much as I understand it - things can proceed much as with any other category U−SetU-Set one might define with a universe UU. We then have the universal family that the axiom of collection is a virtual shadow of.

    In response to Toby’s comment about forming the union of sets above: it always annoyed me that people worry whether sets just happen to have elements in common. It is very much a 'is 2∈π\sqrt{2} \in \pi?' type thing.

    Mike Shulman: I agree with pretty much everything Toby said, except that I don’t think I would go so far as to claim that structural set theory gets at what was the real meaning all along. Maybe it’s what Cantor meant, maybe it isn’t (probably he wouldn’t even have understood the question as we ask it today). Instead, I would say that over the course of the 20th century, it emerged that sets in mathematics were only ever really used structurally.

    AN: only ever?? Undergraduate mathematics is always conceived of materially. It can hardly be taught from a strictly structural point of view. Even many of the most exercises for undergraduates would have to be rewritten completely, and to avoid that things would get completely confusing, utmost care is needed.

    SEAR cannot even define the elementary sets {a,b,c} and {a,b,d} and take their union {a,b,c,d}. These objects exist in SEAR only as subsets, but they are different objects depending on the set a,b,c,d are elements of. But it doesn’t matter which set this is, and a purely structural view should take that into account! Thus one needs to assume a universal set from which all objects of discourse are taken that one might want to have as element in some set. (For maybe one will later introduce an element e….) The subsets of this universal set then form a proxy of the sets of standard set theory. But having that (and augmenting the universal set to contain power sets, which is a natural next step), one can do all standard mathematics in this universal set, obviating the need for SEAR.

    • Toby: I have taught naïve set theory in a structural way.

      AN: I’s like to get a copy of the lecture notes!

    …

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 15th 2011

    …

    • Toby: No lecture notes, I'm afraid, but you can look at the homework assignments. I'm not sure if you'll like it, since it's not very formal; I'll probably still have to convince you that everything can be formalised in SEAR\mathbf{SEAR} (which is fine, just ask). The assignment for July 10 makes it particularly clear that the set theory is structural, and it shows you how to intepret in a structural framework some of the most basic questions of naïve set theory; the assignment for July 13 is also a good one for featuring the disjoint union. But really, the point to get is that you normally can't tell whether someone thinks of set theory materially or structurally; the ideas are almost always almost exactly the same. So if you're not sure how to formalise, say, July 11 in SEAR\mathbf{SEAR}, then perhaps we should talk about that.

      Toby continues: Not that I made a big point about that, but then I didn't need to! The only thing unusual that I had to do was to introduce the concept of disjoint union, which actually made the applications in that course (which were to combinatorics) a little easier. Of course, a course in axiomatic set theory would have to be rewritten.

      For the exercise ‘What is the union of {a,b,c}\{a,b,c\} and {a,b,d}\{a,b,d\}?’, there is no need to change that in the naïve course. But formally, it means ‘Let UU be a set, and let a,b,c,da,b,c,d be elements of UU. Then (by previous results) we have subsets {a,b,c}\{a,b,c\} and {a,b,d}\{a,b,d\} of UU. Find a similar expression for the union of these subsets.’.

      AN: And you are not allowed to claim that {a,b,c} are sets! I am quite sure you didn’t go that far in your course on naive set theory!

      Toby: I don't understand what you're saying that I'm not allowed to claim here. There is a technical distinction between {a,b,c}\{a,b,c\} as a subset of UU and {a,b,c}\{a,b,c\} as a 33-element set in its own right, one which is usually glossed over. But you can think of it as either, if you wish. The subset comes first; in SEAR\mathbf{SEAR} it is a relation 1↬U1 \looparrowright U; then its tabulation is a 33-element set, which by abuse of notation we also write {a,b,c}\{a,b,c\}.

    Mike Shulman continues: The reason I believe in structural set theory is not out of a philosophy that this is the “real” meaning of sets; in fact I think that ZF-theorists are studying a very real and interesting world! But when I look at most mathematics as it is done by most mathematicians, what I see is sets treated structurally—so I think we should have a foundational account of sets which treats them that way.

    AN: And when I look at most mathematics as it is done by most mathematicians, what I see is sets treated materially.

    Clearly, this is not inherent in the mathematical writings but in the view. One needs both the material and the structural view, and foundations should provide both in an easy way.

    To start with the material point of view has many advantages: It is easy to motivate, makes for easy language, and most textbooks are already written in that style.

    Mike Shulman: Can you cite some example of mathematics outside of ZF-theory which really treats sets materially?

    AN: In analysis, the vector space of real n-dimensional column vectors is probably universally treated as material.

    • Toby: How can you tell?
    The material point of view is even clearly visible in books on abstract algebra that use category theory, such as

    Serge Lang, Algebra, second printing 1970

    (which I happen to have at hand; sorry - my books on elementary math are all 40 years old, but all mathematics done then is still valid mathematics today!)

    He begins in the first paragraph of the prerequisites with the assumption that a set may be contained in another set. This is actually heavily used; for example, a subgroup is for him clearly a group contained in another group, and not a group isomorphic to a such a group.

    [This is also the case in modern text; the first algebra lecture notes I found with Google was by Wilkins has the same terminology for subgroups.

    In Section I.7 on categories, he explicitly uses the formula A=B comparing two objects of a category for equality. Since Lang explicitly defines each allowed abuse of language, e.g., “By abuse of language, we sometimes refer to the collection of objects [of a category] as the category itself”, it is clear that he doesn’t consider A=B as an abuse of language, and hence adheres to a material point of view.

    • Toby: If AA and BB are objects in the same category, then writing A=BA = B is perfectly structural. It's evil, but that's a somewhat different matter. In category theory founded on SEAR\mathbf{SEAR}, comparing objects of a small category for equality is perfectly legitimate, because we have a set of objects. It gets messier when you talk about large categories; since you can't write A=BA = B for sets in SEAR\mathbf{SEAR}, you can't do it for objects of the category of sets either. (On the other hand, this is still not a matter of structural set theory exactly; for example ETCS\mathbf{ETCS} admits a notion of equality of sets.)

    One can probably rewrite everything in a way that avoids all material issues, but (i) it hasn’t be done, and (ii) it would read quite different from what Lang actually writes.

    …

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 15th 2011

    …

    Mike Shulman: I think the claim is not that existing mathematics doesn’t use the language of material set theory (after all, for decades that was the only language there was), but rather that its essence does not. Show me a result using the fact that a subgroup is a group literally contained in another group, but which would not work just as well for any injective group homomorphism.

    AN: Maybe, but this cannot be discussed objectively since essence is not well-defined.

    Toby: I do claim that existing mathematics uses the language of material set theory only a little more than it uses the language of structural set theory; for the most part, it is simply indifferent between them. In both cases, it is rife with little abuses of terminology and notation; if (like Lang) one is careful about that sort of thing, then it will be clear whether one thinks of sets materially or structurally. But if Lang had written the prerequisite set theory structurally, then the definition of ’subgroup’ could still have been written with exactly the same words (from my copy, 1993 edition)

    Let GG be a group. A subgroup HH of GG is a subset of GG containing the unit element, and such that HH is closed under the law of composition and inverse.

    In the prerequisites, he might(*) mention the abuse of language in which a subset is conflated with its underlying set (what Mike calls its ’tabulation’), which we need in order to think of HH as a set (and then a group) in its own right. But that is all in the set theory; the language of algebra is the same.

    (*) On the other hand, there are other things that he did not mention. For a map f:A→Bf : A \to B, he defined the preimage f −1(B′)f^{-1}(B') of a subset B′B' of BB, but never defined the image f(A′)f(A') of a subset of AA, even though this is used in the text. (He only mentioned f(A)f(A) itself.) If he had, then he would have had to note the ambiguity in the case that A′A' is also an element of AA; this doesn't come up structurally. (Even for f(A)f(A), it's hard to imagine that really intended to rely on the axiom of foundation to rule out the possibility that A∈AA \in A.) He took care to define what a ’family of elements’ of a given set is, but not a ’family of sets’, even though he mentions the concept. That is harder to formalise, both materially and structurally. Basically, he seems to avoid things that are tricky to state precisely.

    The most common exception that I admit to my thesis is the disjoint union, or rather the reluctance to see this as one of the basic operations of set theory. It is actually easier (although not much) to construct a disjoint union materially than structurally (unless you take its existence as an axiom), but many people don't bother. What I do see is a lot of broad abuse of language to get around this, such as ’Take two disjoint copies of AA.’ or ’If AA and BB are not disjoint, then relabel the elements of BB so that they are, and consider A∪BA \cup B.’. Structurally, you would not be tempted to say such things; although if we had all grown up with structural set theory, I'm afraid that we might have a tendency write ‘A∪BA \cup B’ for the disjoint union when AA and BB bear no relation, and that would also be an abuse of notation.

    Mike Shulman: I’m actually basically in agreement with you, Toby, but I didn’t feel like getting into detail about the sorts of “abuses” (i.e. definitions of terminology/notation) that are necessary to read existing mathematics in a structural way. But you make a good point that reading it in a material way requires different “abuses,” some of which people tend to make explicit and some of which they don’t.

    BTW, in a more leisurely pedagogical treatment of SEAR, I would be tempted to include an axiom of disjoint unions early on, and only remark later, after powersets are introduced, that they imply the existence of disjoint unions.

    Toby: Also quotient sets and (in a constructive theory) function sets make good axioms; one may want these constructions even if one drops power sets. But for people weaned on ZFC\mathbf{ZFC}'s pairing and union axioms, disjoint unions are particularly important!

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 15th 2011

    And the other one:

    Mike Shulman: I think the claim is not that existing mathematics doesn’t use the language of material set theory (after all, for decades that was the only language there was), but rather that its essence does not. Show me a result using the fact that a subgroup is a group literally contained in another group, but which would not work just as well for any injective group homomorphism.

    AN: Maybe, but this cannot be discussed objectively since essence is not well-defined.

    Toby: I do claim that existing mathematics uses the language of material set theory only a little more than it uses the language of structural set theory; for the most part, it is simply indifferent between them. In both cases, it is rife with little abuses of terminology and notation; if (like Lang) one is careful about that sort of thing, then it will be clear whether one thinks of sets materially or structurally. But if Lang had written the prerequisite set theory structurally, then the definition of ’subgroup’ could still have been written with exactly the same words (from my copy, 1993 edition)

    Let GG be a group. A subgroup HH of GG is a subset of GG containing the unit element, and such that HH is closed under the law of composition and inverse.

    In the prerequisites, he might(*) mention the abuse of language in which a subset is conflated with its underlying set (what Mike calls its ’tabulation’), which we need in order to think of HH as a set (and then a group) in its own right. But that is all in the set theory; the language of algebra is the same.

    (*) On the other hand, there are other things that he did not mention. For a map f:A→Bf : A \to B, he defined the preimage f −1(B′)f^{-1}(B') of a subset B′B' of BB, but never defined the image f(A′)f(A') of a subset of AA, even though this is used in the text. (He only mentioned f(A)f(A) itself.) If he had, then he would have had to note the ambiguity in the case that A′A' is also an element of AA; this doesn't come up structurally. (Even for f(A)f(A), it's hard to imagine that really intended to rely on the axiom of foundation to rule out the possibility that A∈AA \in A.) He took care to define what a ’family of elements’ of a given set is, but not a ’family of sets’, even though he mentions the concept. That is harder to formalise, both materially and structurally. Basically, he seems to avoid things that are tricky to state precisely.

    The most common exception that I admit to my thesis is the disjoint union, or rather the reluctance to see this as one of the basic operations of set theory. It is actually easier (although not much) to construct a disjoint union materially than structurally (unless you take its existence as an axiom), but many people don't bother. What I do see is a lot of broad abuse of language to get around this, such as ’Take two disjoint copies of AA.’ or ’If AA and BB are not disjoint, then relabel the elements of BB so that they are, and consider A∪BA \cup B.’. Structurally, you would not be tempted to say such things; although if we had all grown up with structural set theory, I'm afraid that we might have a tendency write ‘A∪BA \cup B’ for the disjoint union when AA and BB bear no relation, and that would also be an abuse of notation.

    Mike Shulman: I’m actually basically in agreement with you, Toby, but I didn’t feel like getting into detail about the sorts of “abuses” (i.e. definitions of terminology/notation) that are necessary to read existing mathematics in a structural way. But you make a good point that reading it in a material way requires different “abuses,” some of which people tend to make explicit and some of which they don’t.

    BTW, in a more leisurely pedagogical treatment of SEAR, I would be tempted to include an axiom of disjoint unions early on, and only remark later, after powersets are introduced, that they imply the existence of disjoint unions.

    Toby: Also quotient sets and (in a constructive theory) function sets make good axioms; one may want these constructions even if one drops power sets. But for people weaned on ZFC\mathbf{ZFC}'s pairing and union axioms, disjoint unions are particularly important!

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 15th 2011

    There’s a citation in structural set theory to “Benacerraf’s paper”, but no paper (or other reference) is listed.

    • CommentRowNumber10.
    • CommentAuthorDavidRoberts
    • CommentTimeFeb 16th 2011

    I put the reference in.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 16th 2011

    Oops! I forgot to add that reference. Thanks! I also added the other one I intended to add, by McLarty.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2014
    • (edited Apr 1st 2014)

    To the Examples-section at structural set theory I have added the following paragraph:

    Generally, set theory set up in intuitionistic type theory is structural. For instance setoids in extensional type theory or h-sets in homotopy type theory (Rijke-Spitter 13).

    Hope that’s okay. Please fine-tune if not. But I thought some mentioning like this must not be omitted from that page.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeApr 1st 2014

    What do you intend the word “generally” to mean? One can just as well set up a material set theory inside ITT, such as Aczel’s construction of CZF.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2014

    Ah, I see. I have changed it to the following, is that better?

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeApr 2nd 2014

    Sure. Thanks!

    • CommentRowNumber16.
    • CommentAuthorspitters
    • CommentTimeMar 18th 2015

    I had a short discussion on structural set theory today. Tom’s beautiful short paper rethinking set theory seems to be missing. Also, we don’t seem to have local set theory by Bell and Aczel. I am inclined to put all three of them in structural set theory. Any objections to this? I seem to recall that we had a pending discussion on reorganizing the set theory pages.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeMar 18th 2015

    Sounds good.

    • CommentRowNumber18.
    • CommentAuthorspitters
    • CommentTimeMar 11th 2016

    algebraic set theory misses a reference to stack semantics (michaelshulman). Should I just add the “external” link, or is there a better way?

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2016

    external link is fine

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeOct 26th 2017
    • (edited Oct 26th 2017)

    I noticed that structural set theory was not cross-linked with Sets for Mathematics, so I added some.

    Then I noticed that the lead-in paragraphs seemed to be lacking some gentle broad remarks before entering technical detail, so I expanded the first paragraph and added a second (before what is now the third).

    Experts here may want to touch this further. Let’s try to keep in mind a reader with standard mathematics background but otherwise no initiation. Think of your colleague on the other floor. Try to make the entry give him a good idea of why strutural set theory matters.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeOct 27th 2017

    Thanks, this looks pretty good. I tweaked the first paragraph since not all structural set theories (e.g. not SEAR) proceed by axiomatizing functions and the category SetSet.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeOct 27th 2017

    Thanks!

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeOct 27th 2017
    • (edited Oct 27th 2017)

    Now I noticed that the Examples-section never mentioned the word “topos”. I have given each example a section header, and then added some lines containing the term “topos” to the section on ETCS and also a few words to the section on h-sets .

    Would be great if you could fine a minute to fine-tune.

    I would like to have the entry say that the idea of sets in HoTT is very much in the spirit (even if different in technical detail) of ETCS, especiall the spirit of “fixing one base topos and then doing all maths in there”. Maybe this could be said in the entry in some way that feels acceptable.

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2017

    Looks fine, I think.

  25. Corrected small spelling error

    EFinatS

    diff, v26, current

  26. Updated page to talk about distinguishing set theories by if they include families in the theory

    Anonymous

    diff, v27, current

    • CommentRowNumber27.
    • CommentAuthorGuest
    • CommentTimeNov 14th 2022

    This is in contrast to traditional Zermelo-Fraenkel-style “material set theory” where the primitive global set-membership relation “∈\in” forces one to think of all elements of sets as sets themselves, hence of sets-of-sets-of-sets-…, a feature that is almost never actually used or even considered in mathematics, away from the study of material set theory itself.

    This paragraph is just flat out wrong. Any material set theory with non-set urelements such as ZFA is a material set theory which does not force one to think of all elements of sets as sets themselves, as urelements are elements which are not sets. One could interpret Zermelo-Fraenkel-style “material set theory” as referring only to pure set theories, but I don’t think the distinction between pure set theory and non-pure set theories is the right distinction between material and structural set theory.

  28. replaced

    This is in contrast to traditional Zermelo-Fraenkel-style “material set theory” where sets can be elements of other sets, where the primitive global set-membership relation “∈\in” forces one to think of all elements of sets as sets themselves, hence of sets-of-sets-of-sets-…, a feature that is almost never actually used or even considered in mathematics, away from the study of material set theory itself.

    with

    This is in contrast to traditional “material set theory” such as ZFC or ZFA, where sets are characterized by the membership function ∈\in, and where sets can be elements of other sets, hence where there are sequences of sets which are elements of the next set in the sequence, the latter feature which is almost never actually used or even considered in mathematics, away from the study of material set theory itself.

    Anonymous

    diff, v34, current

  29. changed clause

    This is in contrast to traditional “material set theory” such as ZFC or ZFA, where sets are characterized by the membership function ∈\in

    to

    This is in contrast to traditional “material set theory” such as ZFC or ZFA, where sets are characterized by the membership function ∈\in alone

    Anonymous

    diff, v34, current

  30. membership function -> membership relation

    Anonymous

    diff, v34, current

  31. sets are characterized by the membership relation and propositional equality in material set theory.

    Anonymous

    diff, v36, current

  32. Requires uncountably many applications of powerset operation in its proof (result of Friedman)

    Anonymous

    diff, v37, current

    • CommentRowNumber33.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 21st 2022
    • (edited Dec 21st 2022)

    Borel determinacy requires countable-ordinal-iterations of powerset, for arbitrary countable ordinals, which is weaker than uncountably many.

  34. Link code error

    Myvh

    diff, v38, current

1 to 34 of 34

  1.