Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have reorganised set theory and spun off material set theory.
(Between the two pages, nothing has been removed.)
I’ve now removed stale discussions from material set theory. One may view them at the original version.
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 in and in might be considered the same if indexes map both to an element in . 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 to and and map to and then and might be considered the same.
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 and to be considered the same in a way, it’s not an equivalence relation.
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!
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.
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.
Thanks Todd!
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.
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).
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.
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?
It's not so much adding axioms/rules as adding to the language, specifically by adding the universal membership relation . 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 only.)
Structural set theory is elegant too, of course, but in an entirely different way. Since need never be referred to directly in ordinary mathematics, structural set theory is the precise structure needed for mathematical foundations.
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.
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.
The G+ discussion is already moving from philosophical chitchat to precise statements.
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.
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.
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:
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.
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 -groupoid theory” would look like.
It might be worth softening those value judgments at structural set theory.
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.)
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.
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).
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!
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’.
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.
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.
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).
It might be worth softening those value judgments at structural set theory.
In the nLab, we have the -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 ), 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 instead of , 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.
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 is defined as 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 rather than injective functions, and use the same notation for an element of the subset and 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 POV — are the mathematical advantages of structural set theory and type theory to a higher category theorist, such as:
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).
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.
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…”?]
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”).
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.
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.
Are Harvey Friedman and Stephen Simpson at FOM behaving like that? They have in the past.
And Michael Harris, on his unapologetic blog.
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.
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?
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 , 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).
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.
(Also, I’m amused that your comment on that MO thread has more upvotes than the answer itself.)
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).
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 or when and are given as subsets of an ambient set . 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 as the basic sum rule for cardinality of (finite) sets, on a par with as the product. That when and 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 and an equivalence relation , there is a set , called the quotient of modulo such that:
(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’:
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 of people and you wish to record some information about them, then you might want to use a bijection between and (or , since the students were mostly CS majors) for some natural number , then refer to each person by the corresponding number. This well-known idea illustrates the power of isomorphism.
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 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.
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.
Well, perhaps, if you allow a “list” to be uncountable…
@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 ]’ in #45, you should be thinking ‹-place predicate about elements of that respects equality in ›. So given a set and a -place predicate about elements of that respects equality in , you get a subset , such that:
(The latter fact justifies the abuse of notation that the same symbol is used for as an element of as is used for as an element of .)
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.
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 with the countably many -place equality-respecting predicates of natural numbers in the otherwise empty context of a particular language). But it's still true, since
where is any subset of , and
where is any function from to . (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
where is any infinite sequence of subsets of , and
(These are mere curiosities in the course that I was teaching, but I tried to mention something like them.)
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 as both a typing declaration (when is a set and is a new variable) and a proposition (when is a subset of some set and is an element of ). Actually, we abuse a lot of things this way; for example, is normally a proposition, but it's a typing declaration in
Ultimately, you only know which it is based on whether the variable is new or not; in
the meaning depends greatly on which of or (or both) is new. Another abuse of notation is to use the same notation for an element of and for an element of whenever and are materially disjoint (which guarantees that there is no overlap between the notations used for elements of and for elements of 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 for both and ; not only does material set theory not justify this, it forbids it, since (and in a meaningful way, not just by a typing mismatch) when , , and are taken from . (If we properly used 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 and 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.
an element of is an element of such that 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.
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 that the elements satisfy. This is certainly possible for elements in a structural set theory like ETCS. For example, it’s perfectly acceptable to specify a subset as consisting of elements satisfying .
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.
@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.
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.
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 , , , , and outside of appropriate contexts.
It’s frustrating that there doesn’t seem to be a formal system that exactly matches ordinary mathematical practice in this simple regard.
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.
Hmm, that’s an interesting challenge. Here are two specific desiderata; can we reconcile these in a formal system?
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, (and this subscript could possibly be left off), but . 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 , you just write (or even ).
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.
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…
And there are other interesting questions to decide about the behavior of subtyping, such as if and , then do we have and ? Do we have ? We certainly shouldn’t have although some subtyping disciplines do allow such a coercion. But a related question is, if is a quotient of , is ?
And then can be a quotient type of (when ), rather than a supertype. It's just as well that way, since is the secondary concept.
I thought of that too, but then I realized that it’s only true when is injective.
Oh, right, it fails when and are empty but is not (and can fail in additional cases constructively.) I meant to check that but must have forgotten.
I think there are other problems with allowing the elements of a quotient to be elements of the original set. For instance, suppose and we have . How do we prevent the substitution law of equality from allowing us to conclude ?
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 when and are given as subsets of some ambient set , then what is it that justifies our considering (in order to be “given” them) the statements and , unless they are a sort of “typing judgment” with a different status?
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).
Sounds like a category with types with* as objects and embeddings as arrows.
*edited
What?
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.
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.
I think there are other problems with allowing the elements of a quotient to be elements of the original set. For instance, suppose and we have . How do we prevent the substitution law of equality from allowing us to conclude ?
Back in #49, I wrote things like
a -place predicate about elements of that respects equality in
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 to distinguish this from ). But clearly that was in the back of my mind somewhere.
Anyway, the substitution rule of equality does not allow you to conclude from for any -place predicate about elements of , but only for a predicate that respects equality in . Which is hardly even a rule, since the validity of this conclusion is what it means for to respect equality in . (An example of a predicate about rational numbers that does not respect equality is ‹has an odd numerator›. Note that is a subquotient of , 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.
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 when and are given as subsets of some ambient set , then what is it that justifies our considering (in order to be “given” them) the statements and , unless they are a sort of “typing judgment” with a different status?
Right, if does double duty as (the judgement that the term is an element of the set ) and as (the proposition that the element of the set belongs to the subset of ), so also does double duty as (the judgement that the term is a subset of the set ) and as (the proposition that the subset of the set is contained in the subset of ). Somewhere around here, there's a discussion where somebody introduced (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 is a term that has appeared before in the context and whose type you already know, then should be the proposition (and you should also already know the type of and it should be the case that is an element of some set and that is a subset of ). On the other hand, if is a new variable, then serves to enrich the context with a new variable for an element of the set (and you should already know the type of and it should be the case that is a set). Similar remarks apply to . It gets trickier when 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 (rather than or ).
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.
Treating as a subtype of as a subtype of as a subtype of (and treating , 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 .
This actually has a different answer in each context:
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 ‘’ without specifying what system this is taken from.
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.
How about this as a basic framework?
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).
Looks nice, but I can’t make any mathematically informed comments/criticism.
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.
@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.
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 as a type, with and merely sets (subsets of, in this case, ), while fancier sets such as and must be constructed from (and so are also types). But in my Discrete Math courses from a decade ago, the only primitive type would have been , which everything else constructed from that.
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 as a type, with and merely sets (subsets of, in this case, ), while fancier sets such as and must be constructed from (and so are also types). But in my Discrete Math courses from a decade ago, the only primitive type would have been , 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 , 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.
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 , 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.
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).
I added a mention of the axiom of extensionality.
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 so that given , means .
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.
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.
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.
1 to 91 of 91