You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
John Baez (May 07 2024 at 07:46):In September, Tom Leinster will teach a course on set theory at the University of Edinburgh. He'll be doing something new: instead of explaining ZFC, he'll explain [[ETCS]], Lawvere's Elementary Theory of the Category of Sets. But he won't talk about categories, since he's found that it's possible to state the axioms and work with them without first explaining any general concepts from category theory! Anyone interested can get a taste of this in his paper:
but he will be creating course notes with a much more detailed treatment, and make these available.
John Baez (May 07 2024 at 07:49):Lacking the [[axiom of replacement]], ETCS is weak enough that it can't define the cardinal
which is called "beth omega", .
John Baez (May 07 2024 at 07:51):It also can't prove the Borel determinacy theorem. But it's strong enough to do most commonly used mathematics.
John Baez (May 07 2024 at 07:54):On a side note, Tom Leinster also plans to work with 4 coauthors to write an introductory article on the theory of magnitude, which he helped originate.
Amar Hadzihasanovic (May 07 2024 at 07:59):So is this the “our work” thread on Tom by proxy? :)
Exciting news though!
David Michael Roberts (May 07 2024 at 08:44):Will the notes be made available as the course covers the material? Or before/after the course?
David Michael Roberts (May 07 2024 at 08:50):It should be noted the ETCS can "almost" prove Borel Determinacy: adding the axiom that inductive constructions of sets along countable well-orderings exist gets you there (and, incidentally, also proves beth_omega exists). Much weaker than ZFC, still :-)
Mike Shulman (May 07 2024 at 15:03):I also think it's a bit misleading to put too much attention on the weakness of ETCS vs ZFC. There's nothing intrinsic to the two theories that means one has to be weaker than the other: it's easy to write down ETCS-style theories that are as strong as ZFC, and ZFC-style theories that are as weak as ETCS. In fact, Lawvere already did the former in his original paper on ETCS, and I kind of wish he'd given that stronger theory the name "ETCS" instead -- then we would be able to say simply "ETCS is equivalent to ZFC" and focus attention on the important differences.
John Baez (May 07 2024 at 19:45):David Michael Roberts said:
Will the notes be made available as the course covers the material? Or before/after the course?
I seem to recall Tom made his Galois theory notes available as he wrote them, while teaching that course. So I'm guessing he'll do the same for set theory.
It should be noted the ETCS can "almost" prove Borel Determinacy: adding the axiom that inductive constructions of sets along countable well-orderings exist gets you there (and, incidentally, also proves beth_omega exists). Much weaker than ZFC, still :-)
Yes, Tom pointed that out. And I think he'd agree with Mike's point, that the really interesting thing is not these differences in strength but how you can teach ETCS in a less technical, more 'human' way than ZFC because it's a structural set theory. He'll be teaching an introduction to set theory, not an advanced course.
Patrick Nicodemus (May 07 2024 at 20:12):Reactions to an earthquake
Perhaps you will wake up tomorrow, check your email, and find an announcement that ZFC is inconsistent. Apparently, someone has taken the ZFC axioms, performed a long string of logical deductions, and arrived at a contradiction. The work has been checked and re-checked. There is no longer any doubt. How would you react? In particular, how would you feel about the implications for your own work? All your theorems would still be true under ZFC, but so too would their negations. Would you conclude that your life’s work had been destroyed?
I believe that most of us would be interested but not deeply troubled. We would go on believing that our theorems were true in a sense that their negations were not. We are unlikely to feel threatened by the inconsistency of axioms to
which we never referred anyway. In contrast, the ten axioms above are such core mathematical principles that an inconsistency in them would be devastating. If we cannot safely assume that composition of functions is associative, or that repeatedly applying a function f : X −→ X to an element a ∈ X produces a sequence (f n(a)), we are really in trouble.
I really don't like this because I feel that he's pulling a sleight of hand by saying that "material" set theory is too strong while "structural" set theory is self-evidently correct and is inconsistent only if our most basic and fundamental conceptions of mathematical reasoning are wrong. As Michael Shulman says one could have untyped set theories equivalent in strength to ETCS. It is clearly an orthogonal issue, this is simply not an argument for "structural" set theory in any sense and has no place in the paper.
Reverse mathematics has classified a huge amount of mathematics into the weakest fragment of second order arithmetic necessary to prove it, why doesn't Tom advocate second order arithmetic or Zermelo set theory?
Frankly I'm inclined to believe that Tom is deluding himself when he suggests that the axioms of ETCS are "such core mathematical principles that an inconsistency in them would be devastating" and the axioms of, say, Zermelo set theory are not. I mean, topos theory and any set theory with powerset is still impredicative in the early sense of the word that Russell used (not in the sense of System F polymorphism or something)
Mike Shulman (May 07 2024 at 21:16):You didn't quote the next paragraph of the article:
As the weaker system, the ten axioms are less likely to be inconsistent than ZFC. But the question of strength is peripheral to this article (and in any case, if one wants a system of equal strength to ZFC, all one needs to do is add the aforementioned eleventh axiom). The real message is this: simply by writing down a few mundane, uncontroversial statements about sets and functions, we arrive at an axiomatization that reflects how sets are used in everyday mathematics.
Mike Shulman (May 07 2024 at 21:18):That seems to me to be saying the same thing you are, that the question of strength is an orthogonal issue.
Patrick Nicodemus (May 07 2024 at 23:23):John Baez said:
the really interesting thing is not these differences in strength but how you can teach ETCS in a less technical, more 'human' way than ZFC because it's a structural set theory. He'll be teaching an introduction to set theory, not an advanced course.
I don't buy this. It is not easier to teach ETCS informally than it is to teach ZFC informally (which we can just call "naive set theory with handwaving about proper classes"). We can teach a formalism informally with the emphasis being on using it and showing how to practically carry out deductions in a way compatible with the framework, allowing students to build intuition for when an argument can and cannot be carried out in the formalism and learning to use it as a mental frame of reference for what is a rigorous argument. Or we can teach a formalism more formally with the goals being to show students that there are objective standards for rigorous mathematical proof that can be checked in a mechanical, algorithmic way, and that this formalism is in fact adequate to express these arguments, and allowing them to actually see that mathematics can be translated into the formalism, rather sketching it.
Both ETCS and ZFC are equally suitable for either of these approaches. I do not believe that it is easier to informally present ETCS than informally present ZFC.
Honestly I'm not sure what the formalism is that he will present to the students because ETCS is a first order theory and he uses language suggestive of first order dependent type theory.
Patrick Nicodemus (May 07 2024 at 23:34):Mike Shulman said:
That seems to me to be saying the same thing you are, that the question of strength is an orthogonal issue.
What he says is that one can strengthen ETCS to be equivalent to ZFC, not that one can weaken ZFC to be equivalent to ETCS. This is stated as a virtue of ETCS because its basic framework is sufficiently strong for most mathematics while being extensible with additional axioms for the mathematics that requires it.
If the intended reading was that strength was an orthogonal issue, I stress that there would be no reason to include this section in the paper. The implication is that material set theory axioms are weird, cryptic and esoteric, so that an inconsistency in ZFC would be unlikely to imply problems in our basic conceptions of mathematical reasoning, it is just formal symbol soup disconnected from mathematical reasoning and so an inconsistency would probably be unproblematic. On the other hand structural set theory directly reflects how mathematicians think and is necessarily much more likely to be consistent.
Patrick Nicodemus (May 07 2024 at 23:44):It is certainly not the case that the axioms of ETCS are mundane or uncontroversial relative to those of ZFC. Most axioms of ZFC are mundane, two controversial axioms of ZFC (powerset and choice) are reflected in ETCS, that leaves only replacement as the controversial axiom of ZFC to which he would be inferring, and this is certainly at least as innocuous as powerset - if a set X exists, and there is a function f defined on X, then the image of f(X) also exists.
Mike Shulman (May 07 2024 at 23:58):This is an argument that has been done to death in many other places and I have no interest in having it again here. Suffice it to say that one person's "mundane" is another person's "controversial".
Patrick Nicodemus (May 08 2024 at 00:08):Sure. Suffice it to say I choose not to charitably interpret his writing to say less hyperbolic and controversial things than he actually says. I don't extend goodwill in interpretation to people who consistently push the envelope with overstated rhetoric.
https://golem.ph.utexas.edu/category/2021/07/borel_determinacy_does_not_require_replacement.html
Patrick Nicodemus (May 08 2024 at 00:10):"Zorn's Lemma has nothing to do with the axiom of choice"
"Sheaves have nothing to do with algebraic geometry"
"Borel determinacy does not require replacement"
Etc. etc.
Mike Shulman (May 08 2024 at 00:21):I always try to try to interpret everyone's writing as charitably as possible.
David Michael Roberts (May 08 2024 at 02:11):I just wanted to point out that when John says ETCS is weaker, it's not that it's massively weaker. By "most commonly used mathematics" it really is more like "all but a small amount of mathematics that people do, mostly in descriptive set theory, or outright axiomatic set theory where people are studying ZFC itself". I don't worry too much about it, and I'm happy to work in, but also critically examine, pretty much any foundational system.
That Lawvere gave a system equivalent in strength to ZFC in his original paper is not something I'd realised, however, so that's good to know.
James Hanson (May 08 2024 at 02:34):This has probably been pointed out before but I suspect that Leinster's statement on page 7 of Rethinking set theory that ETCS + replacement is biinterpretable with ZFC isn't correct, but for fairly subtle reasons involving weak forms of global choice that are provable in ZFC. There is a definable function in ZFC that takes an arbitrary set and produces a linear order and a surjection . I heavily doubt this is possible in ETCS + replacement.
The difference is a lot easier to establish between ETCS - choice + replacement and ZF, since ETCS - choice + replacement is more directly comparable to ZFA with a possibly proper class of atoms. ZF proves that every group is the automorphism group of a graph, but ZFA does not, for instance.
They are definitely mutually interpretable, which is the more salient point, but I thought I should mention this.
Mike Shulman (May 08 2024 at 03:18):What's true is that (1) you can construct a model of ZFC from a model of ETCS+R, (2) you can construct a model of ETCS+R from a model of ZFC, (3) the composite ZFC -> ETCS+R -> ZFC gives you a model isomorphic to the one you started from, and (3) the composite ETCS+R -> ZFC -> ETCS+R gives you a model equivalent, as a category, to the one you started from. This probably isn't what a model theorist means by "biinterpretable" because they are thinking only about models as structured sets, but it's obviously the correct notion when you have a theory like ETCS whose models are structured categories.
Mike Shulman (May 08 2024 at 03:21):(Also, for anyone listening who isn't conversant with the lingo, as I wasn't until fairly recently, "biinterpretable" is apparently used to mean not only that each can be interpreted in the other, which would be the naive meaning of that word but apparently is officially called instead "mutually interpretable", but rather that the composites of the two interpretation functions are the identity -- usually up to isomorphism, but in the case of categories it should be up to equivalence.)
Mike Shulman (May 08 2024 at 03:25):David Michael Roberts said:
That Lawvere gave a system equivalent in strength to ZFC in his original paper is not something I'd realised, however, so that's good to know.
Unfortunately, Lawvere's "replacement axiom" (which is actually more of a reflection axiom, if memory serves) is not, I think, good for much directly except establishing the equivalence to ZFC. In particular, it doesn't seem to weaken gracefully in the absence of choice or excluded middle. However, in the presence of choice and excluded middle, it's equivalent to the various other replacement/collection axioms that have been proposed (by Osius, Cole, McLarty, and myself), some of which are more directly useful. (My paper Comparing material and structural set theories discusses these axioms in sections 7 and 9.)
James Hanson (May 08 2024 at 03:26):Mike Shulman said:
(Also, for anyone listening who isn't conversant with the lingo, as I wasn't until fairly recently, "biinterpretable" is apparently used to mean not only that each can be interpreted in the other, which would be the naive meaning of that word but apparently is officially called instead "mutually interpretable", but rather that the composites of the two interpretation functions are the identity -- usually up to isomorphism, but in the case of categories it should be up to equivalence.)
That's not the definition of biinterpretability.
image.png
James Hanson (May 08 2024 at 03:27):(This is from Hodges' Model Theory.)
Mike Shulman (May 08 2024 at 03:30):Looks pretty much like it to me.
Mike Shulman (May 08 2024 at 03:30):It seems to me he's basically just saying that the isomorphisms on each side have to be definable.
James Hanson (May 08 2024 at 03:33):Okay but this is the kind of nuance that I think should be mention in an academic paper. Biinterpretable is a word with an established technical definition.
Mike Shulman (May 08 2024 at 03:38):Yes, probably Leinster shouldn't have used that word. But I think it's an easy mistake to make, for a non-model-theorist, to assume that the meaning of that word is what one would expect it to be, rather than what the model theorists have defined it as. (-:O
Mike Shulman (May 08 2024 at 03:40):Also, I would conjecture that ETCS+R and ZFC are bi-interpretable if the official model-theory definition of that word is extended in a natural way to theories whose models are categories rather than sets.
Mike Shulman (May 08 2024 at 03:41):I don't know if anyone has written this down in technical language that would satisfy a model theorist, but it seems evident to me from the explicit mutually inverse constructions that they, and the isomorphism and equivalence on either side, are as definable as you could hope for.
James Hanson (May 08 2024 at 03:41):But ZFC isn't a theory whose models are categories.
Mike Shulman (May 08 2024 at 03:42):Yes they are, they are discrete categories. (-:O
James Hanson (May 08 2024 at 03:42):I don't understand your meaning. Are you just saying that the models are sets?
James Hanson (May 08 2024 at 03:42):Under that interpretation, I would think your conjecture doesn't really make sense, does it?
Mike Shulman (May 08 2024 at 03:44):Yes, they are sets, which can be regarded as discrete categories. What doesn't make sense about it?
James Hanson (May 08 2024 at 03:45):How could a discrete category be equivalent to a non-discrete category?
Mike Shulman (May 08 2024 at 03:46):That's not the claim. The claim is that if you take a model of ZFC, which is a discrete category, make it into a model of ETCS+R, which is a non-discrete category, and then make that back into a model of ZFC, which is another discrete category, what you get is equivalent, i.e. isomorphic, to the original discrete category.
Mike Shulman (May 08 2024 at 03:46):And on the other side.
Mike Shulman (May 08 2024 at 03:46):You never ask whether a model of one theory is isomorphic (or equivalent) to a model of a different theory!
James Hanson (May 08 2024 at 03:47):That should already be true in the normal model-theoretic sense. The point is that the interpretation of ETCS+R in ZFC isn't conservative over ETCS+R.
Mike Shulman (May 08 2024 at 03:48):What's not true in the normal model theoretic sense is the other side. If you start with a model of ETCS+R, which is a non-discrete category, make it into a model of ZFC, which is a discrete category, and then make it back into a model of ETCS+R, which is a non-discrete category, what you get is equivalent, but not isomorphic, to the original non-discrete category. So the theories aren't bi-interpretable in the normal model-theoretic sense, but they should be in an expanded categorical sense.
James Hanson (May 08 2024 at 03:51):I agree that that should be true, although this is in some sense relying on choice, right?
Mike Shulman (May 08 2024 at 03:55):Yes, indeed! When you remove choice and other axioms, mutual interpretability is retained, but not bi-interpretability. There's some general discussion of the conditions you need to get equivalences on both sides in section 9 of my paper.
James Hanson (May 08 2024 at 03:57):I'm also guess that mutual interpretability even works constructively with IZF. Is that right?
Mike Shulman (May 08 2024 at 04:14):Yes, IZF is mutually interpretable with "IETCS+Collection".
Mike Shulman (May 08 2024 at 04:14):For a suitable category-theoretic collection axiom.
Mike Shulman (May 08 2024 at 04:17):By the way, another thing I wanted to respond to:
David Michael Roberts said:
By "most commonly used mathematics" it really is more like "all but a small amount of mathematics that people do, mostly in descriptive set theory, or outright axiomatic set theory where people are studying ZFC itself".
What about in category theory where we use Grothendieck universes?
David Michael Roberts (May 08 2024 at 05:59):So after Kevin Buzzard kept talking about "normal mathematics", to exclude a) set theorists and b) category theorists, I coined the phrase "generic mathematics", which I think is better.
So does ETCS+universes give you something as strong as ZFC? I think of universes as large cardinal axioms (or, as Grothendieck did, according to McLarty, as merely a technical convenience but not really important), not as giving strong recursion principles or Replacement-like constructions.
Mike Shulman (May 08 2024 at 06:10):Well, in terms of proof-theoretic strength, one inaccessible cardinal is much stronger than the replacement schema. In particular, the sets in a Grothendieck universe are a model of ZFC, with replacement, even if the ambient set theory in which the universes exist doesn't satisfy replacement.
Mike Shulman (May 08 2024 at 06:11):Replacement is kind of like a "small" large cardinal axiom. For instance, it implies the existence of all the beths and lots of other cardinals that you can't construct in ETCS or BZC.
Mike Shulman (May 08 2024 at 06:11):I don't remember offhand whether adding an axiom like "every set is contained in a Grothendieck universe" to BZC directly implies the replacement schema.
David Michael Roberts (May 08 2024 at 07:28):I didn't say Grothendieck universe. If you're in ETCS, then you aren't looking at Grothendieck universes, strictly speaking, but some kind of structural analogue, no? I can imagine that you could have a hierarchy of universes that give larger and larger models of ETCS without getting to the strength of ZFC.
David Michael Roberts (May 08 2024 at 07:30):However, I notice that Zhen Lin Low points out in Universes for category theory that even working in eg Mac Lane set theory, a universe models ZFC. So I guess my intuition was slightly off. Though that's still on the material side, and not a structural definition of universe, tailored to ETCS.
John Baez (May 08 2024 at 08:38):Patrick Nicodemus said:
John Baez said:
the really interesting thing is not these differences in strength but how you can teach ETCS in a less technical, more 'human' way than ZFC because it's a structural set theory. He'll be teaching an introduction to set theory, not an advanced course.
I don't buy this. It is not easier to teach ETCS informally than it is to teach ZFC informally (which we can just call "naive set theory with handwaving about proper classes").
Leinster will be teaching ETCS rigorously without handwaving, the way you'd teach any upper-level pure math course. His students will learn the axioms of ETCS and presumably do homework proving theorems from these axioms. Naive set theory with handwaving is not ZFC. As for what's easy to teach, the right way to test theories about that is to teach courses and see what happens, so that's what Tom will do.
John Baez (May 08 2024 at 09:03):James Hanson said:
How could a discrete category be equivalent to a non-discrete category?
For example the category with two uniquely isomorphic objects is not discrete, but it's equivalent to the discrete category with one object.
James Hanson (May 08 2024 at 12:05):Mike Shulman said:
I don't remember offhand whether adding an axiom like "every set is contained in a Grothendieck universe" to BZC directly implies the replacement schema.
No it won't. If there are infinitely many inaccessible cardinals, then where is the supremum of the first countably many inaccessibles will be a model of ZC + "every set is contained in a Grothendieck universe" but not replacement.
Matteo Capucci (he/him) (May 08 2024 at 12:10):<mod> Please let's keep the conversation cordial, James </mod>
Mike Shulman (May 08 2024 at 16:22):David Michael Roberts said:
If you're in ETCS, then you aren't looking at Grothendieck universes, strictly speaking, but some kind of structural analogue, no?
Yes, but the analogue should be equivalent, and of equivalent strength. All the important properties of a Grothendieck universe are structural properties of the corresponding notion of "small set". I don't know whether anyone has written it down, but I would expect that given a model of ETCS containing a universe, the submodel of small sets satisfies ETCS+R.
David Michael Roberts (May 08 2024 at 20:57):@Mike Shulman then how to square that with James' comment?
Mike Shulman (May 08 2024 at 23:14):Which comment? I don't see a contradiction.
David Michael Roberts (May 09 2024 at 04:53):I mean you can have a model of
ZC + "every set is contained in a Grothendieck universe" but not replacement
David Michael Roberts (May 09 2024 at 04:56):But then I guess that each Grothendieck universe inside that model is a model of ZFC? I guess that must be it
Mike Shulman (May 09 2024 at 05:51):Right: a model of ZC can contain models of ZFC without itself being a model of ZFC, and similarly a model of ETCS can contain models of ETCS+R without itself being one.
Morgan Rogers (he/him) (May 09 2024 at 09:38):Patrick Nicodemus said:
"Zorn's Lemma has nothing to do with the axiom of choice"
"Sheaves have nothing to do with algebraic geometry"
"Borel determinacy does not require replacement"
Etc. etc.
Only the last of these quotes appears in the n-cat-cafe post you linked and he fully justifies it: a much weaker principle than the axiom of replacement suffices.
The first quote should read "Zorn’s lemma has almost nothing to do with the axiom of choice"; the "almost" does a lot of work there, but the thrust of the post is that Zorn's Lemma is a result about posets and there is a theorem about posets very close in content to Zorn's lemma that does not require choice, but from which Zorn's Lemma can be recovered with a simple application of choice; I think it's a sensible thing to point out.
The second should read "Sheaves Do Not Belong to Algebraic Geometry", which is an entirely uncontroversial statement to me, a topos theorist studying sheaves which rarely relate to algebraic geometry.
@Patrick Nicodemus criticising a person's writing style is one thing, but misquoting them (deliberately or otherwise) as a basis for criticism is not okay, please be more careful in future.
Patrick Nicodemus (May 09 2024 at 10:17):Sorry, I misremembered the title of the sheaf theory post. Yes, "Sheaves do not belong to algebraic geometry" is much less controversial.
Patrick Nicodemus (May 09 2024 at 10:21):Unfortunately the whiny metaphor with the endless buffet and the selective naming of a handful of set theorists to pick on for misrepresenting the subject pissed off a lot of set theorists who probably still haven't forgiven him and he hasn't apologized either so what are you going to do.
Patrick Nicodemus (May 09 2024 at 10:46):Leinster doesn't actually care that "all beth numbers exist" is weaker than replacement. A better title for the blog post would have been something like "ETCS + an additional axiom can prove borel determinacy." The real point of the blog post is that people assume since Borel determinacy requires replacement, it is unprovable in an ETCS like theory where it is not clear how to state and assume the replacement axiom, whereas it is clear how to state "all beth numbers exist."
If "all beth numbers exist" was stronger than replacement and also sufficed to prove borel determinacy he would have written a blog post with the same technical content but without all the drama about how set theorists are lying to us about Borel determinacy (here I am employing hyperbole and not directly quoting him)
Morgan Rogers (he/him) (May 09 2024 at 11:21):Patrick Nicodemus said:
A better title for the blog post would have been something like "ETCS + an additional axiom can prove borel determinacy."
That sounds like a pretty bad title for a blog post, to be honest. Having read the blog post in question, I don't see how the title is misleading. While I agree that the buffet metaphor is a little heavy-handed, I don't know where your scepticism is coming from here. I also don't really see what Tom should be apologizing for: he quoted several people using imprecise language in discussing the relationship between Borel determinacy and the axiom of replacement, explains clearly what the imprecision is and then goes on to show that the stronger result is 'known'. Are you saying that Tom's quotes are taken out of context / mischaracterize the discussion of the relationship between replacement and Borel determinacy?
Mike Shulman (May 09 2024 at 15:48):Leinster doesn't actually care that "all beth numbers exist" is weaker than replacement.
I don't think this is true. Directly after recalling the "all beths exist" axiom, he says that "The axiom that all beths exist is vastly weaker than the axiom scheme of replacement." And later he says
In summary, it seems to be common for people... to state explicitly that replacement is required or necessary or essential to prove Borel determinacy... while fully aware that only a minuscule fragment of replacement is, in fact, needed. [emphasis added]
He doesn't say anything about ETCS until the last couple of paragraphs of the post, where again he says
For those of us whose favourite set theory is ETCS, replacement is just one of many possible axioms with which one could supplement the core system. There are many others. “All beths exist” is one of them — a far weaker one — which is perfectly natural and perfect for the job at hand. [emphasis added]
I don't think I agree with Leinster that "reflexively reaching for replacement just isn’t such a temptation in categorical set theory," but the fact that "all beths exist" is weaker than replacement is essential to his argument for it.
I also don't think that this is true:
The real point of the blog post is that people assume since Borel determinacy requires replacement, it is unprovable in an ETCS like theory where it is not clear how to state and assume the replacement axiom, whereas it is clear how to state "all beth numbers exist."
Leinster doesn't say anything in that post about the statement of replacement in ETCS, whereas five days earlier he had written
I think there’s a lingering impression that replacement is somehow borrowed from ZFC... I’ll explain why this is a misconception, stating replacement in a way that’s entirely natural from a structural/categorical perspective.
Mike Shulman (May 09 2024 at 15:57):That said, I can definitely understand why some of the people quoted in that post would be cranky with him. I would probably have been cranky too if I were in that situation. I haven't read the original sources to see to what extent they were taken out of context, but I expect that nearly all of them were intended to be read in the context of the ZFC axioms, so that e.g. "Borel determinacy cannot be proved without replacement" would clearly be intended and read as "Borel determinacy cannot be proved using only the ZFC axioms other than replacement", which is, I think unobjectionable. (The only exception to this is the one quote that Leinster calls "factually incorrect" which claims that Borel determinacy requires the "full potency" of replacement.) I guess Leinster's claim is that one shouldn't just fix the ZFC axioms and ask which of them are needed for some result instead of considering alternative axioms, but I don't think it's fair to criticize people who were doing that as if their statements in that context were misleading or wrong.
Mike Shulman (May 09 2024 at 16:08):But that said, I think it's good to be forgiving. The permanence and publicness of the Internet, plus its apparently quick and informal nature, makes it too easy to make minor mistakes that end up annoying people in unexpected ways and haunting you for a long time afterwards. I've certainly made that mistake often enough myself.
James E Hanson (May 09 2024 at 16:17):I know that I should be trying to interpret everyone's writing as charitably as possible, but, I have to be honest, I find a lot of Leinster's rhetoric about set theory to be hostile and not that academically honest.
For instance, in Rethinking set theory on page 2 he cites the axiom of foundation as odd, without putting any effort into explaining why it's valuable to set theorists. Admittedly it's often presented in an oddly terse way, but it's an induction principle. Mathematicians love induction. Furthermore, he says
Because of the categorical origins of this axiomatization, three misconceptions commonly
arise.
The first is that the underlying motive is to replace set theory with category theory. It is not. The approach described here is not a rival to set theory: it is set theory.
I don't really see how to square this with the fact that so much of the technology and intuition set theorists have makes good use of the iterative concept of sets. To me this feels like he's trying to claim that his presentation of set theory captures the 'objective content' of set theory (to quote Lawvere) while what set theorists are doing is unnatural or artificial.
Mike Shulman (May 09 2024 at 16:22):I think the problem is that the word "set" is used very differently by set theorists and by most mathematicians. In nearly all of mathematics, while there may be lip service to ZFC for historical reasons, the way sets are used is equally consonant with ETCS as with ZFC, and so ETCS is "set theory" in the obvious naive sense of "a theory of sets" where "set" has the effective meaning that it has in nearly all of mathematics. In other words, if an alien arrived on Earth and learned all of mathematics except the part that generally goes by the name "set theory", and then learned ETCS, they would say "yes, of course this is set theory". The reason that "set theory" generally refers to iterative-conception sets only is purely historical.
Mike Shulman (May 09 2024 at 16:26):One can reasonably argue that we should nevetheless respect history and restrict "set theory" to refer only to iterative-conception sets, but it does become somewhat awkward to talk about "the theory of ETCS-like theories". I think Leinster does have a good point that calling it "categorial set theory" is misleading because it suggests that there is a necessary connection with category theory. (I myself tried to combat this implication by formulating [[SEAR]].) Some of us use "structural set theory" instead, but this has its own problems. And either of them still includes the phrase "set theory", which seems to support Leinster's claim that ETCS is a kind of set theory. Can you think of a better term?
Mike Shulman (May 09 2024 at 16:28):And there is also the fact, discussed above, that ETCS+R is equivalent to ZFC. So how can we say that the phrase "set theory" applies to ZFC and not to the equivalent theory ETCS+R? Wouldn't that be like saying that it's not "category theory" any more if you use the single-sorted definition of category?
James E Hanson (May 09 2024 at 16:29):Sure, but my reading of Leinster's rhetoric is that he doesn't think there's any particular good reason set theory research is done in material set theories. Near the end, he says
A second disadvantage is that any student planning a career in set theory
will need to learn ZFC anyway, since almost all research-level set theory is done with the iterated-
membership conception of set. (That is the current reality, which is not to say that set theory
must be done this way.)
He doesn't actually address any potential reason why ETCS might be a bad framework for doing metamathematical set theory work. He's just leaving open the implication that maybe there's no good reason set theorists do set theory the way they do set theory.
One of the first major results in set-theoretic metamathematics, Gödel's proof the relative consistency of choice and the generalized continuum hypothesis, is something that is pretty natural in material set theory and pretty painful in other contexts (like when one has to try to miniaturize to second-order arithmetic).
James E Hanson (May 09 2024 at 16:30):To be clear, as someone who literally has a paper on a non-well-founded set theory, I don't think the phrase 'set theory' should exclusively refer to ZF-like set theories.
Mike Shulman (May 09 2024 at 16:32):Indeed, and I think this example is one that should be better-known and studied by structural set theorists. I suspect there is a better categorical understanding of out there waiting to be found. But I certainly admit it may never be as natural as the material approach.
However, there are other set-theoretic constructions, like forcing, that I think can be argued to be more natural from the structural point of view. Nearly always in mathematics when we find two equivalent ways of defining the same thing, it happens that each of them has their uses, and we should know both of them and pick the appropriate one for whatever we're doing. I don't see why that shouldn't apply to ZFC and ETCS.
James E Hanson (May 09 2024 at 17:22):Has anyone written down a presentation of the forcing poset presentation of forcing in ETCS (or toposes, for that matter). I know that people say that the Boolean-valued approach is the 'correct' approach, but a lot of set theorists find forcing posets to be a more practical hands-on way of actually working with forcing extensions. I'm asking this because this should in principle be orthogonal to the choice of structural or material perspective. Also, forcing in model theory and computability theory is in my opinion far easier to conceptualize in terms of forcing posets.
Mike Shulman (May 09 2024 at 17:24):I'm not sure exactly what you mean by "the forcing poset presentation", but perhaps it is [[Kripke-Joyal semantics]]?
Mike Shulman (May 09 2024 at 17:52):But in any case, I don't think one should fault Leinster for not delving into this question in his paper, which after all isn't about research in set theory, but about the use of set theory by ordinary mathematicians and the way we teach it to undergraduates. Going into a lot of detail about set-theoretic research wouldn't have been a good use of space and would have diluted the primary message.
And I don't think it's wrong to say that research in set theory doesn't have to be done with ZFC. The fact that ETCS+R is equivalent to ZFC means that research in set theory could be done with ETCS+R instead. Yes, arguably it would be more awkward, some parts more than others. But I don't think anyone has really seriously tried to develop large swaths of research-level set theory in ETCS, so it's hard for me to be confident in knowing exactly how awkward it would be. Certainly current set theorists find ZFC easier; but how much of that is intrinsic, and how much of that is just that it's what they're used to and what all the literature uses? I don't think we can really say. And I think it's entirely possible that some parts of it would be more convenient or natural that way, whether or not forcing is such an example.
James E Hanson (May 09 2024 at 17:54):Set theorists who do forcing in ZFC usually present forcing in one of two ways. As presented in Jech, there's the Boolean-valued model approach, which is morally analogous to sheaves on a complete Boolean algebra, and as presented in Kunen, there's the forcing poset approach. In the context of the dense topology classical set theorists typically implicitly use, these are equivalent in the sense that what you're 'really doing' is working in the Boolean locale of regular open subsets of the poset's order topology, or something like that, but I, and a lot of set theorists, find that it gives a more focused framework for thinking about the generic object you're building, since you only need to consider forcing conditions of a relatively simple form, and checking for density of various conditions is pretty conceptually straightforward.
In computability theory in particular this is important, especially when you think about priority arguments, which are ostensibly a generalization of this kind of forcing in the context of computable mathematics.
James E Hanson (May 09 2024 at 18:23):Mike Shulman said:
But in any case, I don't think one should fault Leinster for not delving into this question in his paper, which after all isn't about research in set theory, but about the use of set theory by ordinary mathematicians and the way we teach it to undergraduates. Going into a lot of detail about set-theoretic research wouldn't have been a good use of space and would have diluted the primary message.
My problem with this is that the kind of rhetoric Leinster is employing (e.g., what I would consider to be tired, shallow criticisms of ZFC like 'isn't the axiom of foundation weird' or highlighting junk theorems in ZFC as a sign of how irrelevant it is to normal mathematics) is pretty close to the kind of 'set theorists aren't real mathematicians' rhetoric that Kevin Buzzard uses or the 'set theory is obsolete and weird' rhetoric Saunders Mac Lane used. Set theory research is struggling in the US and I feel like this is in no small part because most mathematicians are convinced that set theory has nothing to do with what they do, despite the fact that category theory uses large cardinals all the time, type theorists use set-theoretic relative consistency results often, and, frankly, nobody else seems to be nearly as good at things like identifying when results are probably going to be independent of relatively strong foundational theories, building strong failures of choice in classical contexts, or knowing when appeals to choice can be automatically removed from arguments via results like Shoenfield absoluteness.
Mike Shulman (May 09 2024 at 18:59):So does "the forcing poset approach" just mean using the poset itself as a [[site]] to take sheaves on rather than "completing" it to some kind of locale?
James E Hanson (May 09 2024 at 19:02):Mike Shulman said:
So does "the forcing poset approach" just mean using the poset itself as a [[site]] to take sheaves on rather than "completing" it to some kind of locale?
I'm not sure because there isn't an explicit covering relation, but probably?
Mike Shulman (May 09 2024 at 19:02):The covering relation is the [[double-negation topology]].
Mike Shulman (May 09 2024 at 19:03):(Which you're kind of forced to use, no pun intended, if you want to get a Boolean sheaf topos.)
Mike Shulman (May 09 2024 at 19:14):James Hanson said:
My problem with this is that the kind of rhetoric Leinster is employing (e.g., what I would consider to be tired, shallow criticisms of ZFC like 'isn't the axiom of foundation weird' or highlighting junk theorems in ZFC as a sign of how irrelevant it is to normal mathematics) is pretty close to the kind of 'set theorists aren't real mathematicians' rhetoric that Kevin Buzzard uses or the 'set theory is obsolete and weird' rhetoric Saunders Mac Lane used.
I can see how it might feel similar to a ZFC-theorist, but I think there's an important difference. It seems to me that Leinster is interested in set theory research and does think it's valuable. For instance, he wrote a whole 12-part blog series about large cardinals. He just wants to explore to what extent those same results can be stated and proven in the equivalent language of ETCS instead of ZFC, to make them seem more relevant and accessible to mathematicians.
I don't know anything about the situation of set theory research in the U.S., but personally speaking, I tend to get turned off when set theorists insist that the phrase "set theory" can only refer to ZFC, that propositions-as-types is incoherent, or that it is meaningful to ask whether the continuum hypothesis is "true". Maybe some more openness to rephrasing set theory in language that's closer to what most mathematicians use would be a good public relations move.
James E Hanson (May 09 2024 at 19:16):I'm curious about the 'propositions-as-types is incoherent' comment. Are you referring to a specific incident?
James E Hanson (May 09 2024 at 19:19):(If you think it's appropriate to be more specific.)
Mike Shulman (May 09 2024 at 19:21):Well, I don't like to criticize people by name publicly, but there was an incident in 2016 when a well-known set theorist said something like "Bringing the notions of propositions and proofs directly into your foundations for mathematics is a crime against the intellect."
James E Hanson (May 09 2024 at 19:22):Ah yes that is a pretty bad take.
James E Hanson (May 09 2024 at 19:30):Yes, set theory certainly has a PR problem that comes from the inside to some extent. And set theorists and other classical mathematical logicians certainly say stupid, toxic things about other parts of logic with some regularity.
But to me I guess one thing is that I just find the vitriol directed at junk theorems and things like the von Neumann encoding of naturals in particular pretty annoying and off-base. The idea of having a more segmented foundational system in which you do things like treat ordered pairs as primitive is older than set theory itself. Russell and Whithead had binary relations as primitive in Principia Mathematica and they arguably invented type theory in some form (although it has of course changed considerably since then). Similarly, Bourbaki had ordered pairs as primitives in one of their presentations of set theory (although, amusingly enough, one of their systems was eventually shown to be unable to prove the existence of unordered pairs).
Likewise, while it's obviously dumb to go so far as to say that the finite von Neumann ordinals are what the natural numbers 'actually are', they are natural, especially in the context of infinite ordinals. It's a highly non-trivial structural fact about well-ordered sets that (classically) the well-order types are themselves well-ordered by initial segment. A relatively 'univalent' mindset then suggests the idea that it would be nice if we could literally represent a well-order type as the collection of smaller well-ordered types, and at that point what you're thinking of is precisely the von Neumann ordinals.
James E Hanson (May 09 2024 at 19:32):And more broadly, the decision to not have stuff like explicit primitive ordered pairs in set theory was an intentional drive to minimize primitives, in order to make metamathematics easier. And I'm not really convinced that that idea doesn't still have merit.
Mike Shulman (May 09 2024 at 23:38):I think it's a stretch to call Tom's article "vitriol".
Mike Shulman (May 09 2024 at 23:45):Your points are certainly valid (though not without potential counterpoints) for the purposes of doing set theory research and metamathematics. But, again, that's not what Tom is writing about: his point is that for the non-set theorist using set theory, and the student learning set theory -- and he doesn't say this, but I would add, for the computer verifying mathematical arguments -- there can be benefits to a formal system that more closely matches the way sets are used outside of set theory research.
Mike Shulman (May 09 2024 at 23:46):Just because an idea is older doesn't make it wrong. (-:O
Mike Shulman (May 09 2024 at 23:48):Can't you think of ZFC as like an "assembly language" for set theory, that the experts use when coding up the "operating system", and the equivalent language of ETCS (or, even better in my opinion, MLTT) as a "high-level language" that users can work with directly, making "system calls" to the theorems proven by the experts in assembly language without needing to speak the assembly language themselves?
James E Hanson (May 10 2024 at 03:17):I wouldn't call Leinster's article vitriol either, but I do think that people more generally bring up these things as if they're just obviously fatal flaws. Someone in the algebraic topology Discord server recently told me 'nobody in the world thinks of the natural number 2 as an element of the natural number 4' and, as I just argued, I feel like it's not really that ridiculous of a way of thinking about the natural numbers.
I do think the assembly language metaphor is pretty good, although not completely accurate, of course. For instance, if we were designing a proof assistant for 'finitary' mathematics around the consistency strength of PA, we certainly wouldn't have PA be the exposed end-user theory and we might not even really use it for the kernel either. But I also think there's a reason that metamathematics of arithmetic research doesn't work with finitary set theories that often. It's because the global structure of natural numbers-like objects is a bit easier to reason about. Things like cuts are pretty simple to visualize. The fact that coding stuff in PA results in far worse junk theorems than ZFC is irrelevant.
Mike Shulman (May 10 2024 at 03:39):I feel like many of these arguments are people talking past each other. Your point is, if I understand it correctly, that von Neumann ordinals are a sensible way of encoding the natural numbers, which I agree with. But the other person's point is that it's ridiculous to claim that that's what the natural numbers "really are", and I think that's equally true. So the two points are really perfectly consistent with each other.
James E Hanson (May 10 2024 at 04:10):Maybe, but this is also something that gets flattened in heat-of-the-moment comments, so sometimes it's hard to tell what people are saying. The thing is that it's not just that I think the von Neumann ordinals are a sensible or reasonable way of encoding the natural number; I think they're a natural way of encoding the natural numbers. They're certainly not the only natural way of doing so, of course.
I have a more specific point I'd like to bring up. If you'll forgive me for possibly putting words in your mouth, I feel like one of the core points you and Leinster are arguing is something to the effect of 'The non-categorical structure present in ZFC isn't really relevant to everyday mathematics.' Obviously for the sake of friendliness, Leinster isn't phrasing ETCS in directly categorical terms, but I feel it's pretty clear that the formalism is motivated by category theory. The thing is that I don't find this point (which, again, maybe you don't agree is one of the things you're saying) entirely convincing. Consider the following proposition:
Proposition. For any Grothendieck universes and , exactly one of the following happens:
- There is a category object in that is equivalent to .
- and are equivalent as categories.
- There is a category object in that is equivalent to .
This is a pretty strong structural fact about Grothendieck universes, and I would argue a non-obvious one given a purely categorical mental picture of Set. It should be provable in ETCS+R, but I don't really see a 'conceptually clean' proof of it in that framework. Obviously I chose this because it has a pretty intuitive direct proof in ZFC, but what would you say a reasonable ETCS+R proof of this would look like?
David Michael Roberts (May 10 2024 at 05:23):How are you thinking of a Grothendieck universe if you are talking about one being equivalent to a category? As the category of sets of cardinality smaller than the traditional universe-as-set?
David Michael Roberts (May 10 2024 at 05:24):In principle none of these could be true! Depending on how you are thinking of the universes in ETCS+R
Mike Shulman (May 10 2024 at 05:33):I assume James means the full subcategory of Set determined by the -small sets.
Mike Shulman (May 10 2024 at 05:39):But I don't see any problem proving this in ETCS+R, so maybe I'm missing the point. It just follows from the fact that (assuming the axiom of choice and replacement), cardinal numbers satisfy trichotomy, right? So given two universes , either is -small, or , or is -small, and that gives the three cases fairly directly.
Mike Shulman (May 10 2024 at 05:42):Depending on your structural definition of "universe" there is a step to get from that to cardinalities, but that's true in ZFC too: you consider the supremum of all the well-orderings on elements of and that's your inaccessible cardinal of the universe. And of course, like any structural argument about well-orderings, you can do that without any von Neumann encoding.
Mike Shulman (May 10 2024 at 05:46):It's true that this feels like less of a natural thing to do from a categorical perspective. But I would argue that's because it is a fairly unnatural thing to do, as evidenced by the fact that it doesn't survive in the absence of the axiom of choice. (-:
James E Hanson (May 10 2024 at 12:46):Mike Shulman said:
But I don't see any problem proving this in ETCS+R, so maybe I'm missing the point. It just follows from the fact that (assuming the axiom of choice and replacement), cardinal numbers satisfy trichotomy, right? So given two universes , either is -small, or , or is -small, and that gives the three cases fairly directly.
How do you show that two universes with the same cardinality are equivalent?
James E Hanson (May 10 2024 at 12:52):Ah okay I think I can see the argument. One way would be passing to a skeleton.
James E Hanson (May 10 2024 at 13:01):What would be the argument for something like 'every set embeds into a set whose cardinality is a beth number'?
James E Hanson (May 10 2024 at 13:05):Ah, I see. If you just cared about getting into some beth number, you could always use a set of cardinality .
Mike Shulman (May 10 2024 at 14:25):James E Hanson said:
Ah okay I think I can see the argument. One way would be passing to a skeleton.
Or just use choice directly: each set in is isomorphic to some set in , so choose one, and that gives you a map which it's easy to extend to a functor. Do that in the other direction too, and you get a pair of inverse equivalences.
Mike Shulman (May 10 2024 at 14:30):James E Hanson said:
Ah, I see. If you just cared about getting into some beth number, you could always use a set of cardinality .
... and then by the well-ordering principle there is a least such beth number.
James E Hanson (May 11 2024 at 00:29):I can see now that I was wrong in that I was pretty considerably overestimating how difficult these things would be to formalize in ETCS+R, but I feel like there's one of your points that I still disagree with pretty strongly, although of course I could be wrong here too.
You and Leinster both allude to the possibility that pure set theory research itself might be better done in a more categorically motivated framework like ETCS. For instance you said:
Certainly current set theorists find ZFC easier; but how much of that is intrinsic, and how much of that is just that it's what they're used to and what all the literature uses? I don't think we can really say.
The thing is that I feel like there is enough evidence regarding this point to reasonably come to the conclusion that, no, set theorists are not just working in ZFC because of historical inertia. A huge amount of the truly technical work in set theory has to do with really detailed 'fine structure'; you think about building set-theoretic universes 'brick by brick.' This pretty naturally involves more precisely structured versions of the cumulative hierarchy, stuff like L, L[R], and fancier versions of L that are able to accommodate larger large cardinals. This is what eventually leads into things like the inner model program and mice and such.
It should be noted that L and other inner model constructions aren't only relevant in the context of ZFC; they're an important notion in basically all ZF-like set theories, even ones weaker than ETCS, such as KP. So even if we accept Leinster's point that ETCS doesn't really need replacement or pass to working in something like a classical type theory with no global replacement, it doesn't change the relevance of L-like constructions to metamathematics. Absoluteness arguments involving small extensions of L are how you show that certain broad classes of classical theorems don't need the axiom of choice. Removing appeals to choice from theorems is something that you obviously care about and a decent amount of non-set-theorist mathematicians also care about. People write papers about 'dezornifying' well-known results seemingly without knowing about existing general theorems in set theory that could accomplish the same end.
Lawvere's paper on ETCS was published in 1964, 60 years ago. Gödel's L construction was already 26 years old at that point. The construction of L is not an intensely technical thing. It's routinely taught as part of one-semester intro graduate set theory courses. I get the impression from this conversation that in the last 60 years no significant work has been published on trying to smoothly run the construction of L or other inner models in ETCS or some other more categorically motivated framework, otherwise you would certainly know about it and would have mentioned it earlier. Lawvere's original paper and the nLab article on the constructible universe don't mention anything like this either. Why hasn't there been more work on translating basic, fundamental ideas in the field of set theory to a structural framework? Is it just lack of interest? The thing is that I feel like a graduate student or particularly advanced undergradute could write down the construction of L in ETCS. It's really not that hard. It's just that the resulting thing would need to pass through a ZF-like construction and many basic properties of L are proven with exceedingly materialistic methods, such as the condensation lemma. None of this seems very categorically natural, and, in fact, I don't think it is categorically natural. I think it's a different kind of fundamental structure, and at the moment it seems to me that it is obfuscated, to some extent, by the big-pile-of-stuff ontology of categorical frameworks like ETCS.
Mike Shulman (May 11 2024 at 01:19):You definitely have a strong argument. It's quite possible that you're right, and I'm being an old curmudgeon stubbornly complaining about the way the world happens to be. But I'm not ready to throw in the towel just yet.
L and its ilk are, to me, one of the most mysterious objects in mathematics. On the one hand, as you say, the only way we know how to construct them is heavily material. But on the other hand, they clearly have a structural meaning: the category of sets and functions in L is distinct from the category of sets and functions in V, and because ZFC is equivalent to ETCS+R, the category of sets and functions in L carries all the same information as L itself. So it seems contrary to reason to me that there would be no way to achieve the same or a similar construction directly structurally.
This is especially true since practically everything else in mathematics is structural. If you're right, then set theory would be effectively unique in all of mathematics in depending on non-structural properties. It just seems highly unlikely to me, a priori, that any one area of mathematics would be different from the rest of mathematics in this way.
I also feel like there's a mathematical reason to care, namely that once you pass to weaker theories, the structural ones are no longer equivalent to the material ones, only mutually interpretable. So, for instance, it's not clear to me how to use L-like constructions, with the extant understanding of them, to say things about a non-boolean topos or pretopos.
I agree that, as you say, the current definitions of inner models are exceedingly materialistic and would would highly unnatural and awkward if simply passed across to ETCS. But it's not clear to me that this is an argument against the possibility of achieving something equivalent with a different construction that would be more natural in structural set theory. As you say, in the past 60 years no one has done it. But how many people have really tried? Mathematics is full of things that could have been discovered decades earlier than they were, if anyone had thought of them, but it just happens that nobody did.
James E Hanson (May 11 2024 at 02:02):For fancier inner models, I don't know if there's a story like this, but for L itself it's possible to think about it in terms of notions of ordinal computation (stuff like ordinal Turing machines or ordinal primitive recursive functions). There are some connections to -recursion theory here. (In some sense though this is an even more material picture, like passing from ZF - infinity to PA.)
My intuition is that in some sense both impredicativity and the ability to reduce everything to binary {0,1}-valued data are somewhat important to the character of L. I don't remember the exact story, but I seem to recall hearing that Gödel himself thought about the construction as being somehow about the interplay between the impredicativity of the ordinals and this very explicit, almost constructive, definable powerset operation. (I think he might have explicitly cited constructive mathematics as inspiring the construction.) In some sense I feel like it's maybe analogous to Turing completeness or Gödel's original arithmetization of syntax in that there's something significant about the fact that a system doesn't need to have certain kinds of structure to be explicitly present in order to be able to code that structure indirectly.
Even though people have written down the definition and looked at it, I don't yet feel like I really understand what's going on with L in constructive set theory (and by extension in non-Boolean toposes). I'm pretty sure it doesn't admit the same kind of ordinal computation picture, since that relies on the kind of case splitting you really can't do with arbitrary ordinals constructively. I actually asked Rathjen if he knew of any choice-like structural consequences of V=L over IZF or CZF and, if I recall correctly, he said he didn't know any without extra assumptions like LEM for bounded sentences.
James E Hanson (May 11 2024 at 02:05):Oh another thing to note with regards to impredicativity is that in the context of reverse math, we know that V=L as an axiom only really starts making sense once you get up to . You need to be able to perform transfinite induction. I feel like this might be sort of a miniature reflection of Gödel's idea that the impredicativity of the ordinals is important to the construction.
James E Hanson (May 11 2024 at 02:06):Although I guess, strictly speaking I don't know of any results that could be interpreted as saying that V=L doesn't make sense below , just that the standard technique for building L breaks down in that context.
James E Hanson (May 11 2024 at 02:29):Actually I think I'm getting confused. You might need a little bit more to actually construct L in second-order arithmetic. There's actually a pretty well-known result that there is no minimal model of , which is sort of saying that nothing like L can be constructed in alone.
James E Hanson (May 11 2024 at 02:31):This paper by Kameryn Williams discusses this and related phenomena.
David Michael Roberts (May 11 2024 at 04:40):My suspicion is that any structural approach to L will have to be via some kind of syntactic category. Seeing that L is suitably minimal and kinda has a universal property. As L has all the same ordinals as V, the functor from the sets of one to the sets of the other is essentially surjective. So one has to really "just" constrain the allowable functions somehow that will be the morphisms of a putative "category of sets in L", relative to the given category Set axiomatised by ETCS(+R). I have been mentioning the problem of constructing L now and then for over a decade, but category theory people seem to be generally interested in different questions, even when acknowledging that defining a "structural L" is an open problem. Mike here (and a few others) are some of the few people I know that would really like to see a solution.
James E Hanson (May 11 2024 at 13:45):Do you think that 'transitive model of ZF' or 'transitive model of KP' has a nice interpretation in ETCS? When is a model of, say, KP, it is the unique smallest transitive model of KP containing all of the ordinals less than . itself is the union of these.
James E Hanson (May 11 2024 at 13:47):In general I think that a lot of intuition set theorists have about ZFC comes from thinking about reflection. Even if you don't have Grothendieck universes, you have a bunch of 'almost' Grothendieck universes, i.e., arbitrarily good (first-order) approximations of the whole universe.
James E Hanson (May 11 2024 at 13:48):Grothendieck universes seem a little easier to formalize in categorical language to me since they're characterized by a second-order property.
Mike Shulman (May 11 2024 at 16:18):Transitivity of a model doesn't make sense structurally, since it refers to the ambient of set theory. Structural mathematics is up to isomorphism, and every model is isomorphic to a transitive one (at least in a theory strong enough to do Mostowski collapse).
Mike Shulman (May 11 2024 at 16:19):But I would expect reflection should make perfect sense structurally.
James E Hanson (May 11 2024 at 16:53):Mike Shulman said:
Transitivity of a model doesn't make sense structurally, since it refers to the ambient of set theory. Structural mathematics is up to isomorphism, and every model is isomorphic to a transitive one (at least in a theory strong enough to do Mostowski collapse).
I know that, but for -models of first-order ETCS+R, it is an isomorphism invariant thing (or more specifically, a categorical-equivalence invariant thing), so what is a purely structural description of it?
James E Hanson (May 11 2024 at 16:55):I guess it should be this: The transitive model of ZFC corresponding to is a subset of the transitive model of ZFC corresponding to if and only if every set of ordinals in is isomorphic to a set of ordinals in .
James E Hanson (May 11 2024 at 16:56):(Isomorphic as subsets of well-ordered sets.)
James E Hanson (May 11 2024 at 17:03):This might actually be equivalent to being equivalent to a (not necessarily full) subcategory of .
James E Hanson (May 11 2024 at 17:17):I guess, to me, I feel like the cumulative hierarchy gives a pretty clear structural picture of what's going on with small -models of ETCS+R in ETCS+R. Roughly speaking such objects have a 'height' (i.e., how big are the well-ordered sets in it) and a 'width' (i.e., how many subsets of well-ordered sets are in it). There should be some reasonable definition of morphism between -models of ETCS+R (something like categorical embedding that preserves ordinals) and this category is, up to equivalence, a poset (i.e., something like every self-morphism is naturally equivalent to the identity and all morphisms are mono).
For any given height, it's a non-trivial structural fact that there's a unique minimal -model of ETCS+R. L is then a large directed colimit of these minimal models (assuming there are arbitrarily large small -models of ETCS+R, which is not a given).
The tricky thing is that if you don't have arbitrarily large small -models of ETCS+R. Well, you still always have arbitrarily large small -models of arbitrary finite fragments of ETCS+R, and you can tell roughly the same story that way.
James E Hanson (May 11 2024 at 18:25):Mike Shulman said:
This is especially true since practically everything else in mathematics is structural. If you're right, then set theory would be effectively unique in all of mathematics in depending on non-structural properties. It just seems highly unlikely to me, a priori, that any one area of mathematics would be different from the rest of mathematics in this way.
Anyway, I guess that broadly it's kind of hard for me to come away from conversations like this without the feeling that some of the animosity set theorists (and classical mathematical logicians more broadly) feel towards category theory isn't entirely unjustified.
Since Mac Lane and Lawvere, people have been insinuating or outright stating that set theorists are 'doing set theory wrong' because they're not using more category theory (or, more problematically in my opinion, that what set theorists are doing is 'meaningless' because it doesn't seem categorically natural). But, as we have just discussed, people who are interested in doing set theory 'correctly' haven't come up with a satisfactory explanation of the 'real meaning' of a nearly 90-year-old theorem for more than half a century. This is Chapter VI of Kunen.
You implied that if L really is 'non-structural,' then it would make set theory unique in mathematics, but I think that 'essentially non-structural' properties are maybe more common in classical mathematical logic than you're implying. For starters, as I said, L is just the absolute beginning of set theory. Since it is actually canonical it seems maybe more amenable to categorical analysis, but fancier inner models like L[U] aren't going to be the initial object in some category because they're not unique.
There's a really concrete example of this in computability theory. The Friedberg–Muchnik theorem (i.e., that there is a c.e. set with Turing degree strictly between and ) is proven with a priority argument which involves in a seemingly essential way picking some specific enumeration of Turing machines. It's widely conjectured among computability theorists that there is no 'natural construction' of an intermediate Turing degree, something which doesn't rely on a particular choice of enumeration. The impression that Andrej Bauer gave me when we talked about this is that nobody knows how to give a presentation of priority arguments in terms of synthetic computability. Priority arguments are the absolute core of computability theory. And, again, the Friedberg–Muchnik theorem was published in 1956/1957, nearly 70 years ago. Andrej's original paper on synthetic computability theory isn't nearly as old as Lawvere's paper on ETCS, but it's still coming up on 20 years at this point.
But also, I don't know, to me Turing completeness itself is something of a 'non-structural' phenomenon. There doesn't seem to be a candidate for a canonical model of computation, but there's still a level of 'richness' at which all models of 'explicit' finitary computation become equivalent. And it feels like maybe L could be a similar kind of phenomenon. What's going on in the construction of L is that if you take some sufficiently rich 'explicit' way of constructing sets in a really slow, careful, brick-by-brick way and iterate it along an impredicatively long 'large ordinal,' you get something that seems internally like a 'full' universe of sets and, moreover, any two constructions of this end up being equivalent. It may very well be the case that there just is no canonical 'god-given' model for that slow, careful construction.
Morgan Rogers (he/him) (May 12 2024 at 08:17):James E Hanson said:
The Friedberg–Muchnik theorem (i.e., that there is a c.e. set with Turing degree strictly between 0 and 0′) is proven with a priority argument which involves in a seemingly essential way picking some specific enumeration of Turing machines.
Not all constructions are universal, this is a separate issue from whether they can be reproduced in a structural set theory, no? The transformation [enumeration] --> [c.e. set] could still be translated to a structural presentation.
James E Hanson said:
There doesn't seem to be a candidate for a canonical model of computation, but there's still a level of 'richness' at which all models of 'explicit' finitary computation become equivalent.
There have been several attempts to axiomatize models of computation so as to capture Turing completeness (which would give "canonical models" if the axiomatization were algebraic enough to yield free models). I am aware of these because there is a group at my lab actively working on this research and holding a reading group on papers containing such attempts.
I would second Mike's reply that "no one has done this yet" is not much of an argument for whether or not something can be done. Let's set some PhD students on it and see where we end up :wink:
Patrick Nicodemus (May 13 2024 at 12:56):Morgan Rogers (he/him) said:
James E Hanson said:
The Friedberg–Muchnik theorem (i.e., that there is a c.e. set with Turing degree strictly between 0 and 0′) is proven with a priority argument which involves in a seemingly essential way picking some specific enumeration of Turing machines.
Not all constructions are universal, this is a separate issue from whether they can be reproduced in a structural set theory, no? The transformation [enumeration] --> [c.e. set] could still be translated to a structural presentation.
It's definitely the case that one can do degree theory in an elementary topos with LEM by direct translation of the standard arguments.
I would second Mike's reply that "no one has done this yet" is not much of an argument for whether or not something can be done. Let's set some PhD students on it and see where we end up
I won't speculate about the likelihood of this being doable or not, by all means people should be researching it. I think that
Priority arguments are the absolute core of computability theory
this is the more important takeaway, I agree with James that this is "sine qua non". It should be a central research question in synthetic computability theory (insofar as there is a goal of understanding classical computability theory from a "synthetic" perspective, if people have the goal of creating a new and distinct theory that's fine but it will mean less cross fertilization with currently existing computability theory)
Patrick Nicodemus (May 13 2024 at 12:59):I worked on this briefly during my phd, experimenting with a kind of defeasible logic with a temporal modality similar to Nakano's time modality, with the goal of understanding priorirty arguments. I didn't really get anywhere, I got stuck trying to prove the Exact Pair lemma.
Patrick Nicodemus (May 13 2024 at 13:03):It might be possible to avoid explicit program enumeration by incorporating primitives for dovetailing into the domain logic, using a temporal modality, and having some kind of semidecidable predicates as primitives
Mike Shulman (May 13 2024 at 16:56):Perhaps it wasn't clear what I mean by "structural". I was using that adjective in the sense of "structural set theory" vis-a-vis "material set theory", i.e. essentially "invariant under isomorphism of sets and equivalence of categories". So by this definition, the cumulative hierarchy is fundamentally non-structural, because it distinguishes between isomorphic sets; whereas there's nothing non-structural about picking an enumeration of Turing machines any more than there is about picking a basis of a vector space.
Mike Shulman (May 13 2024 at 16:58):In fact, it's very common in structural mathematics for there to be multiple equivalent/isomorphic definitions of something, none of which is preferred as "the" correct definition. Cf. for instance -categories. So the nonexistence of a canonical model of computation is perfectly structural as well.
James E Hanson (May 13 2024 at 18:03):Mike Shulman said:
Perhaps it wasn't clear what I mean by "structural". I was using that adjective in the sense of "structural set theory" vis-a-vis "material set theory", i.e. essentially "invariant under isomorphism of sets and equivalence of categories". So by this definition, the cumulative hierarchy is fundamentally non-structural, because it distinguishes between isomorphic sets; whereas there's nothing non-structural about picking an enumeration of Turing machines any more than there is about picking a basis of a vector space.
I feel like I can't really square why you think L is so 'mysterious' in that case. In a historically revisionist way, set theorists discovered that a certain quotient-inductive type is sufficiently rich to reflect the behavior of a huge amount of the rest of mathematics (especially in the context of a strong, impredicative classical theory with choice). Moreover, by studying 'the combinatorics of well-founded trees' as some people dismissively phrase it, they're able to very precisely build models of ETCS+R that satisfy or don't satisfy a huge variety of statements, as well as doing other impressive stuff such as automatically removing choice from the proofs of various theorems.
To me this could be seen as directly analogous to discovering that untyped lambda-calculus is Turing complete. Type theorists spend a lot of time thinking about really detailed specifics of the behavior of lambda-calculus and variants thereof because they decided it was a good framework to think about these things, but untyped lambda-calculus isn't what computation is. Term normalization isn't what computation is. It's a particular nice model of computation that is amenable to a lot of fine structural analysis.
The fact that in ZFC sets are more than just their place in the category of sets feels like a completely cosmetic issue to me.
Mike Shulman (May 13 2024 at 21:24):That's a very interesting perspective: that working in ZFC is kind of like choosing a basis for a vector space or a model of computation. It still makes me uncomfortable because only in the (IMHO fairly degenerate) case of a "strong, impredicative classical theory with choice" can this "basis" be shown to "span" the entire "space". But, of course, in constructive mathematics not every vector space has a basis either, so maybe I shouldn't be surprised that one can do more classically than constructively.
Mike Shulman (May 13 2024 at 21:27):It does still seem somewhat mysterious to me. In linear algebra, the notion of linear combination, span, and hence basis is really kind of implicit in the very notion of vector space, so it's not surprising that to do computations we pick one. And most definitions can be formulated without choosing a basis, in terms of the abstract notion of vector space. Whereas in the theory of computation, we don't really have a definition of "computation" at all except "the thing that's modeled by all these equivalent things", so it's again unsurprising that we have to pick a model in order to do anything. But in the case of set theory, we do have an abstract "basis-free" definition of a universe of sets (ETCS and its ilk), and the well-founded trees of ZFC are not implicitly present in this definition; so why should we expect them to be necessary to prove things about abstract universes of sets?
Benedikt Peterseim (May 13 2024 at 21:40):If using well-founded trees to construct certain (Boolean) topoi is mysterious to you (is it?), are the other ways to do so such as sheaves or realizability topoi less mysterious? And why so? (Not trying to make a point, just trying to understand yours.)
James E Hanson (May 14 2024 at 00:00):Mike Shulman said:
It does still seem somewhat mysterious to me. In linear algebra, the notion of linear combination, span, and hence basis is really kind of implicit in the very notion of vector space, so it's not surprising that to do computations we pick one. And most definitions can be formulated without choosing a basis, in terms of the abstract notion of vector space. Whereas in the theory of computation, we don't really have a definition of "computation" at all except "the thing that's modeled by all these equivalent things", so it's again unsurprising that we have to pick a model in order to do anything. But in the case of set theory, we do have an abstract "basis-free" definition of a universe of sets (ETCS and its ilk), and the well-founded trees of ZFC are not implicitly present in this definition; so why should we expect them to be necessary to prove things about abstract universes of sets?
(Apologies, this is a bit long.)
Well so, for starters I think there's a relatively clear picture in the presence of enough choice (and therefore also enough classicality). The ordinals (in the sense of isomorphism classes of well-ordered sets) have a pretty clear rigid global structure (since they are themselves well-ordered up to isomorphism by initial segments). Since we have choice, any small configuration of sets is isomorphic to a configuration of subsets of finite sequences from a fixed well-ordered set, which you can then think of as a configuration of finite sequences of ordinals. If we have just a little bit of replacement, the ordinals are closed under Gödel's ordinal pairing function, which is arbitrary but very absolute in the set-theorist's sense. Using this (and possibly some other tricks involving Cantor normal form) we can code these arbitrary configurations as just sets of ordinals. So in this way you arrive at the idea of representing set theory sort of as the theory of 'second-order ordinal arithmetic' (but with the stipulation, provided that we have a little bit of replacement, that sets of ordinals are bounded).
Second-order ordinal arithmetic is a decently nice theory and set theorists do sometimes say that this is what ZFC 'really is' (i.e., the theory of ordinals and sets of ordinals), but one annoying thing about it is that it's even more material than ZFC. You have no native representation of sets of sets of ordinals. The power set axiom itself is quite a pain to actually even state (although the flipside is that choice is of course automatic in this context). One thing also I think should be noted is that L has to me a pretty clear description in this context as being the smallest family of sets of ordinals closed under some very basic closure conditions that any model of this theory (with the same ordinals) must have. In the presence of enough replacement, this smallest family is then itself a model of the theory.
So, now, assuming we have, say, full replacement, one thing we could do at this point is flesh the theory out into a fuller classical almost Principia-style 'type theory' (although it's not going to be quite like most MLTT-style type theories). We have a set for each ordinal , which is just a canonical choice of a well-ordered set of that length. Then we have power sets, function sets, and products and coproducts of families indexed by sets in a sufficiently explicit way (i.e., first-order definable). All of these constructors were there already up to isomorphism, but now we're more explicitly tracking the 'provenance' of various sets, which is useful for thinking about the interplay between the power set operation (and the other constructors) and the ordinals, which is in some sense the heart of what makes different set-theoretic universes (with choice, etc.) 'actually different.' For instance, CH is a statement of this kind. In particular though, we're going to assume that all sets are built using these constructors. This gives us a good induction principle to prove things about arbitrary sets. Since we already know every set is isomorphic to some (since we have choice), if our goal is to track this interplay carefully, we want to have an explicit description of where everything is coming from.
At this point though, I am obviously going to point out that well-founded trees have naturally popped up in what we're talking about. We started from ordinals, which are of course closely related to well-founded trees, but then we've added explicit bookkeeping for these set-generating operations, which also naturally have the structure of well-founded trees (since we're assuming all of the sets are generated by our constructors). Well-founded trees are very natural in the context of induction on infinite structures, and by assuming choice, we've made it so that 'everything is controlled by induction' in some sense. So at this point, I feel like it's reasonable to conclude that thinking about well-founded trees might be a natural way of understanding the combinatorial behavior of a universe of sets.
This thing I've described might at this point be a decently 'usable' theory, depending on how you implement in precisely. One could probably make a reasonable proof assistant based on it (maybe with some more inductive constructions thrown in explicitly). I would also argue that this is maybe a decent approximation of what mathematicians who are 'working in ZFC' are 'actually working in.' But if our goal is to do metamathematics, I still maintain there's some value in minimizing primitives. (Obviously we started from a theory with fewer primitives, but not all ways of minimizing primitives are equally useful.) Even type theorists do this. System F doesn't explicitly have inductive types, for instance. Some of the things I described are obviously redundant since we're working with classical sets. Functions can obviously be coded as subsets of the product, but products themselves can also be coded in terms of power sets of coproducts. And maybe this is where I might lose you if I haven't already, but if you whittle this down enough you get to the point that the only thing you really need is iterating power sets along the ordinals (with coproducts at limit ordinals). This suggests a 'slightly typed' von Neumann hierarchy: , , and for limit . (We've even thrown away the 's since these get generated in a lot of different explicit ways by this process, even without choice.) Then 'the whole universe' would be . This is basically a transfinite version of TST (Théorie Simple des Types, which was itself constructed to be a version of Principia Mathematica with fewer primitives) and is really close to the actual von Neumann hierarchy in ZFC. In some sense the only real difference is the absence of 'subtyping.'
At this point I think the motivation for going to the actual von Neumann hierarchy is a maybe a little bit harder to state, and yes, possibly a bit historical. (Although I'll be quick to point out that Coq itself has universe subtyping in its own 'cumulative hierarchy,' so I don't think it's prima facie a ridiculous design decision.) I think there are still some arguments for the 'von Neumann hierarchy with subtyping,' but I think I need to spend some time thinking about what things like measurable cardinals and the condensation lemma look like in this picture I've painted.
James E Hanson (May 14 2024 at 00:03):But here a different 'basis' does suggest itself. The lack of functions as first-class objects is definitely an obnoxious aspect of ZFC. We could define our 'cumulative hierarchy' in terms of function sets instead of power sets like this: , , and (or maybe starting with to make the beginning less silly). But there still is something fundamentally 'well-foundedly treeish' about this construction.
Mike Shulman (May 14 2024 at 00:16):I was about to respond "But what makes you think that well-orderings should figure in a "basis" for set theory in the first place?" But then I remembered [[algebraic set theory]]!
James E Hanson (May 14 2024 at 00:17):What is the connection there?
Mike Shulman (May 14 2024 at 00:20):I mean in the sense of the original paper of Joyal and Moerdijk. The meaning of the phrase drifted a bit after that, coming to refer almost as much to the abstract "categories of classes" they introduced as to the ZF-algebras they introduced them in order to define, but I think what they intended the phrase to refer to was the ZF-algebras. It seems arbitrary to me to just randomly pick on well-orderings as a structure to use as a basis for set theory, but Joyal and Moerdijk showed that the po-class of ordinals, and indeed the cumulative hierarchy itself, has a natural universal property in the category of classes.
Mike Shulman (May 14 2024 at 00:31):A ZF-algebra is a partially ordered class with suprema of all sets and a successor operation ; the cumulative hierarchy is the initial ZF-algebra. This is arguably almost as natural an object to study as the natural numbers, which are the initial pointed set equipped with a successor. So one doesn't have to make up the notion of well-ordering, it comes naturally from a universal characterization.
James E Hanson (May 14 2024 at 00:32):I think something we're not really going to see eye-to-eye on is that I don't think a notion needs to come from category theory to be natural.
Mike Shulman (May 14 2024 at 00:33):I wouldn't say that I think something needs to come from category theory to be natural, but it should have some motivation. I didn't come away from your long message with a motivation for introducing ordinals; you just said here are a bunch of things we can do with them, and once we have ordinals we're naturally led to sets of ordinals and the cumulative hierarchy.
Mike Shulman (May 14 2024 at 00:34):Maybe "motivation" is the wrong word.
Mike Shulman (May 14 2024 at 00:37):I mean, I said what feels weird to me about the well-orderings is that they aren't anywhere in the axioms of ETCS, you have to decide to bring them in. As a technical device that's fine, but philosophically, why ordinals rather than something else?
Mike Shulman (May 14 2024 at 00:39):On the other hand, @Benedikt Peterseim has a good not-a-point :smile: that sheaves and realizability are also something you have to decide to bring in, so why do I feel differently about V and L?
Mike Shulman (May 14 2024 at 00:40):(I am really enjoying this conversation, by the way, and how it's forcing me to try to express these feelings clearly. Maybe I'll even end up convinced of something.)
James E Hanson (May 14 2024 at 00:43):The story doesn't need to start with ordinals. You can start with just the set-forming constructors, which bring well-founded trees in immediately. One philosophical argument at this point is that it might be reasonable to think about the smallest family of sets generated by these constructors. This is sort of like the 'second-order initial model' of the theory, and it already contains isomorphic copies of a lot of the objects mathematicians think about. (This would be analogous to restricting to pure sets in the context of ZFA.) Choice (with enough replacement) ends up implying that every set is isomorphic to a set generated in this way. Ordinals come out of well-founded trees pretty naturally (even constructively, although constructive ordinals can behave strangely) via ranks, although I do personally think that well-founded trees are a bit more fundamental than ordinals, especially constructively.
Mike Shulman (May 14 2024 at 00:43):The material set-forming constructors bring in well-founded trees immediately (assuming the axiom of foundation), but that's circular -- I want a motivation starting from ETCS.
Mike Shulman (May 14 2024 at 00:47):I do agree that well-founded trees are more fundamental than ordinals. Coming from type theory, I would probably say that inductive definitions are even more fundamental than well-founded trees. So I guess you could argue that if you want to build the "smallest model" of set theory, it makes sense to think of it as built out of "all inductively defined sets" and interpret that as meaning well-founded trees.
James E Hanson (May 14 2024 at 00:48):I'm conceptualizing the constructors in a type-theory-like way. But also, I feel like this is fairly clear. If I just start from Leinster's informal description of ETCS and imagine that these are the only way of building sets and moreover sets come tagged with a 'type,' you get an inductive-type-like structure.
image.png
James E Hanson (May 14 2024 at 00:50):Also, I guess, when I talk about well-founded trees, in my head it's sort of given that they may have labels on the nodes, which makes them almost literally the same thing as inductive types.
James E Hanson (May 14 2024 at 00:53):The point is that as soon as you start tracking how the sets are being generated explicitly, you get this structure that resembles an inductive type/well-founded tree.
James E Hanson (May 14 2024 at 00:54):This is in some sense why I don't really find ETCS to be all that satisfying relative to type theories or material set theories. I like having the existence of things like Cartesian products be a little more explicit/constructive than just saying that an object with the required universal property exists.
James E Hanson (May 14 2024 at 01:06):James E Hanson said:
Also, I guess, when I talk about well-founded trees, in my head it's sort of given that they may have labels on the nodes, which makes them almost literally the same thing as inductive types.
Also, a lot of the time well-founded trees in classical mathematical logic have ordered levels, so they really are pretty similar to just being inductive types.
Mike Shulman (May 14 2024 at 01:10):Well, yes of course, any equationless algebraic structure has an initial model, which is inductively defined and therefore has a well-founded order. But the well-founded order you get on the objects of the initial model of ETCS is entirely different from the well-founded ordering on ZF-sets, so it doesn't directly motivate that, and it doesn't motivate the general notion of well-foundedness any more than any other algebraic structure does.
James E Hanson (May 14 2024 at 01:14):Fundamentally the motivation for talking about well-foundedness in the context of 'arbitrary' sets is going to be that choice implies that all sets can be well-ordered. This means that (in the context of choice) the structure of arbitrary sets is controlled by the structure of 'explicitly well-ordered sets' (i.e., subsets of ordinals). I don't know if it's going to be much more to say about it than that.
Mike Shulman (May 14 2024 at 01:15):Uh-oh, that better not be the motivation or you'll never convince anyone who doesn't believe in choice to care about it!
Mike Shulman (May 14 2024 at 01:19):Didn't you just say a minute ago that well-founded trees are more natural than ordinals, especially constructively?
Mike Shulman (May 14 2024 at 01:22):James E Hanson said:
This is in some sense why I don't really find ETCS to be all that satisfying relative to type theories or material set theories. I like having the existence of things like Cartesian products be a little more explicit/constructive than just saying that an object with the required universal property exists.
I agree entirely with that criticism of ETCS, but I think ZFC suffers from "the other side" of the same criticism, and type theory is what solves all the problems! I wrote a bunch about that here.
James E Hanson (May 14 2024 at 01:23):Well, there are a couple of other justifications for caring about set theory with choice:
Also, a bit bluntly, a lot of mathematicians seem to not really be that bothered by choice at this point.
James E Hanson (May 14 2024 at 01:23):Mike Shulman said:
James E Hanson said:
This is in some sense why I don't really find ETCS to be all that satisfying relative to type theories or material set theories. I like having the existence of things like Cartesian products be a little more explicit/constructive than just saying that an object with the required universal property exists.
I agree entirely with that criticism of ETCS, but I think ZFC suffers from "the other side" of the same criticism, and type theory is what solves all the problems! I wrote a bunch about that here.
I still don't really agree with this.
James E Hanson (May 14 2024 at 01:28):There are also a fair number of things I find unsatisfying about existing type theories in the context of formalizing classical mathematics, but that's an entirely different conversation.
James E Hanson (May 14 2024 at 01:30):Mike Shulman said:
Uh-oh, that better not be the motivation or you'll never convince anyone who doesn't believe in choice to care about it!
But also, earlier in this conversation, you criticized some set theorists for being platonists about the continuum hypothesis. Why aren't you similarly critical of people who 'don't believe in choice'?
Mike Shulman (May 14 2024 at 01:31):By "not believing in choice" I include "not believing there is a fact of the matter about whether choice is true".
Mike Shulman (May 14 2024 at 01:32):Since if I don't believe there is such a fact, then I certainly don't believe it is true (and I also don't believe it is false).
Mike Shulman (May 14 2024 at 01:33):Of course what matters practically is whether I am willing to assume it or prefer to avoid it, so if you like you can read "don't believe in choice" as "prefer not to assume choice".
James E Hanson (May 14 2024 at 01:33):Okay but I also don't believe that there's a fact of the matter over whether the axioms of groups imply the 'abelianity hypothesis' (i.e., the group axioms don't imply that all groups are abelian), but that doesn't mean that I think Pontryagin duality is 'fake math' just because it only applies to abelian groups.
James E Hanson (May 14 2024 at 01:35):So the point is that you could read (and this is more or less how I intended it) my story as being about specialized tools for studying classical, impredicative, choicy universes of sets. That's a pretty special case, but they're also highly special universes of sets.
James E Hanson (May 14 2024 at 01:36):And, yes, I do think there's a compelling case (that has been made by set theorists over the last 100 years) that ordinals are fundamental to the structure of such universes of sets.
Mike Shulman (May 14 2024 at 01:36):I never said I think set theory is 'fake math'.
James E Hanson (May 14 2024 at 01:37):Sorry, I was slipping into grouchiness there. I shouldn't have said that. I do think it's true that a lot of the rhetoric people employ around the axiom of choice (and classical math more generally) has an air of 'moral condemnation,' and I find this rather annoying. You do not do this, to be clear.
Mike Shulman (May 14 2024 at 01:39):Well, I try not to, at least. I'm glad to hear you think I'm succeeding (and please do tell me if I do slip).
James E Hanson (May 14 2024 at 01:44):In any case, a set theory graduate student named Elliot Glazer was recently telling me about some results he has in Z set theory (without foundation) that are supposed to motivate the idea that 'everything can be conservatively coded as sets of ordinals' or something to that effect, but the results seem a lot more subtle and I don't really understand them yet. They're also not constructive at the moment, obviously. But in particular, this is supposed to cover the case of having urelements via Quine atoms.
James E Hanson (May 14 2024 at 01:45):In particular, he seems to be interested in trying to motivate the kind of thing we're talking about in broader contexts than things that are ultimately equivalent to ZFC.
James E Hanson (May 14 2024 at 01:45):So I'm interested to see where that goes.
James E Hanson (May 14 2024 at 01:46):I also really would like to understand what exactly is going on with the constructive version of L.
Mike Shulman (May 14 2024 at 01:49):Anyway, it sounds like we both agree that well-foundedness is natural, and either by starting with ordinals and well-orderings or an algebraic notion of ZF-algebra we can get to the cumulative hierarchy. And I take your point that ordinals are more natural a priori if you start out intending to study only classical mathematics.
Mike Shulman (May 14 2024 at 01:49):I think my remaining sticking point with is in going the other direction. Maybe once you have the notion of ZF-algebra or cumulative hierarchy, is a natural thing to look at (although it would be really interesting if there is a characterization of as some kind of ZF-algebra). But when thinking of as a presentation of a category of sets (which is the "basis-invariant" object I would really be interested in), it looks pretty weird. In practically any other construction of a large category anywhere in mathematics (including sheaves and realizability), the objects are some kind of structured set and the morphisms are some kind of function or relation preserving the structure. But I don't know of any "local" description of the objects and morphisms of like this: the morphisms are some kind of relations, but it's not clear to me how they "preserve" or "respect" the "constructibility" of their domain and codomain.
James E Hanson (May 14 2024 at 02:02):Are there any constructions of large categories that you are comfortable with that involve 'shrinking' rather than 'growing' something that looks like Set?
Mike Shulman (May 14 2024 at 03:13):I don't normally think of constructions of categories as either "shrinking" or "growing".
Mike Shulman (May 14 2024 at 03:16):One way of classifying categories of structured sets is by [[stuff, structure, property]]. I guess you could think of a functor that forgets only properties (= fully faithful) as "shrinking" its codomain, and a functor that forgets structure (= faithful) or stuff (= neither) as "growing" its codomain by equpping its objects with extra things. But my understanding is that the forgetful functor is faithful but not full, so from a categorical perspective an object of should be regarded as an object of with extra structure, just like an object of Grp, Ring, or Vect.
David Michael Roberts (May 14 2024 at 03:29):And the functor Set_L --> Set_V is eso (assuming AC), since they have the same ordinals.
It strikes me that one could consider Ord inside Set_L, and ask if every object of Set_L has a definable well-ordering (working in the material setting), so that Ord --> Set_L is eso.
Then if one can characterise what a constructible function between ordinals is, you can recover Set_L up to equivalence.
Tom Leinster (May 14 2024 at 14:54):Hi all. I'm coming late to this thread but thought I should say something.
The course I'll be teaching in Edinburgh this autumn, Axiomatic Set Theory, is principally for undergraduates in their last two years. As John says, it'll be a rigorous development of set theory based on the ETCS axioms, but I'll neither assume nor teach the notion of category. The tentative chapter/week headings are:
I'm really excited to be teaching this course, because as far as I know, nothing like it has ever been done before.
Plus, lots of people -- even category theorists and set theorists -- don't realize it can be done! For example, two people I know who are knowledgeable in both subjects assumed I'd have to get into toposes, and didn't realize it's possible to do everything in a completely elementary way. I want the world to know!
I like to explain this point by analogy with number theory and rings. If you're going to teach an introductory number theory course, you have a choice. You could say "the integers form a ring, number theory eventually needs rings other than the integers, and rings are important throughout mathematics anyway, so I'm going to begin my course by introducing rings and then specialize to the integers". Alternatively, you could say "basic number theory doesn't require the general notion of ring, so let's just talk directly about addition, subtraction and multiplication of integers without ever mentioning rings". Both kinds of course are valuable. The first is like teaching ETCS via the general notion of category, more or less as in Lawvere and Rosebrugh's book Sets for Mathematics. The second is like my course: no categories, just sets and functions done directly.
I'll say almost nothing in the course about membership-based set theories such as ZFC. I'll have to say something, as we're not in a cultural vacuum: some students will already have had some contact with ZFC, and I'll need to address the usual questions. But it'll be kept to an absolute minimum.
On some other points...
I have the same respect for set theory research as I do for any other branch of mathematics. It's a subject full of strange and wonderful things uncovered by brilliant people. What separates set theory from, say, differential geometry or harmonic analysis or semigroup theory is the claim that set theory -- specifically, ZFC -- has a special, central role in the whole of mathematics. Such a claim becomes the business of all mathematicians.
I believe it should be possible to discuss and debate such claims in a calm and constructive way. In fact, I know it is possible: when I wrote a blog post to accompany what was to become my American Mathematical Monthly article Rethinking set theory, there was a fantastic conversation of 200+ comments, involving widely different viewpoints, that was extremely civil and enlightening.
Personally, I've said just about all I want to say about the mismatch (as I see it) between sets as treated in membership-based set theories like ZFC and sets as used in practice by the vast majority of mathematicians. (In a nutshell, it's not so much the ZFC axioms that are the problem, it's the very set-up: that elements of sets are always sets, and that one can always legitimately ask whether one set is an element of another.) I have no desire to have that conversation again. Right now, I'm much more interested in demonstrating what set theory looks like when you develop everything in ETCS.
Regarding my past writings, nothing I've written about sets is intended to be hyperbolic. If something I've said looks like hyperbole, please consider that it's probably my genuinely held opinion, however much you might think it's impossible that anyone could really believe it. Of course, I'm as human as anyone and may sometimes have slipped up. I'm acutely aware of how sensitive these matters are (look at the first few paragraphs of that blog post), I know how deep a personal attachment every mathematician has to their own research area, and I have no desire to hurt or antagonize anyone. So I work hard to avoid overstatement. I want to produce light, not heat -- although I'm aware that sometimes it's impossible to have one without the other.
And this respect for differing views should go in all directions. In particular, grand claims are made for the place of ZFC in mathematics, and it's natural and healthy for those claims to be challenged. I would hope that those who advocate for the special role of ZFC (and its friends) would welcome these challenges as an opportunity to reflect and engage constructively, as people like François Dorais did in that really productive n-Café thread, and as in some of the conversation going on here right now.
I also hope that everyone, regardless of viewpoint, will agree that it's worthwhile to at least see what happens when you try to develop axiomatic set theory based on ETCS, without reference to categories, in a way that works for undergraduates. Maybe it will be a disaster, maybe it will all work out wonderfully, or, most likely, it will be somewhere in between -- but in any case, it'll be food for thought.
Mike Shulman (May 14 2024 at 17:11):Thanks for joining us, @Tom Leinster! One thing I'm curious about is what you plan to say about "elements". Are you planning to first intuitively introduce a set as a collection of things called elements, and a function as a mapping from elements to elements, and then later say that we define an element to be a function of a terminal set just for axiomatic parsimony?
Tom Leinster (May 14 2024 at 17:55):I guess I haven't decided exactly how to handle that. The introduction (week/chapter 1) will be about what it means to give axioms for sets, why it's needed, etc., including the point that we need to choose some concepts as primitive and derive the others. And I'll explain informally why elements should correspond to functions from a one-element set. (I mean "should" in terms of all the experience with sets that my students already have.) Then I'll launch in with the definition of an element as a function from a terminal set as soon as we begin the actual axioms in week/chapter 2.
Later on, we'll do the correspondence between functions and functional relations , via graphs.
James E Hanson (May 14 2024 at 18:02):David Michael Roberts said:
Then if one can characterise what a constructible function between ordinals is, you can recover Set_L up to equivalence.
A constructible function between ordinals is precisely one which is computable using an ordinal Turing machine.
James E Hanson (May 14 2024 at 18:06):Specifically though you may need a larger ordinal as a parameter.
Mike Shulman (May 14 2024 at 19:19):James E Hanson said:
A constructible function between ordinals is precisely one which is computable using an ordinal Turing machine.
Could that possibly mean that could be constructed using a sort of realizability? What is an ordinal Turing machine?
James E Hanson (May 14 2024 at 19:44):There are multiple different models of 'ordinal computation,' and there seems to be a Turing-completeness-like phenomenon here too. There's ordinal Turing machines, which are a surprisingly naive generalization of literal Turing machines to transfinite tape lengths and transfinite numbers of computational steps. There's -definability in , of course. There's Takeuti's ordinal primitive recursive functions. There's some notion of ordinal register machines. There's even been an attempt at generalizing untyped lambda-calculus to ordinal computation, but the existing formalism seems pretty unnatural to me in that it needs an explicit notion of 'iterating a function -many times' in order to allow Church numeral encoding of ordinals.
There has been some work on ordinal-computation-based realizability (this is how Andrej got a topos in which Baire space injects into the naturals), but I'm not sure whether a direct generalization would give you something equivalent to L.
Mike Shulman (May 14 2024 at 19:50):I must know the answer to this right now! (-:O
Mike Shulman (May 14 2024 at 19:57):I wonder if @Andrej Bauer knows?
Mike Shulman (May 14 2024 at 20:04):Google led me to Koepke's 2005 paper Turing Computations on Ordinals for a definition of ordinal computability, is that a good reference? He defines (Definition 4) what it means for a partial function to be ordinal computable. I assume that this collection of ordinal functions forms a (large) [[partial combinatory algebra]], and therefore we should be able to perform a realizability construction on it, obtaining at least a category, although since the PCA is large, it's not immediately clear that the realizability category is even an elementary topos. If it isn't, that would obviously preclude its being equivalent to . But perhaps even if it isn't, there is some localization or other construction on it that relates it to .
Is this a good way to formulate the question precisely? If so, and no one here knows the answer right away, I can ask it on MathOverflow.
James E Hanson (May 14 2024 at 20:10):I believe Koepke is one of the standard references, but I actually done any research in this stuff.
James E Hanson (May 14 2024 at 20:11):Ignoring the size of the PCA for a minute, when does a topos derived from a PCA satisfy LEM?
Mike Shulman (May 14 2024 at 20:17):I don't know.
James E Hanson (May 14 2024 at 20:19):Doesn't a topos constructed from a PCA usually have 'access' to the original topos via double-negation?
Mike Shulman (May 14 2024 at 20:22):Yes. Are you suggesting that means this realizability category can't be since that doesn't contain (and how do we know that?)?
James E Hanson (May 14 2024 at 20:27):What do you mean by contain? Contain as a subcategory?
James E Hanson (May 14 2024 at 20:27):I don't know how this kind of realizability is going to interact with a large PCA, but it makes me suspicious that it's not going to work this simply.
Mike Shulman (May 14 2024 at 20:27):Yes.
James E Hanson (May 14 2024 at 20:33):Mike Shulman said:
Yes. Are you suggesting that means this realizability category can't be since that doesn't contain (and how do we know that?)?
Let , where is a Cohen generic real over . Suppose for the sake of contradiction that is equivalent to a subcategory of . (This is the part I'm most sketchy on but it really should work.) Since ordinals are absolute between and , the natural numbers object of and the natural numbers object of must be isomorphic. This means that as a set of naturals already exists in , but it doesn't.
Mike Shulman (May 14 2024 at 20:36):It's definitely not true that the natural numbers object of a subcategory must coincide with the one of the supercategory. Already in the ordinary effective topos, the natural numbers object is discrete, but the natural numbers object of Set is indiscrete.
James E Hanson (May 14 2024 at 20:36):But everything is classical here.
Mike Shulman (May 14 2024 at 20:37):So?
Mike Shulman (May 14 2024 at 20:37):I don't see why the fact that the supercategory and subcategory are both boolean would force their NNOs to coincide.
James E Hanson (May 14 2024 at 20:37):I don't think that's true in general, but I think that it should be true in this case.
Mike Shulman (May 14 2024 at 20:42):I see what you mean that the von Neumann ordinals in and coincide. But I think what that says categorically is that the forgetful functor preserves the NNO, whereas the composite wouldn't be the identity, so I don't think it follows immediately that the NNO of must also be that of .
Mike Shulman (May 14 2024 at 20:43):I do agree it seems unlikely that could contain a copy of .
James E Hanson (May 14 2024 at 20:43):Think about it this way. There should be a canonical map from into defined by recursion on 's zero and successor map, right? The pullback of the indicator function of on will be the indicator function of on .
Mike Shulman (May 14 2024 at 20:44):But the subobject classifier of might also not agree with that of .
James E Hanson (May 14 2024 at 20:45):Do you know of an example of that actually happening with two models of ETCS?
Mike Shulman (May 14 2024 at 20:46):Sure, via .
James E Hanson (May 14 2024 at 20:47):Do you know an example of it happening where their subobject classifiers are literally 2-element sets?
Mike Shulman (May 14 2024 at 20:48):What does "literally a 2-element set" mean when talking about objects of a category?
James E Hanson (May 14 2024 at 20:49):Assuming we're talking about 1-categories, I mean 'actually two morphisms from the terminal object.'
Mike Shulman (May 14 2024 at 20:50):You mean, that the toposes are [[two-valued topoi]]?
James E Hanson (May 14 2024 at 20:51):That link doesn't work.
John Baez (May 14 2024 at 20:51):https://ncatlab.org/nlab/show/two-valued%20topos
Mike Shulman (May 14 2024 at 20:51):I just added the missing plural redirects (-:
James E Hanson (May 14 2024 at 20:51):Do the axioms of ETCS not imply that its models are two-valued?
Mike Shulman (May 14 2024 at 20:52):Of course not, that's an external property, not an elementary one.
James E Hanson (May 14 2024 at 20:52):I mean if you interpret them with the standard semantics of first-order logic instead of Boolean-valued models.
Mike Shulman (May 14 2024 at 20:52):No boolean-valued models here.
Mike Shulman (May 14 2024 at 20:53):is a perfectly good model of ETCS that's not two-valued.
James E Hanson (May 14 2024 at 20:53):Okay but then this presentation of the axioms is misleading.
image.png
James E Hanson (May 14 2024 at 20:54):Am I not supposed to read {0,1} as a two-valued object?
James E Hanson (May 14 2024 at 21:00):In any case, what is an example of an embedding of a two-valued model of ETCS into another two-valued model of ETCS in which the subobject classifier doesn't end up being isomorphic?
Mike Shulman (May 14 2024 at 21:02):has two elements inside the theory.
Mike Shulman (May 14 2024 at 21:03):That is, the statement "there are exactly two morphisms " is a consequence of (or perhaps is one of) the axioms of ETCS.
James E Hanson (May 14 2024 at 21:03):But then how can ETCS+R be 'equivalent' to ZFC? isn't equivalent as a category to a model of ZFC. (It's equivalent to a Boolean-valued model.)
Mike Shulman (May 14 2024 at 21:07):Ahh, phooey, you're right. I forgot that ETCS includes the well-pointedness axiom (4), which implies two-valuedness, since it's such an unnatural thing topos-theoretically.
Mike Shulman (May 14 2024 at 21:09):And I guess that does imply that any subtopos of a model of ETCS that's also a model of ETCS must have the same subobject classifier, since the map is a bijection on global elements and hence an isomorphism.
Mike Shulman (May 14 2024 at 21:09):But do we know that is well-pointed?
Mike Shulman (May 14 2024 at 21:09):I guess we do, since it's equivalent as a category to .
James E Hanson (May 14 2024 at 21:10):Okay so do you think my argument works?
Mike Shulman (May 14 2024 at 21:11):How do you know that the pulled back indicator function on also classifies ? The indicator function in classifies , the copy of in , but if isn't the identity, how do we know that coincides with in ?
James E Hanson (May 14 2024 at 21:12):Okay so if doesn't have standard naturals, I'm not completely sure this argument is going to work, but if it does then it's just a matter of 'for each n, the bit is the same.'
Mike Shulman (May 14 2024 at 21:13):We did argue that the NNOs of L and V coincide. What more than that does "standard naturals" mean?
James E Hanson (May 14 2024 at 21:14):No non-trivial automorphisms.
Mike Shulman (May 14 2024 at 21:15):What does that have to do with it?
James E Hanson (May 14 2024 at 21:16):and are both functions from to , right?
Mike Shulman (May 14 2024 at 21:16):Yeah. And I think I see how well-pointedness (= "every bit is the same") and the equivalence implies that , but I don't see how automorphisms are relevant.
James E Hanson (May 14 2024 at 21:18):It's a question of how internally definable in the embedding of into is.
James E Hanson (May 14 2024 at 21:20):There are models of with automorphisms that don't fix . This would be an example of a functor from to that isn't equivalent to the identity on the natural numbers object.
Mike Shulman (May 14 2024 at 21:25):Actually, now I think we can prove that the NNOs of L and V' actually do coincide, just like for the subobject classifiers, so it's much easier. I'm thinking that we're working inside ZFC where V is "the" universe of sets, and therefore the elements of the NNO are exactly the finite iterates of following . And the same is true for , which is equivalent as a category to . Now the localization functor is a functor, and by comparing universal properties. So the localization map is a bijection on global elements, hence an isomorphism by well-pointedness.
James E Hanson (May 14 2024 at 21:29):So do you think and agree?
Mike Shulman (May 14 2024 at 21:30):Yes.
Mike Shulman (May 14 2024 at 21:30):So I think I'm convinced now that L cannot contain a copy of V.
Mike Shulman (May 14 2024 at 21:31):My previous fallback guess was that maybe L is a localization of this realizability category, but now I think that's unlikely too since it would be hard to find a good localization that doesn't contain the embedded copy of V. Also, and I guess you meant to make this point earlier too but maybe I missed it, the embedded copy of Set is usually the double-negation sheaves, but L is boolean so it would equal its own double-negation sheaves.
Mike Shulman (May 14 2024 at 21:32):But now I have another suggestion: perhaps L is the "modest sets" in this realizability category.
James E Hanson (May 14 2024 at 21:34):I'm less certain of what I'm talking about here, but L has quotients. Wouldn't that be a problem for being the 'modest sets'?
Mike Shulman (May 14 2024 at 21:35):Ok, maybe the discrete objects?
Mike Shulman (May 14 2024 at 21:35):Perhaps where discreteness is generalized to use ordinals rather than just N.
James E Hanson (May 14 2024 at 21:37):What does discrete mean again? Decidable equality?
Mike Shulman (May 14 2024 at 21:38):In an ordinary realizability topos, the discrete objects are the subquotients of the NNO.
Mike Shulman (May 14 2024 at 21:38):I'm suggesting to instead consider the subquotients of the ordinals, under a suitably canonical embedding of Ord into our realizability category.
Patrick Nicodemus (May 14 2024 at 21:39):Tom Leinster said:
Hi all. I'm coming late to this thread but thought I should say something.
The course I'll be teaching in Edinburgh this autumn, Axiomatic Set Theory, is principally for undergraduates in their last two years. As John says, it'll be a rigorous development of set theory based on the ETCS axioms, but I'll neither assume nor teach the notion of category. The tentative chapter/week headings are:
- Introduction
- The axioms, part one
- The axioms, part two
- Subsets
- Relations
- Coproducts and families
- Number systems
- Well-ordered sets
- The axiom of choice
- Cardinal arithmetic.
I'm really excited to be teaching this course, because as far as I know, nothing like it has ever been done before.
Plus, lots of people -- even category theorists and set theorists -- don't realize it can be done! For example, two people I know who are knowledgeable in both subjects assumed I'd have to get into toposes, and didn't realize it's possible to do everything in a completely elementary way. I want the world to know!
I like to explain this point by analogy with number theory and rings. If you're going to teach an introductory number theory course, you have a choice. You could say "the integers form a ring, number theory eventually needs rings other than the integers, and rings are important throughout mathematics anyway, so I'm going to begin my course by introducing rings and then specialize to the integers". Alternatively, you could say "basic number theory doesn't require the general notion of ring, so let's just talk directly about addition, subtraction and multiplication of integers without ever mentioning rings". Both kinds of course are valuable. The first is like teaching ETCS via the general notion of category, more or less as in Lawvere and Rosebrugh's book Sets for Mathematics. The second is like my course: no categories, just sets and functions done directly.
I'll say almost nothing in the course about membership-based set theories such as ZFC. I'll have to say something, as we're not in a cultural vacuum: some students will already have had some contact with ZFC, and I'll need to address the usual questions. But it'll be kept to an absolute minimum.
On some other points...
I have the same respect for set theory research as I do for any other branch of mathematics. It's a subject full of strange and wonderful things uncovered by brilliant people. What separates set theory from, say, differential geometry or harmonic analysis or semigroup theory is the claim that set theory -- specifically, ZFC -- has a special, central role in the whole of mathematics. Such a claim becomes the business of all mathematicians.
I believe it should be possible to discuss and debate such claims in a calm and constructive way. In fact, I know it is possible: when I wrote a blog post to accompany what was to become my American Mathematical Monthly article Rethinking set theory, there was a fantastic conversation of 200+ comments, involving widely different viewpoints, that was extremely civil and enlightening.
Personally, I've said just about all I want to say about the mismatch (as I see it) between sets as treated in membership-based set theories like ZFC and sets as used in practice by the vast majority of mathematicians. (In a nutshell, it's not so much the ZFC axioms that are the problem, it's the very set-up: that elements of sets are always sets, and that one can always legitimately ask whether one set is an element of another.) I have no desire to have that conversation again. Right now, I'm much more interested in demonstrating what set theory looks like when you develop everything in ETCS.
Regarding my past writings, nothing I've written about sets is intended to be hyperbolic. If something I've said looks like hyperbole, please consider that it's probably my genuinely held opinion, however much you might think it's impossible that anyone could really believe it. Of course, I'm as human as anyone and may sometimes have slipped up. I'm acutely aware of how sensitive these matters are (look at the first few paragraphs of that blog post), I know how deep a personal attachment every mathematician has to their own research area, and I have no desire to hurt or antagonize anyone. So I work hard to avoid overstatement. I want to produce light, not heat -- although I'm aware that sometimes it's impossible to have one without the other.
And this respect for differing views should go in all directions. In particular, grand claims are made for the place of ZFC in mathematics, and it's natural and healthy for those claims to be challenged.
Hi, Tom. As I am responsible for some of the harsh language in this thread I apologize for the vitriol. I think your book on higher categories and higher operads is excellent and I found a lot of value in it. I will try to be less astringent in the future. I hope your class goes well.
James E Hanson (May 14 2024 at 21:40):Mike Shulman said:
I'm suggesting to instead consider the subquotients of the ordinals, under a suitably canonical embedding of Ord into our realizability category.
This sounds plausible to me.
Mike Shulman (May 14 2024 at 21:42):Wow! This would be super-duper awesome if it were true.
James E Hanson (May 14 2024 at 21:43):But it's also probably not going to generalize to other inner models. I don't think there's a 'computational' description of or (for a measurable ultrafilter ).
James E Hanson (May 14 2024 at 21:46):And is important in the construction of Solovay's model.
Mike Shulman (May 14 2024 at 21:47):That only dims my enthusiasm a trifle. I feel like if we can "crack the shell" of inner models categorically by describing the simplest case of L, we can open the door to future attacks on other examples. For instance, a PCA doesn't have to be "computational" in any naive way. Even more so for a tripos, and for the various generalizations of realizability that lots of people have studied. And we could also combine realizability with other categorical constructions like sheaves and ultraproducts.
Mike Shulman (May 14 2024 at 21:53):Maybe that's overly optimistic of me. But in any case, if this is true I think it is really interesting, even if it doesn't turn out to generalize a lot.
Mike Shulman (May 14 2024 at 21:54):So what now? Should I ask on MathOverflow to see if someone already knows whether this is true?
James E Hanson (May 14 2024 at 21:56):It would be a reasonable question.
Mike Shulman (May 14 2024 at 21:56):Ok, I have to leave now, but I'll write up a question probably later today or tomorrow.
Mike Shulman (May 14 2024 at 21:57):(Also maybe we should move the conversation here about ordinal realizability to another topic, since it's not really even tangentially about Tom's course any more.)
James E Hanson (May 14 2024 at 21:57):But also, why is phrasing it like this so much better than just saying 'the category of ordinals with ordinal-computable maps'?
James E Hanson (May 14 2024 at 21:58):Okay but it is related though. If Tom's course is about 'set theory' then proving the relative consistency of adding choice to various set theories is relevant, and the primary way you do this is with L-like constructions.
James E Hanson (May 14 2024 at 21:59):So, I don't think you can really say it's 'not even tangentially' related.
James E Hanson (May 14 2024 at 21:59):I'm going to be honest. I'm still not really happy with this program as a whole. I can't get away from the feeling that it's motivated largely by not accepting that the tools set theorists use are natural for the problems they care about and the things they apply them to.
Verifying that ordinal Turing machines actually capture all of the behavior of L is really involved. It's a lot more work than verifying that L is a model of ZFC in the first place. If you accept the idea that the cumulative hierarchy is a natural concept, which I do, L is also a really natural construction. You're just replacing the power set operation with the 'first-order definable power set' operation.
James E Hanson (May 14 2024 at 22:05):James E Hanson said:
Okay but is related though. If Tom's course is about 'set theory' then proving the relative consistency of adding choice to various set theories is relevant, and the primary way you do this is with L-like constructions.
Even in the presence of urelements, L-like constructions are pretty important. They show up in Barwise's treatement of KP with urelements a lot, for instance.
James E Hanson (May 14 2024 at 23:44):Mike Shulman said:
That only dims my enthusiasm a trifle. I feel like if we can "crack the shell" of inner models categorically by describing the simplest case of L, we can open the door to future attacks on other examples. For instance, a PCA doesn't have to be "computational" in any naive way. Even more so for a tripos, and for the various generalizations of realizability that lots of people have studied. And we could also combine realizability with other categorical constructions like sheaves and ultraproducts.
(Let me know if you think this should be in another thread. I feel a little awkward starting a new thread because I am admittedly being explicitly argumentative right now.)
I'm probably being unfair to you since you did just learn about these ideas, but let me ask you this, if I had responded to David's message like this
A constructible function between ordinals is precisely one which is -definable (with parameters) in .
would you have been nearly as excited? Maybe it doesn't feel like as much of a characterization, but it is equivalent to what I said. The way you show the close relationship between ordinal computation and is by showing that there is an ordinal Turing machine that computes the -diagram of (relative to some canonical bijection with ). is a model of ordinal computation and it's a better, more usable model than the others I listed. (Part of the reason I'm comfortable claiming this is that it's the language that -recursion theory, the generalization of computability/recursion theory that studies of this kind of ordinal computation, is phrased in.) And to me part of what makes it more usable is precisely the fact that it is more 'structural' and less 'material' than things like ordinal Turing machines.
Of course maybe you could say we should go even more structural than this, and I am sort of pondering a 'type theory for ordinal computation' in my head right now, but it just ends up feeling like a microcosm of the rest of the conversation. The behavior of -recursions theory is really shaped by the interplay between the Löwenheim-Skolem theorem and Mostowski collapse. Gödel's condensation lemma is absolutely fundamental to understanding ordinal computation, and I just don't think it's going to be nearly as natural in something with more semantic bells and whistles than a ZF-like set theory.
David Michael Roberts (May 15 2024 at 00:37):Cool, good to see progress on this!
David Michael Roberts (May 15 2024 at 00:41):I found out after a naive question on math.SE that we can get Def(\alpha) just from looking at its well-order structure, not that it is a ZFC set, and that it gains a canonical well-ordering. This makes me think I would revise my hopes upward from looking at Ord inside Set_L and all the constructible functions between ordinals, but looking at all well-orders, and the definition of "Def" of a well-order that agrees with the usual Def on ordinals.
Mike Shulman (May 15 2024 at 01:25):A constructible function between ordinals is precisely one which is -definable (with parameters) in
I wouldn't have been as excited about that characterization because I wouldn't have known that it was equivalent to some kind of computability, and therefore wouldn't have guessed that it might be expressible as a realizability construction. But that's just due to my ignorance.
Mike Shulman (May 15 2024 at 01:30):In general, I feel like it is a good thing in mathematics when we discover a new connection between two different areas. It allows the tools and ideas of each area to be brought to bear on the problems of the other. I think having multiple descriptions of an object is always good; especially when each of them is "natural" in its own context, it nearly always turns out that there are some applications for which each is better-suited than the other. And the more work it takes to establish the equivalence between two things, the more likely that equivalence is to be useful: a trivial rephrasing of something isn't likely to enable you to do much that you couldn't do just as well with the original definition.
In particular, I am instantly suspicious of anyone claiming that one model of something is unequivocally better than another.
David Michael Roberts (May 15 2024 at 01:31):Someone pointed out on math.SE I had a misapprehension about how the powerset in L works. @James E Hanson is given , is there a stage by which ?
James E Hanson (May 15 2024 at 01:46):David Michael Roberts said:
Someone pointed out on math.SE I had a misapprehension about how the powerset in L works. James E Hanson is given , is there a stage by which ?
Yes there is such a , but I think it's a little bit subtle how behaves as a function of .
James E Hanson (May 15 2024 at 01:47):But such a must exist (if the ambient theory is ZF) because satisfies ZFC including the power set axiom and .
James E Hanson (May 15 2024 at 01:50):So in particular, I believe it will occur in , where is computed in , but this can differ pretty wildly from computed in . The only real restriction is that .
David Michael Roberts (May 15 2024 at 02:44):Bleh. That's a mess! (sorry (-: )
James E Hanson (May 15 2024 at 05:56):It really isn't.
James E Hanson (May 15 2024 at 05:58):I would say this is pretty on par with most technical mathematics.
David Michael Roberts (May 15 2024 at 07:41):Well, as opposed to eg or . As a non-expert it looks like an unexplained mess, but I could perhaps vaguely intuit what part of the ordinal index tell me. If I really needed this, I wouldn't use the sharp estimate, but any old upper bound.
James E Hanson (May 15 2024 at 14:33):For a lot of ordinals you're going to have that , but I don't remember an exact characterization of this condition. On the other hand, the impredicative cardinal successor operation is going to be necessary for this (and in some sense the characterization I gave is almost by definition). Something weird and interesting about the construction is that when you're 'inside it,' you can't really tell whether you've found all of the subsets of a given set that are ever going to show up. There can be countable ordinals such that . This means that there will be some where it looks like you've seen all of the real numbers and all of the countable ordinals and so on, but then suddenly much later you find a bijection between and or something like that.
James E Hanson (May 15 2024 at 14:37):And this is also something that's going to be visible pretty directly on the level of ordinal Turing machines too. If I'm remembering how some of these things work correctly, you can make an ordinal Turing machine that looks for a computable bijection between a given ordinal and . (Unlike with ordinary Turing machines, checking that a given computable map is a bijection is something that you can check computably, and just like with normal Turing machines you can run a parallel search on all ordinal Turing machines.) If you run this ordinal Turing machine it might eventually halt or it might just keep looking forever, and there's no way to really check for this in a bounded amount of time.
James E Hanson (May 15 2024 at 14:46):So basically, to put it another way, part of the reason it's messy is that the –power set operation isn't computable. It's really only 'semi-computable' in that eventually you stop finding new subsets.
The fact that you stop finding new subsets relies on a bit of impredicativity in the ambient universe, such as the power set axiom or some amount of replacement, and it doesn't happen in weaker contexts like KP. is a model of KP and in it new reals keep showing up all the way up to .
James E Hanson (May 15 2024 at 17:32):Tom Leinster said:
I'm acutely aware of how sensitive these matters are (look at the first few paragraphs of that blog post), I know how deep a personal attachment every mathematician has to their own research area, and I have no desire to hurt or antagonize anyone.
Professor Leinster, hopefully I am being civil (and I did sleep on this draft as you suggested in your blog post), but there's a part of Rethinking set theory where I really feel that you did not do academic due diligence when presenting your case. Near the end, when discussing possible downsides for a student going into set theory learning ETCS first, you say
A second disadvantage is that any student planning a career in set theory will need to learn ZFC anyway, since almost all research-level set theory is done with the iterated-membership conception of set. (That is the current reality, which is not to say that set theory must be done this way.)
Obviously your article isn't about research into pure set theory, it's about trying to improve the relationship between set theory and the rest of mathematics. As Mike pointed out, what you're doing could be a nice bridge for non-set-theorist mathematicians to engage with set theory more. And, to be clear, mathematicians and set theorists should stop saying that ZFC is 'the foundation of mathematics,' and set theorists should broaden their horizons, but by presenting no substantive devil's advocate argument for why set theorists might not really get that much out of ETCS, you rhetorically leave open the implication that there might be no good reason at all that set theorists tend to study material set theories rather than structural set theories. This is obviously possible prima facie, but as I've been discussing with Mike, I feel like there's pretty ample evidence at this point that there is more to the fact that set theorists haven't switched to ETCS(+R) than just cultural inertia.
When you put out Rethinking in 2012, Lawvere's paper on ETCS was already 48 years old. Gödel's L construction, one of the first spectacular results of set-theoretic metamathematics, was 74 years old. As we are currently discussing right now, it's an open research problem to find the 'correct' categorical presentation of L. L is an extremely important tool in set-theoretic metamathematics (and it shows up a surprising amount in computability theory and reverse math too). It really is no exaggeration to say that it is the beginning of the story of modern set theory research. For instance, it plays a major role in Saharon Shelah's 1974 proof that the Whitehead problem is independent of ZFC (and therefore independent of any theory ZFC can 'reasonably' interpret, such as classical HoTT).
How would you propose presenting Solovay's 1970 construction of a model in which all sets of reals are Lebesgue measurable? The standard presentation of this construction involves passing to a HOD-like inner model, and HOD is even more tied up in the iterative-set concept than L is. This is a pretty big result in set theory that mathematicians outside of set theory care about; it's not an esoteric question about premice and fine structure of large cardinals. If a student asks about this result in your class, what are you going to say? "Sorry, we haven't been able to crack that nut yet, just give us a few more decades"?
To give another example, consider this type theory paper by Fiore, Pitts, and Steenkamp. In order to establish the expressiveness of quotient-inductive types, this paper cites Blass's result that (under some large cardinal assumptions) it is consistent with ZF that there is an infinitary equational theory with no initial algebra in ZF. Blass's result relies in an essential way on Gitik's famous 1980 result of the consistency of all uncountable cardinals being singular (relative to some large cardinals). This is a pretty technical class forcing result that frankly type theorists and categorical logicians don't seem to be even remotely equipped to prove. (And to be clear, that's obviously fine; type theorists and categorical logicians have their own stories that they're exploring. Set theorists aren't remotely equipped to prove plenty of things too.) But the only formal work I can find about class forcing over toposes is talk notes by David from 2018 about trying to make topos class forcing work and I get the definite impression from those notes that it's just very hard and unclear how to proceed. Maybe David will let us know if he's made more progress on this, but as far as I can tell nothing more has really been written about it.
For me, it's hard to not sit back and feel like it's somewhat intuitively obvious why these things are so difficult. With toposes in particular, some of it has to be working constructively, but a big part of the difficulty is that ETCS and topos theory eschew most of the global 'scaffolding' that is present in ZF-like set theories. What makes L-like constructions a complete pain in more structural theories like Z and second-order arithmetic is that you need to locally build this scaffolding everywhere, instead of having it all in one uniform structure. This scaffolding might not be categorically natural, but it's extremely useful for doing detailed global constructions like inner models and class forcing. One could almost think of models of ZFC as a 'normal form' for models of ETCS+R. Admittedly this scaffolding doesn't need to take the form that it does in ZFC, as I already discussed, but it is still seemingly fundamentally at odds with the categorical mindset, since when you build a set-theoretic universe 'brick-by-brick,' you build many redundant isomorphic copies of the same set which nevertheless 'live at different places in the scaffolding.'
Given the general stigma against set theory in mathematics and the frankly toxic rhetoric coming from some of the people criticizing set theory and set theorists and given the fact that an extremely common element of that criticism is the very same junk theorem argument you hold up as the fatal flaw of ZF-like theories, I feel like you have some amount of academic responsibility to address these points when criticizing the main object that set theorists are studying, regardless of the legitimacy of the junk theorem argument in the context of practical usability. Despite working with a system riddled with 'nonsense' like and despite not using the 'correct' understanding of forcing, nobody seems to be able to get as far with these kinds of classical metamathematical questions as set theorists studying ZF-like theories. One can always say 'well it doesn't need to be this way, set theorists could be working in a different system, they could be using toposes or ETCS,' but after some number of decades of struggling to translate basic tools of pure set theory research, I feel like maintaining this edges into the territory of not respecting the intellectual autonomy of the field.
Tom Leinster (May 15 2024 at 19:14):Thanks, @Patrick Nicodemus , very much appreciated.
David Michael Roberts (May 15 2024 at 20:38):Re my notes on class forcing: I had a break from academia at the time of that talk, and, now I am working in industry. My main research is not on set theory, but geometry. I've wanted to write that paper for a long while, but I haven't found the time. And I want to write it in more general terms than classical logic. Were that my main area of research it would have been published by now!
Mike Shulman (May 15 2024 at 20:51):I asked the MO question: https://mathoverflow.net/q/471344/49
David Michael Roberts (May 16 2024 at 12:32):@James E Hanson is there an analogue for , like there is for , whereby we know which stages are models for (at least) Z? I think I've read one could take something like , but I don't want that. Clearly L is the "narrowest" model of ZFC with the same ordinals, but can we shrink the _height_ at the cost of getting a model of merely Z?
David Michael Roberts (May 16 2024 at 12:55):Hmm it seems that for a regular cardinal, satisfies (roughly) ZFC-Powerset. But this is really getting off-topic, and I should not clog up the thread too much with my musings!
Tom Leinster (May 16 2024 at 16:29):In case my opinion matters, I'm extremely happy for this conversation on L to continue in this thread!
Tom Leinster (May 16 2024 at 16:37):@James E Hanson -- thanks very much for your considered response (and please, call me Tom).
Again, I think this is a matter of differing viewpoints rather than bad faith. You quoted from the paragraph of my paper where I was discussing potential disadvantages of teaching ETCS:
almost all research-level set theory is done with the iterated-membership conception of set. (That is the current reality, which is not to say that set theory must be done this way.)
The parenthetical comment was mainly to clarify that the "is done" of the previous sentence wasn't intended to be normative. In other words, I didn't want to give the impression that just because set theory research is done a certain way, it necessarily follows that it has to be. I was just making the mild statement that I'm not taking a position on the matter.
If I'd thought it was established beyond reasonable doubt that set theory research could only be done in an element-based way, then I guess I wouldn't have added that parenthetical sentence. But I wasn't convinced of that, and I'm still not, which is where our views differ.
(Also, if I'd known of a good source making the kind of argument you're making here, then I should perhaps have cited it; but I didn't.)
I think you know the following, but just to be extra clear for anyone else reading: I don't claim that all set theory can be done nicely in a structural way. I simply don't know. I think it's an interesting question well worth exploring. You may be absolutely right, and it may be that research-level set theory really isn't viable without adopting a membership-based or material viewpoint. But I, personally, am not yet convinced of that.
So, why am I not convinced?
First, because human beings are ingenious, and I think it's rash to rule out a possibility. Maybe there's even a fantastic way of doing set theory that's neither material nor structural, but unlike anything any of us have thought of.
Second, from the results on the close relationship between ZFC and ETCS+R, we know that any argument about ZFC can be turned into an argument about ETCS+R. (Thank you, by the way, for correcting my usage of "biinterpretable".) The question then becomes the more subjective one of whether it seems "natural" or "helpful" to do things in ETCS+R.
Of course, not all of set theory is about ZFC. There must be many questions in set theory research that no one would claim can be helpfully addressed in a structural way, because they're specifically element-based in nature. The directions taken in set theory research, the questions asked and the problems regarded as important by its practitioners, have surely been shaped by the dominant material viewpoint. Different directions would have been taken and prioritized if the structural viewpoint had been dominant. And that's another sense in which I'm not convinced that set theory research can't be done structurally: if it were, we'd be asking and answering different questions.
I'm entirely open to the possibility that you're right: that there are results in set theory, of direct relevance to parts of mathematics outside logic, where the material approach is really the only sensible one. You mention Solovay's result on Lebesgue measurability and Shelah's on the Whitehead problem. Personally, I've never read their proofs, so I'm in no position to pronounce on whether or not they could be done in a nice structural way. That's why I'm keeping my mind open and remaining noncommittal.
(Incidentally, I'd give them same "I don't know" answer to a student, in the unlikely event that anyone asked. I should emphasize that my course is for undergraduates and so relatively basic. The intended climax is that for infinite sets and , which is obviously miles off the kind of thing we're discussing now.)
The question of how well set theory can be done structurally seems to me to be very much worth investigating. My own little contribution was to spend a couple of months learning some stuff about large cardinals (new to me at the time), understanding everything structurally, then writing up my understanding in a series of blog posts. The first one begins like this:
My primary interest is not actually in large cardinals themselves. What I'm really interested in is exploring the hypothesis that everything in traditional, membership-based set theory that's relevant to the rest of mathematics can be done smoothly in categorical set theory. I'm not sure this hypothesis is correct (and I suppose no one could ever be sure), which is why I use the words "hypothesis" and "explore". But I know of no counterexample.
I'm well aware that everything covered in that series would be regarded as utterly basic by a set theorist, but that was as much as I had the energy to learn (and 13 posts seemed like enough). It would be excellent if someone else, ideally someone with a more suitable background than me, took it further.
About L specifically: I do think it would be great to have a structural account of L -- or a really compelling explanation of why that's impossible. And I do think it's a major gap that we don't have either already. So, I'm glad to see the conversation between you and Mike. It could be that there's a structural account of L that's much more than a mere translation of standard material, involving some new angle or thought-provoking new idea. Obviously I don't know. But I'm open to the possibility.
What I find least convincing in your argument is the part about the passage of time. It seems to me that it's quite common in mathematics that something could have been done decades ago and hasn't been. For instance, the course on ETCS I'm about to write could have been done 50 years ago. But as far as I know, it'll be a first.
We can speculate on the reasons why ETCS has been widely misunderstood and, arguably, underdeveloped. Some of the responsibility probably lies with category theorists for not communicating well enough with the rest of the world. Another reason is that if anyone was to have found a categorical account of L (for example), it would probably have been topos theorists -- but topos theorists tend to be interested in other things. To them, an ETCS category is a very, very special kind of topos, and usually their attention is on a much more general context.
Over the last year or two, I've asked several category theorists about L, or more specifically about the status of the result that GCH is consistent with ETCS. One distinguished topos theorist gave me the impression that they didn't regard it as an interesting question. I do! Of course, everyone's free to find any topic uninteresting, and that's different from saying something's unimportant or not worthwhile. (I can't honestly claim cancer research as an interest of mine, but I'm very glad it's being done.) If this topos theorist's attitude is at all representative, that does begin to suggest why the question of a categorical account of L hasn't received much attention. There's just a difference in what people find interesting.
There's also the matter of incentives. Many mathematicians have lamented that our academic system doesn't give enough reward to people who find new ways of looking at old results. It's too winner-takes-all. Suppose, for instance, that someone wanted to embark on the project of taking Shelah's massive body of work on pcf theory and trying to do it structurally. It would require a huge investment of time, and what would the reward be? Just about the best case: they succeed, set theorists say "we knew all that already", and hiring committees say "they haven't proved anything new". Maybe that's a slight exaggeration: it could be that new light is genuinely shed, as in the categorical approach to forcing. But hopefully you see my point: it would be a very risky venture in terms of career.
There's more to say, but I don't want to ramble on forever, so I'll leave it there for now. Thanks for the conversation so far.
James E Hanson (May 16 2024 at 16:40):David Michael Roberts said:
James E Hanson is there an analogue for , like there is for , whereby we know which stages are models for (at least) Z? I think I've read one could take something like , but I don't want that. Clearly L is the "narrowest" model of ZFC with the same ordinals, but can we shrink the _height_ at the cost of getting a model of merely Z?
So, we'll know this to some extent but there really can't be a simple description of it. In some sense this is because the relationship between and can be quite complicated. There is a club (closed, unbounded set) of ordinals at which . (Also note that by the absoluteness of rank.)
Any (infinite) -cardinal (where by cardinal I mean initial ordinal of a given cardinality) should have this property and any -cardinal is also an -cardinal, but there will in general be more -cardinals than -cardinals.
But the other thing is that there will be 's at which is a first-order model of various fragments of ZFC, such as Z, but isn't a second-order model (relative to ). In fact there will be many countable ordinals at which .
James E Hanson (May 16 2024 at 16:53):There will in fact be many countable ordinals at which 'thinks' it's a model of Z containing or whatever other enormous definable cardinal you choose. Moreover we can replace Z with any finite fragment of ZFC (and more if there are large cardinals around). This is an example of the interplay between the Löwenheim–Skolem theorem and Mostowski collapse. For any big uncountable , there are many smaller with the property that 'looks like from the inside.'
Madeleine Birchfield (May 16 2024 at 21:05):Tom Leinster said:
Hi all. I'm coming late to this thread but thought I should say something.
The course I'll be teaching in Edinburgh this autumn, Axiomatic Set Theory, is principally for undergraduates in their last two years. As John says, it'll be a rigorous development of set theory based on the ETCS axioms, but I'll neither assume nor teach the notion of category. The tentative chapter/week headings are:
- Introduction
- The axioms, part one
- The axioms, part two
- Subsets
- Relations
- Coproducts and families
- Number systems
- Well-ordered sets
- The axiom of choice
- Cardinal arithmetic.
I'm really excited to be teaching this course, because as far as I know, nothing like it has ever been done before.
Is there a rationale for not including the axiom of replacement in the set theory? Plenty of mathematics uses replacement - for example, Peter Scholze has said that some of the theorems from condensed mathematics aren't provable without replacement. In addition I believe that Lawvere's original paper on ETCS talks about the axiom of replacement.
David Michael Roberts (May 17 2024 at 00:15):James E Hanson said:
There will in fact be many countable ordinals at which 'thinks' it's a model of Z containing or whatever other enormous definable cardinal you choose.
Is this a problem? I don't have some kind of platonic urge to have some small 'inner model' (abusing terminology slightly) of Z agree with what the ambient set theory says about what sets are isomorphic to other sets power sets or not. All this tells me is that the inclusion of the topos of sets into the topos of sets doesn't preserve powerset (I hope at the very least it preserves functions, and composition!). One can then ask what operations on sets it does preserve up to isomorphism, for instance disjoint unions (unobjectionable), quotients by relations (less obvious to me), finite products (perhaps tricky, esp for infinite sets).
I don't even need to know all the ordinals where the stages are models of Z, just some club. This is not at this stage about understanding fine structure, but just trying to build the class as some kind of union, no matter how coarse, using —I hope!—purely structural aspects of ordinals and what we can glean about properties of the categories of -sets.
To connect this to what you and Mike were saying, if we can describe those toposes of sets using even a more restricted notion of computability than the full ordinal computability (where we restrict to some nice club of cardinals where everything has the nicest possible properties), and also the inclusion functors, then taking the colimit of categories we can ask: is it a model of ETCS? (it should be, as sets give one) And then ask questions about GCH etc.
James E Hanson (May 17 2024 at 00:18):David Michael Roberts said:
James E Hanson said:
There will in fact be many countable ordinals at which 'thinks' it's a model of Z containing or whatever other enormous definable cardinal you choose.
Is this a problem?
It's not a problem. I'm just trying to paint a picture of how complicated the behavior of as a function of is.
James E Hanson (May 17 2024 at 00:19):If you just need a club I think that the uncountable -cardinals should suffice.
James E Hanson (May 17 2024 at 00:20):The way quotients (of equivalence relations) and products are coded in set theory is fairly absolute, so I suspect they should be preserved by the embedding of into .
David Michael Roberts (May 17 2024 at 00:31):OK, so if are uncountable cardinals (in ), then it would be super awesome if the inclusion (or rather the inclusion of the corresponding categories of sets, where the functions are those in the corresponding stage) preserved quotients, disjoint unions and finite products.
James E Hanson (May 17 2024 at 04:50):David Michael Roberts said:
OK, so if are uncountable cardinals (in ), then it would be super awesome if the inclusion (or rather the inclusion of the corresponding categories of sets, where the functions are those in the corresponding stage) preserved quotients, disjoint unions and finite products.
Does the inclusion of into normally satisfy this?
By the way, there's also a fairly generic argument that the class of ordinals for which is a club.
David Michael Roberts (May 17 2024 at 07:37):Well, you have to check that given sets and in and their usual cartesian product in , then functions in in are still in bijection with pairs of functions and (again in ). This should be alright, no?
Tom Leinster (May 17 2024 at 16:46):@Madeleine Birchfield wrote:
Is there a rationale for not including the axiom of replacement in the set theory?
The course is a prescribed length, which means that lots of interesting topics have to be omitted. Replacement is one of them.
If I had more time, I would introduce and discuss replacement, although whether I'd include in the core axioms is another matter. In any case, it's a moot point.
Peter Scholze has said that some of the theorems from condensed mathematics aren't provable without replacement.
I'd be interested in reading Scholze's comments on that. Could you give me a reference?
James E Hanson (May 17 2024 at 23:11):David Michael Roberts said:
Well, you have to check that given sets and in and their usual cartesian product in , then functions in in are still in bijection with pairs of functions and (again in ). This should be alright, no?
I have difficulty seeing how this wouldn't work.
James E Hanson (May 17 2024 at 23:38):Tom Leinster said:
it could be that new light is genuinely shed, as in the categorical approach to forcing.
I am going to ask a fairly contrarian question. What new light is actually shed on forcing by the categorical perspective, especially in the context of Boolean toposes? This is a really common piece of rhetoric coming from category theorists and I'm not really all that convinced by it. While it is true that in the context of toposes forcing generalizes significantly to the broader notion of sheaf toposes, this generalization is seemingly orthogonal to what classical mathematical logicians do with forcing and doesn't seem to shed all that much light on other directions of generalization, such as priority arguments in computability theory.
Matteo Capucci (he/him) (May 21 2024 at 12:30):In my extremely modest experience, forcing was completely alien and unapproachable until I was taught it in terms of Boolean models. Ergonomicity and insight are pretty useful traits, and moreover I was able to understand realizability models with little to no extra effort. Generally speaking, structural theories seem to be pretty good at taming complexity.
Patrick Nicodemus (May 21 2024 at 12:45):Matteo Capucci (he/him) said:
In my extremely modest experience, forcing was completely alien and unapproachable until I was taught it in terms of Boolean models. Ergonomicity and insight are pretty useful traits, and moreover I was able to understand realizability models with little to no extra effort. Generally speaking, structural theories seem to be pretty good at taming complexity.
Boolean valued models seem to be standard though, like the Scott-Solovay paper is widely influential in set theory and Jech covers Boolean models.
So I don't think what you're saying is really controversial, I won't speak for James but I am pretty sure set theorists widely recognize the importance of boolean valued models. I don't follow how that relates to "structural theories" though
Mike Shulman (May 21 2024 at 18:35):Set-theoretic Boolean-valued models are better than other kinds of set-theoretic forcing, but I still find them pretty alien and unapproachable compared to sheaves.
Mike Shulman (May 21 2024 at 18:38):This feels to me a lot like the arguments that category theorists had with mathematicians in other fields in the late 20th century. People would look at category theory and say "it's just a different language for saying things we already know" and "there aren't any real theorems you prove with category theory". But after the ideas of category theory percolated sufficiently, people began using that language to say things and prove theorems that they wouldn't have been able to think of previously, even if in principle it would have been possible to state and prove them without category theory.
Todd Trimble (May 21 2024 at 19:07):people began using that language to say things and prove theorems that they wouldn't have been able to think of previously
This reminds me of something Rota said, in his Indiscrete Thoughts:
“What can you prove with exterior algebra that you cannot prove without it”? Whenever you hear this question raised about some new piece of mathematics, be assured that you are likely to be in the presence of something important. In my time, I have heard it repeated for random variables, Laurent Schwartz’ theory of distributions, idèles and Grothendieck’s schemes, to mention only a few. A proper retort might be: “You are right. There is nothing in yesterday’s mathematics that could not also be proved without it. Exterior algebra is not meant to prove old facts, it is meant to disclose a new world. Disclosing new worlds is as worthwhile a mathematical enterprise as proving old conjectures.”
Patrick Nicodemus (May 21 2024 at 19:30):That's a beautiful quote. It's a good general philosophy to adopt. However, I don't think it is helpful to throw around such quotes when people are asking questions about what category theory is good for, as it amounts to saying "You just don't get it."
I think it is more helpful to talk in direct concrete language about what it is that category theory gives you. "Disclosing new worlds" is not a concrete and specific thing, the Yoneda lemma is.
Direct concrete examples will, I think, help to avoid the feeling of staleness that Mike Shulman was referring to in the repetition of discussion, as we may learn some interesting new mathematics.
Todd Trimble (May 21 2024 at 21:34):My narrow focus here was simply to respond, positively, to what Mike wrote, as opposed to engaging in the general discussion about forcing, which frankly I haven't studied deeply enough.
James E Hanson (May 22 2024 at 00:45):Mike Shulman said:
Set-theoretic Boolean-valued models are better than other kinds of set-theoretic forcing, but I still find them pretty alien and unapproachable compared to sheaves.
And I find sheaves pretty alien and unapproachable because I don't use categorical language on a regular basis in my actual research.
I am not saying that I think category theory isn't useful or that it doesn't have any real theorems or even that classical mathematical logicians couldn't possibly benefit from phrasing some things in terms of category theory a bit more. In more than one model theory talk I've been in in the last couple of years, I have found myself thinking 'wouldn't this be a lot easier to phrase as a functor?' I've actually been spending a fair amount of time trying to think of applications of category theory in classical model theory; although honestly I still haven't come up with much yet.
I am, however, saying that just because something can be phrased in categorical language doesn't make the categorical perspective automatically more practical or more insightful. It is true that Boolean-valued models are a useful language for proving certain general facts about forcing in set theory, but my impression is that set theorists generally consider the forcing poset perspective to be more practical for actually building forcing notions and reasoning about their behavior, and this has really been my personal experience too.
As evidence of this preference among set theorists, consider the Handbook of Set Theory Volume 1. My cursory search through the document indicates six instances of the phrase 'Boolean-valued' or 'Boolean-values,' but 98 instances of the phrase 'forcing poset.' On page 32 in the introduction, Kanamori also writes:
Still, the view of forcing as a way of actually extending models held the reservoir of sense and the promise of discovery, and after Shoenfield popularized an approach to the forcing relation that captured the gist of the Boolean-valued approach, forcing has been generally cast as a matter of partial orders and generic filters.
He then goes on to discuss how the Boolean perspective is still valuable in that it motivated a lot of ideas used in the context of forcing posets and is useful for certain kinds of proofs about the relationship between different forcing posets.
In the context of something like Levy collapse, thinking about a poset of finite partial functions on some set just requires less conceptual overhead than thinking about the Boolean algebra of regular open subsets of a poset of finite partial functions. Admittedly some of this probably has to do with working in a 'fairly degenerate' case (as Mike phrased it earlier), but this is the only case that matters classically and mathematics is full of examples of specialized tools and perspectives for special cases. Moreover, these classical independence results sill establish independence in the wider context of toposes and constructive mathematics. Whenever a statement is proven to be independent of ZFC, it's also automatically shown to be unresolvable in the context of the internal theory of toposes as well. Shelah's theorem about the independence of the Whitehead problem is a stronger theorem because it is phrased in terms of ZFC and not toposes.
The problem with trying to apply Rota's quote to the context of this conversation is that Boolean-valued models are not a new idea, and they're not even an idea that wholly originated outside of the context of set theory itself. (Boolean-valued models were independently invented by Scott and Solovay. Scott obviously has roots in category theory, but Solovay doesn't.) ETCS and topos theory are also not new ideas. At some point in order to maintain that a more categorical perspective is probably going to be more practical or more insightful in the context of research questions that set theorists care about in particular, you need to explain why working set theorists haven't taken to these more categorical perspectives for the last 50 years despite these ideas being fairly well-known in the field. Some of this could be explained by cultural inertia to be sure, but I do not accept the idea that it is just cultural inertia.
Todd Trimble (May 22 2024 at 01:11):The problem with trying to apply Rota's quote to the context of this conversation
Once more: I was not "trying" to do that. See my response to Patrick. Mike reminded me of something, that's all.
Hell, I'm not even taking sides (although if pressed, I find the explanations I've read about forcing more congenial when cast in the language first set out by my PhD adviser, Myles Tierney). Clearly it was a mistake for me to say anything.
James E Hanson (May 22 2024 at 01:24):Todd, I apologize for criticizing your comment directly. It just fit into part of what I perceive to be the broad disagreement in this thread.
Mike Shulman (May 22 2024 at 01:25):James E Hanson said:
thinking about a poset of finite partial functions on some set just requires less conceptual overhead than thinking about the Boolean algebra of regular open subsets of a poset of finite partial functions.
As I already said, it seems to me that the "forcing poset approach" just means working with arbitrary sites rather than completing them to some kind of locale. This is a perfectly category-theoretic thing to do that topos theorists do all the time, so I don't find this particularly compelling as an argument against taking a topos-theoretic perspective on forcing.
James E Hanson (May 22 2024 at 01:27):The problem is that phrasing it in terms of sites requires bringing in a bunch of categorical machinery that doesn't really seem to be that useful in the context of set theory. This is just a different kind of unneeded conceptual overhead.
Mike Shulman (May 22 2024 at 01:28):I think we're going to have to agree to disagree.
James E Hanson (May 22 2024 at 01:30):I know what your stance is, but how do you explain the lack of adoption of this viewpoint in set theory research?
James E Hanson (May 22 2024 at 01:31):Why should set theorists talk about covering relations on categories when the only categories they need to care about for their context are posets and the only covering relation is the double negation topology? All of that generality is degenerate in the context of classical set theory.
Mike Shulman (May 22 2024 at 01:45):I think it's hard to overestimate the power of cultural inertia. For instance, here in the U.S. we still use imperial units in daily life. (-:O
Todd Trimble (May 22 2024 at 02:11):James E Hanson said:
I know what your stance is, but how do you explain the lack of adoption of this viewpoint in set theory research?
I would guess that in large part it comes down to different training, different cultures.
Todd Trimble (May 22 2024 at 02:11):Once category theorists began investigating topos theory, and began getting a sense of what its scope could be, encompassing variously the toposes of algebraic geometry, Kripke semantics, Boolean-valued models, and rather later, realizability toposes, there was a lot of excitement about their unifying power of the concept. Here the emphasis wasn't necessarily on solving problems that the set theorists care about, but perhaps more on a sort of conceptual unification, and (recalling Rota's quote now) the new worlds opened up by considering sets that "vary" over domains in various interesting ways (prescribed by sites in many instances, but there are other ways as well). Synthetic Differential Geometry is an interesting case study in this respect.
Todd Trimble (May 22 2024 at 02:12):Demanding that the success of such broad research programs be gauged by how well they solve the problems that the "specialists" care about sets a very high bar. Since I brought up Rota (my fault!), it seems that he is pointing to other gauges of success than solving problems developed within a certain culture. Category theorists put a lot of stock in conceptual unifications.
Todd Trimble (May 22 2024 at 02:12):(I was enjoying reading this conversation more when there was some excitement over possibilities of gaining a better categorical understanding of L... )
Mike Shulman (May 22 2024 at 02:30):I agree with what Todd said. But also, I think one can't know what categorical techniques might make possible that even specialists care about while the specialists are still resistant to even using the language.
James E Hanson (May 22 2024 at 02:40):Mike Shulman said:
I agree with what Todd said. But also, I think one can't know what categorical techniques might make possible that even specialists care about while the specialists are still resistant to even using the language.
Different fields of math are not that culturally isolated from each other. Grad students talk to each other all the time, and take classes outside of their specialization. Andreas Blass, a pretty classical guy, wrote a few papers on topos theory. Plenty of set theorists know category theory.
I spoke to a couple of young set theorists and a young type theorist about ETCS online in the last week. One of the set theorists studies weak set theories without axioms like choice or foundation and the other has a background in categorical logic and explicitly studied toposes and ETCS in grad school. The type theorist had some earlier background in set theory and is very good at category theory, as far as I can tell. They all agreed that ETCS just isn't a good framework for classical set theory research. The set theorist with a background in categorical logic also talked a bit about how categorical thinking doesn't seem to be a very good fit for set theory, descriptive set theory, and computability theory.
So my question is, what evidence would be sufficient to convince you that set theorists might not actually have all that much use for rephrasing existing set theory in categorical language?
David Michael Roberts (May 22 2024 at 03:14):more insightful.
it depends on who it is insightful for. Knowing that there is this general toolkit developed for algebraic geometry that also explains (or 'explains', if you like) what forcing 'is', in purely mathematical and not set-theoretic/logic terms, is very useful. It opens up understanding the process for more people for whom the whole business of names and generic objects etc rather distant from what they understand.
James E Hanson (May 22 2024 at 03:15):David Michael Roberts said:
more insightful.
it depends on who it is insightful for. Knowing that there is this general toolkit developed for algebraic geometry that also explains (or 'explains', if you like) what forcing 'is', in purely mathematical and not set-theoretic/logic terms, is very useful. It opens up understanding the process for more people for whom the whole business of names and generic objects etc rather distant from what they understand.
I feel like your phrasing here is implying that set theory and logic aren't mathematics. Am I reading too much into your phrasing?
Todd Trimble (May 22 2024 at 03:16):They all agreed that ETCS just isn't a good framework for classical set theory research.
I believe I've heard it said by strong set theorists that in spirit, in practice, contemporary set theory is a vast exploration of the ramifications of well-foundedness and recursion, and this is the point where ETCS is comparatively weak, both in its technical framework and also in its "ontology", for lack of a better word.
Todd Trimble (May 22 2024 at 03:16):That's ETCS. Algebraic set theory (in the sense of Joyal and Moerdijk) probably has a much better handle on such things, and comes closer to capturing intuitions about the cumulative hierarchy.
Todd Trimble (May 22 2024 at 03:17):But again, you (James) seem to be putting the emphasis on problem-solving, doing research on the problems that the set theory culture is interested in. It should be clear this is not where Tom Leinster is coming from, in expounding on ETCS or the version of set theory he is developing for his course. So his interests here are orthogonal to all those concerns within the set theory community.
Todd Trimble (May 22 2024 at 03:17):Put differently: on some level, just about all mathematicians use sets. The vast majority will pick up the basics of naive set theory in a kind of apprentice fashion, without ever really getting into the nitty-gritties at a foundational level, the axioms of ZFC and all that. And they don't need to. And they certainly don't need to think about ZFC sets (as -trees), ever. What they want sets for is to carry out the fundamental constructions they need, like products and quotients and function spaces. What Tom is demonstrating is more pedagogical: sets in the way that mathematicians use them natively can be axiomatized in a way that many of us believe is closer to that native practice.
David Michael Roberts (May 22 2024 at 03:27):James E Hanson said:
David Michael Roberts said:
I feel like your phrasing here is implying that set theory and logic aren't mathematics. Am I reading too much into your phrasing?
Sorry, yes. I should have said 'generic mathematics'—which is a fuzzy term which apparently is supposed to rule out both set-theory-as-foundations and pure CT, and be more like "mathematics that wins Fields medals", Cohen notwithstanding. The whole sheaf-theoretic enterprise was developed by people interested in algebraic geometry, not pure CT. That you can do pure CT on toposes is a subsequent development.
Or more specifically, if you like, 'other kinds of mathematics than set theory, or mathematicians than set theorists'.
Matteo Capucci (he/him) (May 22 2024 at 07:13):Patrick Nicodemus said:
Boolean valued models seem to be standard though, like the Scott-Solovay paper is widely influential in set theory and Jech covers Boolean models.
So I don't think what you're saying is really controversial, I won't speak for James but I am pretty sure set theorists widely recognize the importance of boolean valued models. I don't follow how that relates to "structural theories" though
I was replying to this question of James':
James E Hanson said:
What new light is actually shed on forcing by the categorical perspective, especially in the context of Boolean toposes?
Matteo Capucci (he/him) (May 22 2024 at 07:15):Mike Shulman said:
Set-theoretic Boolean-valued models are better than other kinds of set-theoretic forcing, but I still find them pretty alien and unapproachable compared to sheaves.
Yeah I haven't been fully accurate with my terminology---I forgot Boolean valued models are a thing of their own, but I learned about shef-theoretic forcing basically at the same time so I tend to conflate them. We agree, and my point still applies.
Mike Shulman (May 24 2024 at 21:18):James E Hanson said:
So my question is, what evidence would be sufficient to convince you that set theorists might not actually have all that much use for rephrasing existing set theory in categorical language?
Sorry, it's taken me a while to come up with the right response to this. I think my answer to the question as you phrase it is that I'm already convinced of that, but that I don't think it's the right question. I don't expect rephrasing existing set theory in categorical language would make any of it significantly easier on a technical level, and I don't expect it would be conceptually helpful to many set theorists either, who are used to thinking in 's.
As we've seen in this thread, one can argue that it is conceptually helpful to category theorists trying to understand set theory, and perhaps to at least some other mathematicians (neither category theorists nor set theorists). So, perhaps if set theorists care about publicity for their work, they might find some value in writing some of it in categorical language, even if they don't find it helpful for their personal understanding. I think the evidence for this is pretty strong.
And finally, as in the remark from Rota that Todd quoted, such a rephrasing might help discover new worlds of mathematics at the boundary between set theory and category theory. If you meant to ask what would convince me that this wouldn't happen, then probably the answer is "nothing". How can I be convinced that there isn't something interesting out there waiting to be discovered?
David Michael Roberts (May 25 2024 at 02:05):such a rephrasing might help discover new worlds of mathematics at the boundary between set theory and category theory.
eg a potential structural definition of an L-like model of ETCS
Madeleine Birchfield (May 30 2024 at 01:36):Tom Leinster said:
Madeleine Birchfield wrote:
Peter Scholze has said that some of the theorems from condensed mathematics aren't provable without replacement.
I'd be interested in reading Scholze's comments on that. Could you give me a reference?
It seems like I had misremembered Scholze's comments from a few years ago - he was talking about a particular construction of a well-behaved category of profinite sets, which are in turn used to define condensed sets, rather than proving theorems in condensed mathematics. Then furthermore you had mentioned in a subsequent comment that in that particular case one only needs the existence of beth large cardinals rather than the full strength of replacement:
https://golem.ph.utexas.edu/category/2021/06/large_sets_2.html#c060029
Tom Leinster (May 31 2024 at 18:31):@Madeleine Birchfield Thanks very much for looking into it, in any case.
James E Hanson (Jun 14 2024 at 05:58):@Mike Shulman Mike, I'm sorry for taking so long to respond. I was mulling over what to say and then I had to move to another state for my upcoming position.
The difficulty I'm having is that I feel like you very carefully did not answer the spirit of my question. I certainly could have phrased it in a more precise way, but in my mind my question was not about whether categorical generalizations of things in set theory are interesting or about what language set theorists are merely 'used to thinking in.'
Part of the problem in my mind is that this whole enterprise (rephrasing set theory in categorical language via ETCS and/or topos theory) started from a place of overt hostility towards existing set theory and existing set theorists. Mac Lane and Lawvere decided that they thought set theory was, for lack of a better term, bad. Mac Lane called set theory 'obsolete' and said that measurable cardinals were 'strange.' Lawvere allegedly called set theory 'Bourgeoisie idealism' at one point.
With that in mind, here are my contentions:
So really, here is my question: Do you agree with me? Do you agree that, on the particular topic of set theory, Saunders Mac Lane and William Lawvere were wrong?
Mike Shulman (Jun 14 2024 at 06:47):I'm sorry you felt that I didn't answer the spirit of your question. That certainly wasn't intentional on my part. I did feel at the time as though the question as you phrased it didn't really get to the heart of the matter, but I didn't realize that answering the question literally would sound like I was avoiding the heart.
Mike Shulman (Jun 14 2024 at 06:52):I'm not sure I agree with you about Mac Lane, based on what I've read. Here's a quote from Mac Lane in his 1992 response ("Is Mathias an ontologist?") to Mathias's criticism ("What is Mac Lane missing?"):
...my flashy title "Set theory is obsolete" was intended to draw attention to that remarkable observation by F.W. Lawvere: axiomatics for sets is no longer the only effective way to a foundation--one may instead start with axioms on functions--that is on the category of sets.
I don't know what was actually in the lecture with that provocative title, but here he seems to be saying that he didn't mean that set theory was obsolete as a discipline, only that it was obsolete to regard it as the unique foundation of mathematics. I agree with him there.
More, in his book Mathematics: Form and Function, Mac Lane argued for the theory ZBQC (later called by Mathias "Mac Lane set theory"), which although weaker than ZFC is still written using . And in the paper "Relating first-order set theories and elementary toposes" by Awodey, Butz, Simpson, and Streicher, they write that their -based theory BIST
...fulfils a longstanding wish of Saunders Mac Lane, who often expressed the desire to find a first-order set theory whose notion of set corresponds to that given by elementary toposes.
which also doesn't sound as though he thought set theory was obsolete as a discipline.
Can you give some published quotations supporting your view of Mac Lane's opinion on set theory?
James E Hanson (Jun 14 2024 at 06:58):I cannot, but I also don't really find giving a lecture titled 'Set Theory is Obsolete' and then just apologizing when criticized directly to be an acceptable thing to do. You can't just undo rhetoric that way.
Mike Shulman (Jun 14 2024 at 06:59):I think it depends entirely on what was in the lecture.
Mike Shulman (Jun 14 2024 at 07:00):If the content of the lecture was the same as what he wrote later in the paragraph I quoted, then he was guilty only of using an overly provocative title.
Mike Shulman (Jun 14 2024 at 07:02):I think your quote from the nLab is a bit misleading too. Here's the entire "Idea" section, with some emphasis added by me:
Around the nLab it is believed that higher algebra, homotopy theory, type theory, category theory and higher category theory provide a point of view on Mathematics, Physics and Philosophy which is a valuable unifying point of view for the understanding of the concepts involved.
So at the nLab, we don’t care so much about being neutral. Although we don’t want to offend people unnecessarily, we are also not ashamed about writing from this particular point of view. There are certainly other valid points of view on mathematics, but describing them and being neutral towards them is not the purpose of the nLab. Rather, the nLab starts from the premise that higher algebra, homotopy theory, type theory, category theory and higher category theory are a true and useful point of view, and one of its aims is to expose this point of view generally and in a multitude of examples, and thereby accumulate evidence for it.
If you feel skeptical about the n-point of view, you may want to ignore the nLab. Or you may want to take its content as a contribution to a discussion on what is behind the claim that higher algebra, homotopy theory, type theory, and/or category theory is the right language to describe the world, or at least the world of mathematical ideas.
In particular, among the phrases I emphasized there are three indefinite articles, to contrast with the single definite article in the phrase you quoted, not to speak of the explicit acknowledgment that there are "certainly" other valid points of view on mathematics. And even the phrase you quoted, when read in context, doesn't directly make the claim that these subjects are "the right language" to describe the world. I do agree, now that you bring it to my attention, that this particular phrase is overly broad; but I think that in the context of the entire three paragraphs, it should be clear that the nLab is acknowledging the nPOV as only one among many points of view, but just the one that we are choosing to explore here.
Nathanael Arkor (Jun 14 2024 at 07:08):
- Even if someone were to come up with a satisfactory account of these things today, the fact that translating this basic set-theoretic result with an existing proof took decades is in fact conclusive evidence that Mac Lane and Lawvere were just wrong about set theory.
I don't think that the length of time it takes to obtain a result is indicative of the naturality of a language. For instance, at the very least it depends on the number of people working on the problem. Perhaps you have some indication that this was a hotly pursued topic, but I did not have the impression this was a topic many people were working on? Furthermore, even if many people take a long time to prove a result, I think the naturality of the language should be judged by the eventual outcome, viz. the proof itself. A proof of a known result in a new language might require fundamentally new ideas that lead to an entirely new perspective on the problem, which I believe could justify claims that the language is natural.
(I should say that I'm not making a claim either way about naturality, just that I don't think it's reasonable to judge by this metric.)
James E Hanson (Jun 14 2024 at 07:15):@Mike Shulman There's a gap between the kinds of things people say in careful, professional contexts and the kinds of things people say in more earnest moments. In professional contexts, you're a lot more likely to get the kind of rhetorical hedging that you're highlighting in the nLab article, but I still think that the way people in this space talk about these ideas clearly indicates that people do believe the overly strong statement I highlighted to some extent. I've seen you make grandiose claims like
The point is that if you instead put in the effort to get over the "universal hump" of learning category theory, you end up at a high enough place that you can see over all other humps without any extra effort.
How exactly can you square this kind of statement with what you're saying now?
James E Hanson (Jun 14 2024 at 07:16):If I take your words here at face value, then giving a presentation if L in categorical language should be strictly easier than the existing presentations.
Mike Shulman (Jun 14 2024 at 07:17):I feel like you are taking a lot of phrases out of context. Can you please give a link or citation for that quote?
Mike Shulman (Jun 14 2024 at 07:20):Ah, ok, I found it: https://mathoverflow.net/a/370135/49. And you did indeed omit a crucial piece of context. The full quote is
The point is that if you instead put in the effort to get over the "universal hump" of learning category theory, you end up at a high enough place that you can see over all other humps without any extra effort. (-:O
You omitted the halo smiley face, indicating that my tongue was in my cheek.
James E Hanson (Jun 14 2024 at 07:21):People usually don't make jokes like that unless they believe some kernel of it.
Mike Shulman (Jun 14 2024 at 07:21):The kernel of it that I believe is what you get by replacing "all" with "many" (and perhaps "any" by "much").
James E Hanson (Jun 14 2024 at 07:29):But also, how sure are you that everyone in your community actually gets that that is a joke. I see people make these kinds of ridiculous statements in a deadly serious way all the time. This kind of rhetoric, things like your joke and Mac Lane's lecture title, have a tendency to foster that kind of sentiment in others.
Also I can't help but notice that you didn't really rush to defend Lawvere's alleged statement about set theory. More recently, and in a more concretely demonstrable way, you have people like Paul Taylor, a fairly major figure in the general 'nPOV sphere,' saying completely idiotic things about set theory, literally accusing it of being a religion at times.
How is, say, a student supposed to ingest all of these kinds of sentiments and not develop a bit of a negative attitude about set theory?
Matteo Capucci (he/him) (Jun 14 2024 at 07:30):James, it seems to me you are confusing statements of preference and taste (CT people prefer structuralist foundations like MLTT or ETCS) with judgments of mathematical legitimacy. Idk, perhaps the latter was true in the past but definitely not what I am seeing right now in this conversation. It doesn't seem productive to push this narrative into people's mouth or keyboards, when they are explicitly denying to your face that is what they think...
Mike Shulman (Jun 14 2024 at 07:32):I can't take responsibility for what other people say or believe. I feel like I've been fairly clear about my own beliefs in many places, and anyone who forms an opinion of my beliefs based only on a brief tongue-in-cheek comment on a MathOverflow question deserves what they get.
James E Hanson (Jun 14 2024 at 07:32):It's a delicate line to tread, but I also don't think I'm wrong to criticize this. Not stating these things carefully has a tendency to create people like Kevin Buzzard, who literally never ever bring up set theory in a positive light in any context.
Mike Shulman (Jun 14 2024 at 07:33):I don't think you can blame Kevin Buzzard on category theory, given how seriously he seems to misunderstand univalence. (-:O
David Michael Roberts (Jun 14 2024 at 07:34):Kevin used to say "real mathematics" as code for "mathematics that wins Fields Medals", and he's been open about this. So you can hardly judge his general opinion on this or that specific field
Mike Shulman (Jun 14 2024 at 07:34):I haven't said anything about Lawvere yet because I type at a finite speed and I needed to look up some quotes before commenting, as I did for Mac Lane and the nLab.
David Michael Roberts (Jun 14 2024 at 07:35):And this is orthogonal to any influence category theory has had on him, since he's always moved in the circle of people that proved FLT.
James E Hanson (Jun 14 2024 at 07:38):Consider for example the rhetoric about set theory in the HoTT book. As far as I can tell, there isn't a single positive mention of set theory in the book anywhere, even though the book implicitly uses results (such as Gitik's construction of a model of ZF with no uncountable regular cardinals) proven by set theorists using tools that nobody has been able adapt directly to type theory.
Suppose for the sake of argument you're a mathematician who already has a bit of a negative attitude about set theory. You see people doing formalization work in proof assistants that use type theories and you're told in talks about HoTT that ZFC is 'whacky' (this is an exact quote from a talk about HoTT I attended). You thumb through the HoTT book and only see criticisms of set theory. Now suppose you then find yourself on the hiring committee and a young set theorist's application crosses your desk, and you see that they study something like inner models of determinacy in ZFC. Are you telling me that all of that negativity about set theory and ZFC isn't going to maybe bolster your preexisting negative attitude? Are you saying that this isn't going to maybe embolden you in just ignoring the application?
James E Hanson (Jun 14 2024 at 07:39):This is why I don't find giving talks with titles like 'Set Theory is Obsolete' to be acceptable.
James E Hanson (Jun 14 2024 at 07:41):You can point out that there is an academic difference between preference for foundations and opinions about fields of study if you want, but that doesn't change the rhetorical reality that these kinds of criticisms unless phrased very carefully have a deleterious impact on the reputation of the field of set theory within mathematics.
Mike Shulman (Jun 14 2024 at 07:43):I do think you're on somewhat firmer ground with Lawvere. I can only find one paragraph in his ETCS paper that says anything relevant to this question, but here it is:
...these developments partially support the thesis that even in set theory and elementary mathematics it is also true as has long been felt in advanced algebra and topology, namely that the substance of mathematics resides not in Substance (as it is made to seem when ∈ is the irreducible predicate, with the accompanying necessity of defining all concepts in terms of a rigid elementhood relation) but in Form (as is clear when the guiding notion is isomorphism-invariant structure, as defined, for example, by universal mapping properties). As in algebra and topology, here again the concrete technical machinery for the precise expression and efficient handling of these ideas is provided by the Eilenberg-Mac Lane theory of categories, functors, and natural transformations.
This is not too far from your summary (1), but I still think there are important differences. Lawvere doesn't say that if set theory isn't phrased in terms of category theory it has no content. Rather, it seems to me he's saying that because set theory does have mathematical content, if set theory could only be phrased in terms of , that would give the impression that "the substance of mathematics resides in Substance" (whatever that means); but because he's now shown that set theory can also be phrased in terms of category theory, we are not forced to draw that conclusion.
However, Lawvere does claim here that the substance of mathematics resides not in Substance but in Form. I think at most, ETCS supports the claim that even in set theory, the substance of mathematics could reside in Form in addition to Substance, since it is an alternative to -based theories and in no way "invalidates" them. And I do also get the impression from other writings that Lawvere had an overly optimistic view of the capabilities of categorical set theory vis-a-vis classical set theory research. So on that, I do agree with you. (Although I also agree with Nathanael's response to your point (4).)
James E Hanson (Jun 14 2024 at 07:45):And yes, I do sort of blame the rhetoric from places like the HoTT book for (some of) Kevin Buzzard. He frequently cites the same kind of junk theorem criticism that the HoTT book and Tom's paper on ETCS mentions, but he seems to take it to a much greater extreme where at times it seems like he thinks that junk theorems are what set theorists actually care about.
James E Hanson (Jun 14 2024 at 07:46):Like, where else do you think Buzzard would have gotten the idea that is somehow a fatal flaw of ZFC?
David Michael Roberts (Jun 14 2024 at 07:49):Benacerraf was complaining about things like that simultaneously and independently of Lawvere, and without the particular philosophical baggage that Lawvere brought to the discussion.
James E Hanson (Jun 14 2024 at 07:51):I don't think Buzzard has read Benacerraf. I think Buzzard has talked to a fair amount of people who have studied type theory.
David Michael Roberts (Jun 14 2024 at 07:51):Not to say that Buzzard was reading Benacerraf, but it shows that the idea is not peculiar to the usual players here. The particular example of 3 being a topology on 2 (which I think I have seen him mention) might well have turned up in discussions eg on MathOverflow or the n-Category Café, so it might well be he saw such a thing there.
Mike Shulman (Jun 14 2024 at 07:51):James E Hanson said:
Consider for example the rhetoric about set theory in the HoTT book. As far as I can tell, there isn't a single positive mention of set theory in the book anywhere,
I think this is a totally unreasonable standard to judge by. The HoTT Book is explicitly written to present a new foundation that could be an alternative to set theory. Why would you expect it to go out of its way to say positive things about set theory? A better question to ask is whether it says unjustified or unnecessarily negative things about set theory. I just searched through it for the phrase "set theory" and while I didn't read every word, the most negative remarks I found were things like
In set theory, various circumlocutions are required to obtain notions of “cardinal number” and “ordinal number” which canonically represent isomorphism classes of sets and well-ordered sets, respectively — possibly involving the axiom of choice or the axiom of foundation. But with univalence and higher inductive types, we can obtain such representatives directly by truncating the universe.
which is a factual statement about mathematics.
David Michael Roberts (Jun 14 2024 at 07:58): David Michael Roberts (Jun 14 2024 at 07:58):This example is brought up by an algebraic geometer, and Mike here seems to respond to it as if it was new to him.
David Michael Roberts (Jun 14 2024 at 08:01):This (in 2015) is the oldest example of the phrase "3 is a topology on 2" that Google finds.
James E Hanson (Jun 14 2024 at 08:06):Mike Shulman said:
James E Hanson said:
Consider for example the rhetoric about set theory in the HoTT book. As far as I can tell, there isn't a single positive mention of set theory in the book anywhere,
I think this is a totally unreasonable standard to judge by. The HoTT Book is explicitly written to present a new foundation that could be an alternative to set theory. Why would you expect it to go out of its way to say positive things about set theory? A better question to ask is whether it says unjustified or unnecessarily negative things about set theory. I just searched through it for the phrase "set theory" and while I didn't read every word, the most negative remarks I found were things like
In set theory, various circumlocutions are required to obtain notions of “cardinal number” and “ordinal number” which canonically represent isomorphism classes of sets and well-ordered sets, respectively — possibly involving the axiom of choice or the axiom of foundation. But with univalence and higher inductive types, we can obtain such representatives directly by truncating the universe.
which is a factual statement about mathematics.
I find the implication that von Neumann ordinals are a 'circumlocution' to be obnoxious and hostile.
James E Hanson (Jun 14 2024 at 08:07):In any case it is not a 'factual statement about mathematics.'
James E Hanson (Jun 14 2024 at 08:09):I also find the vague negative reference to the axiom of foundation annoying and particularly rich coming from type theorists. The axiom of foundation is an induction principle.
Mike Shulman (Jun 14 2024 at 08:09):Ok, I guess we disagree there.
James E Hanson (Jun 14 2024 at 08:09):Are you saying that you disagree whether calling it a 'circumlocution' is a 'factual statement'?
James E Hanson (Jun 14 2024 at 08:10):'Circumlocution' is a pretty loaded word, and is not a technical term in any sense.
Mike Shulman (Jun 14 2024 at 08:11):Well, I don't think "circumlocution" is quite the correct word, but I don't think the words I would choose would be less bothersome to you. I find it artificial and unaesthetic to have to appeal to the axiom of choice or the axiom of foundation in order to define "the cardinal number of a set".
James E Hanson (Jun 14 2024 at 08:12):You're literally saying it's artificial to use an induction principle right now.
Mike Shulman (Jun 14 2024 at 08:13):Yes, it's artifical to invoke an induction principle for objects that I don't consider to be inductively defined.
James E Hanson (Jun 14 2024 at 08:13):In any case that is just as much a matter of opinion and not a 'factual statement about mathematics.'
James E Hanson (Jun 14 2024 at 08:14):Or do you disagree?
James E Hanson (Jun 14 2024 at 08:14):But also, you don't need foundation to use von Neumann ordinals. You just need replacement.
James E Hanson (Jun 14 2024 at 08:15):I'm not talking about Scott's trick right now. I'm just talking about von Neumann ordinals.
Mike Shulman (Jun 14 2024 at 08:15):But without the axiom of choice, von Neumann ordinals don't represent all cardinalities.
James E Hanson (Jun 14 2024 at 08:15):I'm not talking about cardinal numbers. I'm just talking about ordinals.
Mike Shulman (Jun 14 2024 at 08:15):I'm talking about cardinal numbers.
James E Hanson (Jun 14 2024 at 08:16):I'm saying that calling von Neumann ordinals 'circumlocutions' or 'artificial' or 'unaesthetic' is obnoxious and hostile to me.
James E Hanson (Jun 14 2024 at 08:17):And not a 'factual statement about mathematics' in any case.
Mike Shulman (Jun 14 2024 at 08:17):Do you agree that the following is a factual statement about mathematics?
In set theory, to obtain a notion of “cardinal number” that canonically represents isomorphism classes of sets one has to use the axiom of choice or the axiom of foundation.
James E Hanson (Jun 14 2024 at 08:20):Well this is the exact same sense of the term 'has to use' that Tom took exception to with regards to replacement and Borel determinacy. There are weak forms of choice and/or weak forms of foundation that are sufficient to allow you to do that. If, say, every set is linearly orderable, then you can build canonical representatives in ZF - foundation. Likewise, if there's only a set of Quine atoms and that's the only failure of foundation, then you can do it too.
Mike Shulman (Jun 14 2024 at 08:21):Okay, sorry for being sloppy. The quote from the book just says "possibly" involving AC or AF, so it covers those variations too. And I don't find those variations any less artificial.
James E Hanson (Jun 14 2024 at 08:23):But is it being artificial a 'factual statement about mathematics'?
James E Hanson (Jun 14 2024 at 08:25):Why is it so hard for you to just agree that it's not a factual statement about mathematics? It is clearly an aesthetic judgement. You used that word yourself.
Mike Shulman (Jun 14 2024 at 08:25):Well, by "factual" I mainly meant to refer to the mathematical fact expressed in my modified quote (suitably un-sloppified).
James E Hanson (Jun 14 2024 at 08:27):This started with you saying that the original quote from the book is a factual statement about mathematics. I do not think it is a factual statement about mathematics. Do you agree?
Mike Shulman (Jun 14 2024 at 08:28):It's a factual statement about mathematics that describes that fact using one noun that has a slightly negative connotation.
James E Hanson (Jun 14 2024 at 08:28):It contains a factual statement about mathematics, to be sure, but it also contains a pretty clear aesthetic judgement.
James E Hanson (Jun 14 2024 at 08:28):"Various circumlocutions are required" is not a factual statement if they're not circumlocutions.
James E Hanson (Jun 14 2024 at 08:29):I do not think they are circumlocutions, and therefore the statement is false from my point of view. This is an odd property for a factual statement about mathematics to have.
Mike Shulman (Jun 14 2024 at 08:30):I don't think you can say the statement is "false" because it is described using words whose connotations you don't agree with.
James E Hanson (Jun 14 2024 at 08:31):The von Neumann ordinals are not a circumlocution, and they do not require choice or foundation to represent ordinals. This at the very least means that I can't say the statement is "true" either and certainly not a "factual statement about mathematics."
Mike Shulman (Jun 14 2024 at 08:33):The statement says "possibly". I assume this was inserted because the author was aware that AC/AF are not required to represent ordinals, but they (or some weaker form of them) are required to represent cardinals, and the statement mentions both.
James E Hanson (Jun 14 2024 at 08:33):The other thing about the statement I find misleading is that if you add in the same kind of universes to that you're implicitly using in HoTT, you can form 'non-artificial' representatives in set theory directly. If I have an explicitly named sequence of inaccessible sets, then I can just represent a cardinality with its equinumerosity class (within the given universe).
Mike Shulman (Jun 14 2024 at 08:34):Ah, that's a much better point.
James E Hanson (Jun 14 2024 at 08:36):But for the record, I find the way type theory handles universes to be 'artificial' and 'unaesthetic.' What exactly is picking out the explicitly named universes?
James E Hanson (Jun 14 2024 at 08:37):I understand why it's a practical necessity given the way type theory works, but it doesn't strike me as a fundamental fact about mathematical reality that there is a countable sequence of inaccessible sets that is cofinal in the entire universe.
Mike Shulman (Jun 14 2024 at 08:37):I agree with you there. Fortunately, modern type theories as actually implemented usually have universe polymorphism, so you don't have to imagine that there is a fixed sequence of universes.
Mike Shulman (Jun 14 2024 at 08:38):The HoTT Book uses a fixed sequence just for simplicity.
James E Hanson (Jun 14 2024 at 08:38):Well except in the case of Agda, where there's an even more awkward arrangement as far as I can tell.
Mike Shulman (Jun 14 2024 at 08:38):Agda also has universe polymorphism, it's just explicit rather than implicit.
James E Hanson (Jun 14 2024 at 08:39):I'm talking about the second hierarchy of universes above the first one. That one is explicit, no?
Mike Shulman (Jun 14 2024 at 08:39):But Setω is admittedly bizarre, I dunno what's up with that.
Mike Shulman (Jun 14 2024 at 08:40):But I always figured that "real" mathematics happens in the first hierarchy of polymorphic universes;, with Setω and its friends just a technical device to hack that polymorphism into a particular formal framework.
James E Hanson (Jun 14 2024 at 08:41):Okay but why can't I define a map from to the universe levels in basically any type theory?
Mike Shulman (Jun 14 2024 at 08:41):Because the universe levels are not usually a type.
James E Hanson (Jun 14 2024 at 08:42):Right but that feels artificial to me.
Mike Shulman (Jun 14 2024 at 08:42):More artificial than the class of sets not being a set?
James E Hanson (Jun 14 2024 at 08:42):Yes.
Mike Shulman (Jun 14 2024 at 08:42):Well, it takes all kinds. (-:
James E Hanson (Jun 14 2024 at 08:42):The collection of all types is not a type.
Mike Shulman (Jun 14 2024 at 08:43):Right. So neither is the collection of all universes.
Mike Shulman (Jun 14 2024 at 08:43):Should I have said "more artificial than the class of all inaccessible cardinals not being a set"?
Mike Shulman (Jun 14 2024 at 08:43):(assuming a universe axiom)
James E Hanson (Jun 14 2024 at 08:43):I'm not saying that the collection of all universes needs to be a type. I'm saying that there's something that really clearly looks like a countable sequence and yet I'm artificially not allowed to call it that.
Mike Shulman (Jun 14 2024 at 08:44):I'm saying that in a universe-polymorphic theory, it doesn't look like a countable sequence.
James E Hanson (Jun 14 2024 at 08:44):What does it look like then?
Mike Shulman (Jun 14 2024 at 08:44):Um... why does it need to look like anything?
James E Hanson (Jun 14 2024 at 08:44):Because this is news to me.
James E Hanson (Jun 14 2024 at 08:45):If I have dependent choice, can I form an ascending sequence of universes?
Mike Shulman (Jun 14 2024 at 08:45):No.
James E Hanson (Jun 14 2024 at 08:45):Why not?
James E Hanson (Jun 14 2024 at 08:45):This is completely artificial.
Mike Shulman (Jun 14 2024 at 08:45):Because the collection of universes is not a type.
James E Hanson (Jun 14 2024 at 08:45):Is every universe contained in a bigger universe?
Mike Shulman (Jun 14 2024 at 08:45):Yes.
Mike Shulman (Jun 14 2024 at 08:46):But that's a metatheoretic statement, you can't internalize it as a quantification over universes.
Mike Shulman (Jun 14 2024 at 08:46):(In the sort of theory I'm talking about.)
James E Hanson (Jun 14 2024 at 08:46):You're not convincing me that this isn't artificial.
Mike Shulman (Jun 14 2024 at 08:46):Well, as I said, it takes all kinds.
James E Hanson (Jun 14 2024 at 08:48):I need to go to sleep but since we already started talking about this, I'm just going to say that I am basically incapable of reading the HoTT book for more than about 10 minutes at a time because I find so many of the little jabs at set theory infuriating.
Mike Shulman (Jun 14 2024 at 08:51):I'm sorry to hear that. Maybe you could send me privately a list of what you regard as "jabs". I picked as my example to quote the mention of set theory that seemed to me to be the most critical of any that I found. Your point about quotients of universes may convince me that this particular one is not mathematically a fair comparison, although I don't know whether the other authors would agree to make any change to it at this point. But most of the remarks about set theory that I found seem to me to be even more clearly factual.
David Michael Roberts (Jun 14 2024 at 08:51):I think this discussion about the universe indices illustrates an interesting distinction between the structural and material approaches: the universe indices _are_ (or can be) "countable", but their structure isn't such that you can't call them a model of PA, for instance.
David Michael Roberts (Jun 14 2024 at 08:53):I'm not talking about the "collection" of universes, but even just their indices. And so they are more like a proper class than a set, in that the allowed operations are much more restricted.
Mike Shulman (Jun 14 2024 at 08:53):I disagree that they "are" countable in any sense. Any particular theorem only uses finitely many universe indices, and there are always more indices if we need them. But there's no reason there couldn't be uncountably many of them, or even a proper class of them.
Mike Shulman (Jun 14 2024 at 08:54):There are countably many syntactic names for universe indices, but there are also countably many syntactic names for real numbers.
David Michael Roberts (Jun 14 2024 at 08:55):Let us say in the case they are indexed by external natural numbers (like in actual implementation). There is not a finite number of them, and none of the indices are infinite sets.
Mike Shulman (Jun 14 2024 at 08:55):But that's not the case I'm talking about.
Mike Shulman (Jun 14 2024 at 08:55):And they don't necessarily have to be implemented that way either.
Mike Shulman (Jun 14 2024 at 08:57):In universe-polymorphic Coq, for instance, any theorem has a collection of universe indices together with ordering relationships among them. But I don't think at any point these indices are instantiated by natural numbers; it suffices to maintain the collection of them and their ordering relationships.
David Michael Roberts (Jun 14 2024 at 08:57):Sure. But the "smallest possible" case is where you have an unbounded discrete linear order, no? In principle any directed set might be enough, but most often I see only a linear order etc.
David Michael Roberts (Jun 14 2024 at 08:58):It's more like a potential infinity than otherwise, I feel
Mike Shulman (Jun 14 2024 at 08:58):Yes, I agree it's a potential infinity. It could semantically be the infinity , but it could be lots of other things too, and the theory doesn't specify.
David Michael Roberts (Jun 14 2024 at 08:58):If we have unboundedly large indices, but are not allowed to consider all of them
James E Hanson (Jun 14 2024 at 09:01):Mike Shulman said:
I'm sorry to hear that. Maybe you could send me privately a list of what you regard as "jabs". I picked as my example to quote the mention of set theory that seemed to me to be the most critical of any that I found. Your point about quotients of universes may convince me that this particular one is not mathematically a fair comparison, although I don't know whether the other authors would agree to make any change to it at this point. But most of the remarks about set theory that I found seem to me to be even more clearly factual.
I could also just edit the source code myself and make a 'de-propagandized' version of the book. I also actually started compiling such a list because someone suggested that I should make a GitHub issue about this, although I was never really hopeful that that would go anywhere if I did it.
In any case, I do find it problematic. The HoTT book is one of the most commonly suggested textbooks for learning about type theory. I think that given how commonly the Blass-Gitik result is cited in the homotopy type theory literature (and given the extent to which set theory is struggling as a field because of bad PR within mathematics), it's really pretty bad form to not admit even in the end notes of the book that that theorem relies on a fairly technical class forcing result that nobody even remotely knows how to do in type theory at the moment. Type theory is one of the fields of mathematics that uses set theory the most, and people should know this.
Mike Shulman (Jun 14 2024 at 09:04):I feel like you are way overstating the importance of the Blass-Gitik result. As far as I know, it's totally irrelevant for actually doing mathematics in type theory. It's only mentioned because people are interested in the relationship between novel HoTT ideas like HITs and classical set theory.
Mike Shulman (Jun 14 2024 at 09:05):Type theory is one of the fields of mathematics that uses set theory the most
Um... evidence please?
James E Hanson (Jun 14 2024 at 09:05):Type theorists use set-theoretic models all the time. The original Voevodsky model of univalence was explicitly constructed in ZFC.
James E Hanson (Jun 14 2024 at 09:07):Also, as far as I know, all known proofs of relative consistency of choice factor through set theory, no?
Mike Shulman (Jun 14 2024 at 09:07):Sure, if you want to model type theory in set theory, then of course you need to use some set theory. I don't see this as using any more set theory than many other parts of mathematics. But for doing mathematics in type theory one doesn't need set theory.
Mike Shulman (Jun 14 2024 at 09:08):I think most type theorists would not regard the relative consistency of choice as part of type theory.
James E Hanson (Jun 14 2024 at 09:09):Okay sure but the HoTT book talks about all these various forms of AC and LEM, and it mentions which ones are consistent and inconsistent. Obviously the inconsistencies are shown with a direct proof, but how do you know those other forms are consistent?
Mike Shulman (Jun 14 2024 at 09:10):I don't think you can expect the HoTT Book, which was essentially written to inform people about HoTT and its potential advantages (remember that it was a very new thing at the time it was written), to sing the praises of ZFC.
Nathanael Arkor (Jun 14 2024 at 09:11):Surely any text that was proposing a new foundation for mathematics would compare it with pre-existing foundations, and promote its (perceived) advantages? It seems unreasonable not to expect the HoTT Book to do so.
James E Hanson (Jun 14 2024 at 09:11):Sure, but I'm saying that that project in and of itself is socially irresponsible in the context of the perception of set theory in mathematics. Going in front of a bunch of ordinary mathematicians and saying 'ZFC is whacky' full stop is not okay.
James E Hanson (Jun 14 2024 at 09:11):This is why it's a fine line.
Mike Shulman (Jun 14 2024 at 09:12):I don't think you can expect people to bend over backward to not say anything bad about ZFC just because some people already don't like it.
James E Hanson (Jun 14 2024 at 09:13):I'm not asking for you to bend over backwards. I'm asking for you to have maybe one paragraph where you say 'oh by the way set theory is still useful for metamathematics, the stuff set theorists do is pretty cool, we actually use it a lot behind the scenes.'
Nathanael Arkor (Jun 14 2024 at 09:14):Where does the HoTT Book give the impression that set theorists are not doing interesting mathematics?
James E Hanson (Jun 14 2024 at 09:15):It does this by omission. When it cites the Blass result, for instance, it doesn't mention that it's a set-theoretic metamathematical result.
Nathanael Arkor (Jun 14 2024 at 09:16):But it cites the Blass result explicitly in reference to ZF.
Mike Shulman (Jun 14 2024 at 09:17):It's long past my bedtime, and I don't think this discussion is going anywhere productive any more, so I'm going to sign off. Good night everyone.
James E Hanson (Jun 14 2024 at 09:18):Here's a better example. On page 14 (of hott-ebook-13-g2e736d1.pdf), in the introduction, we have the following parenthetical comment.
(One of the original virtues of type theory, relative to set theory, was that it can be seen to be consistent by proof-theoretic means).
This issue, establishing consistency proof-theoretically, is fairly orthogonal to set theory vs. type theory and has more to do with proof-theoretic strength. While it is true that some weak predicative type theories have purely proof-theoretic consistency proofs, stronger impredicative or classical type theories don't. On the other hand, there are several predicative set theories, such as KP and CZF, that are weak enough to have proof-theoretic consistency proofs. And while it's true that CZF was (if I recall correctly) motivated by a type-theoretic construction, Kripke-Platek set theory was not (and KP is about a decade older than MLTT for that matter).
Benedikt Peterseim (Jun 14 2024 at 09:20):@James E Hanson Could you clarify a bit what you’re trying to argue at this point? I feel like the discussion is meandering around various topics, so I’m having trouble seeing where precisely the disagreement actually mostly lies, and I’d be interested in understanding this better. Is it more on the cultural/community side of things? Is it that set theory as a field of study should receive more praise? Is it that type / category theorists should tone down their rhetoric?
Or do you actually disagree somewhere with mathematical structuralism as a philosophy, and think it shouldn’t spread as dogma so much by category theorists? E.g. if your response to the "junk theorem" argument is that finite von Neumann "just encodings", you must think they are encodings for something. That something is probably "the natural numbers" (notice the definite article!). But what are those? If you say "finite von Neumann ordinals" then finite von Neumann ordinals wouldn’t be "just encodings" after all. If you say "the (essentially) unique mathematical structure generated from an element '0' and a 'successor' function", then you agree with the structuralist point of view that the encoding shouldn’t matter and that isomorphic objects should be regarded as equal.
James E Hanson (Jun 14 2024 at 09:23):I will try to give a more thought-out answer after I have slept, but I think the core point I am trying to make is that I think that some type / category theorists should tone down their rhetoric because at this point set theory is a fairly marginalized field and their rhetoric is damaging the reputation of set theory as a field.
John Baez (Jun 14 2024 at 09:56):Note that this core point is about rhetoric, reputations, marginalization etc., and not primarily about theorems, axioms, etc. That doesn't mean it's unimportant! It's very important. But it does suggest that some of the technical discussion we've been seeing about mathematics here will not ever make James happier.
John Baez (Jun 14 2024 at 10:00):I think one thing going on here is that category theorists and homotopy type theorists tend to see themselves as rebels against the dominant paradigm, which I'll jokingly call "big ZFC" - while set theorists, or at least @James E Hanson, tend to focus on how hard it is for set theorists to get their work taken seriously compared to some other areas in mathematics: taken seriously enough to get good jobs, that is.
James E Hanson (Jun 14 2024 at 10:20):Mike Shulman said:
Well, as I said, it takes all kinds.
The more I think about this comment the more I find it really condescending, honestly.
James E Hanson (Jun 14 2024 at 10:24):John Baez said:
I think one thing going on here is that category theorists and homotopy type theorists tend to see themselves as rebels against the dominant paradigm, which I'll jokingly call "big ZFC" - while set theorists, or at least James E Hanson, tend to focus on how hard it is for set theorists to get their work taken seriously compared to some other areas in mathematics: taken seriously enough to get good jobs, that is.
Yes. I'm aware of this mismatch. HoTT is trying to push against the mainstream mathematician's idea that 'ZFC is the foundation of mathematics', but in doing so I feel like it's contributing to the decline of set theory as a field. I feel like this is a pretty shitty thing for a field that gets so much more military and commercial funding to be doing with its relatively greater resources.
Nathanael Arkor (Jun 14 2024 at 10:38):in doing so I feel like it's contributing to the decline of set theory as a field
Do you have any evidence that this is the case? I'm not trying to assert that it is not, just that the only people I can see being influenced by the HoTT community's perspective on foundations are not the people who are in a position to be making decisions about careers.
Nathanael Arkor (Jun 14 2024 at 10:40):I also feel that mathematical fields grow and decline, and it is not the responsibility of other fields to try to prevent that. If a field is valuable, then surely its own merits demonstrate that, regardless of how other fields perceive it?
James E Hanson (Jun 14 2024 at 10:43):Nathanael Arkor said:
in doing so I feel like it's contributing to the decline of set theory as a field
Do you have any evidence that this is the case? I'm not trying to assert that it is not, just that the only people I can see being influenced by the HoTT community's perspective on foundations are not the people who are in a position to be making decisions about careers.
No I do not have data or anything, just a lot of anecdotal observation of how mathematicians talk about other fields.
James E Hanson (Jun 14 2024 at 10:44):Nathanael Arkor said:
I also feel that mathematical fields grow and decline, and it is not the responsibility of other fields to try to prevent that. If a field is valuable, then surely its own merits demonstrate that, regardless of how other fields perceive it?
This is a nice idea but completely ignores the funding angle. I've seen type theorists argue that set theory is in decline because it doesn't represent everyday mathematical reasoning as well as type theory, and I just do not buy that this is the major contributing factor.
James E Hanson (Jun 14 2024 at 10:45):Mainstream type theory research is also pretty disconnected from everyday 'mainstream' mathematics. Most mathematicians cannot stand constructive math at all, but almost all type theory research is constructive by default.
James E Hanson (Jun 14 2024 at 10:46):Try explaining to the mathematician on the street what 'propositional extensionality' is and see if they think it's relevant to the math they do.
Nathanael Arkor (Jun 14 2024 at 10:47):My impression, which could be incorrect, was that much of the funding for type theory was being motivated by the promise that type theory is amenable to formal verification (more so than other methods). If this is true, then it is a concrete advantage type theory has as a foundation over set theory. If it is not true, then set theorists ought also to be able to acquire the same funding. But perhaps I am being naïve?
James E Hanson (Jun 14 2024 at 10:49):Formal verification for military and industrial applications. This is not the same design goal as writing a proof assistant for classical pure mathematics. While I don't necessarily think a proof assistant based on set theory is the right approach, I also do not think we have an even remotely unbiased data set for this kind of question.
James E Hanson (Jun 14 2024 at 10:49):There are tons of design decisions that go into type theories used in proof assistants that are aimed at things like constructive math and program extraction. These don't make any sense if your only goal is verifying classical pure math.
James E Hanson (Jun 14 2024 at 10:52):Microsoft, Intel, and the US Airforce are not going to be dumping big buckets of money into better proof automation and AI integration for Mizar and Metamath.
James E Hanson (Jun 14 2024 at 10:52):So, yes, I do actually think you're being a little bit naïve.
Nathanael Arkor (Jun 14 2024 at 10:54):If we're being realistic, don't hiring committees look more favourably on researchers who can consistently secure funding, regardless of whether it is for military/industrial applications, or for pure mathematics applications? It's not ideal, but that's how things are. So if type theory is better for the applications that bring in funding, then it is inherently more desirable in an academic career than set theory. The mathematical advantages of one over the other are almost irrelevant.
James E Hanson (Jun 14 2024 at 10:56):Okay well then HoTT doesn't really have the right to pretend that it's some bold new philosophical approach to math rather than a mercenary approach to securing funding via proof assistants.
Nathanael Arkor (Jun 14 2024 at 10:58):I think a branch of mathematics can both be a new approach to an existing problem/field, and also have practical value that means it can be advertised for funding.
James E Hanson (Jun 14 2024 at 10:59):But also, this just isn't how all math funding actually works. Kevin Buzzard didn't get five million pounds to formalize FLT because it has industry applications. Plenty of math exists on the basis of being interesting to other pure mathematicians, but this means that by attacking the legitimacy of a field you are smothering it in that domain.
James E Hanson (Jun 14 2024 at 11:00):Set theory is interesting and useful in ways that type theory isn't. It's useful to type theory. And type theorists standing up in front of a room full of pure mathematicians and calling ZFC 'whacky' or 'outdated' or 'artificial' is duplicitous.
James E Hanson (Jun 14 2024 at 11:00):It is hostile.
Nathanael Arkor (Jun 14 2024 at 11:00):I don't think Buzzard received funding by smothering the legitimacy of another field. It's not type theory vs set theory. It's the fact the Lean community have demonstrated they can formalise complex mathematical proofs, which other approaches have not done convincingly before.
James E Hanson (Jun 14 2024 at 11:01):That's not really relevant to my point.
James E Hanson (Jun 14 2024 at 11:02):That was just an example of how funding isn't always on the basis of purely mercenary applications.
Nathanael Arkor (Jun 14 2024 at 11:04):James E Hanson said:
Set theory is interesting and useful in ways that type theory isn't. It's useful to type theory. And type theorists standing up in front of a room full of pure mathematicians and calling ZFC 'whacky' or 'outdated' or 'artificial' is duplicitous.
I don't think there's who has been anyone involved in this discussion that would say it is appropriate to diminish another field of mathematics. The two examples I saw mentioned earlier were Lawvere, who is no longer with us, and Buzzard, who is not a type theorist. I have no doubt there are some type theorists who would say such things, but I think this is their personal problem, and the complaints would be better take up with them.
James E Hanson (Jun 14 2024 at 11:05):Okay I didn't want to go and name names specifically, but the 'whacky' quote I keep referencing was from Emily Riehl during a talk she gave at the University of Maryland on HoTT. Riehl is by no means a small name in the field.
Nathanael Arkor (Jun 14 2024 at 11:05):(From what I could tell, the earliest disagreement was with whether the HoTT Book diminishes set theory, and my impression from the examples given was that it does not. And certainly not to extent of calling set theory whacky or outdated.)
Nathanael Arkor (Jun 14 2024 at 11:06):James E Hanson said:
Okay I didn't want to go and name names specifically, but the 'whacky' quote I keep referencing was from Emily Riehl during a talk she gave at the University of Maryland on HoTT. Riehl is by no means a small name in the field.
Maybe you could email her and explain why you think this is unhelpful (I don't think she reads the Zulip).
James E Hanson (Jun 14 2024 at 11:07):I don't really think that that would change her mind.
Honestly the fact that I can't seem to convince anyone that the 'circumlocutions' quote from the HoTT book is hostile makes me feel pretty hopeless about this endeavor in general.
James E Hanson (Jun 14 2024 at 11:08):Mike and I just spent something like 20 minutes arguing about whether basic ideas in set theory research are 'artificial' or not. It doesn't really matter how welcoming you think you're being when that's your baseline.
Nathanael Arkor (Jun 14 2024 at 11:11):I kind of feel this is just the process of scientific research. If people didn't perceive shortcomings with set theory, then type theory might not have been proposed as an approach to foundations. If people didn't perceive shortcomings with X, then Y might not have been proposed as an alternative. Y might not be better than X, but having new perspectives is useful. And the proponents of Y will always view it more favourably than X.
Nathanael Arkor (Jun 14 2024 at 11:12):To me, it seems clear what the HoTT Book is trying to express, and the reader is free to decide whether or not they agree.
James E Hanson (Jun 14 2024 at 11:12):But type theory has not supplanted set theory. I know that the existence of non-measurable sets is independent of HoTT. I know this because of its relatively explicit interpretation in ZF + some large cardinals. Type theorists aren't even remotely close to being able to prove this with their own tools.
Nathanael Arkor (Jun 14 2024 at 11:12):Maybe I missed it earlier in the conversation, but does the HoTT Book ever claim to supplant set theory?
Nathanael Arkor (Jun 14 2024 at 11:13):Type theorists are generally not interested in those problems.
James E Hanson (Jun 14 2024 at 11:13):No, but plenty of people talking about HoTT do.
Nathanael Arkor (Jun 14 2024 at 11:13):But I don't think this is an impression obtained from the HoTT Book. If people say this, then the problem should be taken up with them (or wherever they got that impression from).
James E Hanson (Jun 14 2024 at 11:14):Nathanael Arkor said:
Type theorists are generally not interested in those problems.
Sure but lots of mathematicians are.
Nathanael Arkor (Jun 14 2024 at 11:14):Right, and for them, set theory will be the more appropriate tool.
James E Hanson (Jun 14 2024 at 11:14):Nathanael Arkor said:
But I don't think this is an impression obtained from the HoTT Book. If people say this, then the problem should be taken up with them (or wherever they got that impression from).
You can't address a systemic issue by sending out a bunch of individual emails.
Nathanael Arkor (Jun 14 2024 at 11:14):But I think mathematicians are generally wise enough to find the right tool for their problems.
James E Hanson (Jun 14 2024 at 11:14):Nathanael Arkor said:
Right, and for them, set theory will be the more appropriate tool.
No, I mean that ordinary mathematicians working in Lean might care about whether things are independent of Lean.
James E Hanson (Jun 14 2024 at 11:15):And often the easiest way of establishing those kinds of results is via set theory.
Nathanael Arkor (Jun 14 2024 at 11:15):James E Hanson said:
Nathanael Arkor said:
But I don't think this is an impression obtained from the HoTT Book. If people say this, then the problem should be taken up with them (or wherever they got that impression from).
You can't address a systemic issue by sending out a bunch of individual emails.
But at the moment you seem to be taking issue with the HoTT Book for a problem I don't see stems from, or is even present in, the HoTT Book.
James E Hanson (Jun 14 2024 at 11:16):Someone reading the 'circumlocutions' quote might reasonably come away from it thinking 'well, so if set theory is so bad at talking about cardinals and such, what are set theorists even doing?'
Nathanael Arkor (Jun 14 2024 at 11:17):To me, that sounds like a good thing. "Why are set theorists still working on set theory if type theory is better at talking about X, Y, Z? Surely there must be a good reason. Let me take a look..."
James E Hanson (Jun 14 2024 at 11:17):It's really not that big of a jump from 'the way set theory talks about cardinals is artificial' to 'set theorists must be doing set theory wrong'.
Nathanael Arkor (Jun 14 2024 at 11:17):Surely there are good texts on set theory that explain its advantages relative to type theory (or other approaches to foundations)?
James E Hanson (Jun 14 2024 at 11:18):No not really. There aren't very many recent set theory textbooks and a lot of set theorists don't really care about type theory per se.
Nathanael Arkor (Jun 14 2024 at 11:19):Then that sounds more like set theorists' problem. If type theorists are advertising its advantages over set theory, but set theorists are not advertising its advantages over type theory, then it seems natural newcomers will be drawn to one over the other.
Nathanael Arkor (Jun 14 2024 at 11:19):I don't see that that's type theorists' responsibility to correct.
James E Hanson (Jun 14 2024 at 11:20):The responsibility is to not do that advertising with incorrect or otherwise biased statements.
Nathanael Arkor (Jun 14 2024 at 11:20):I disagree. Advertising is inherently biased. Of course type theorists prefer type theory.
Nathanael Arkor (Jun 14 2024 at 11:20):In keeping up with the times, a well established field should continue to promote the reasons it's still relevant. Simply ignoring new developments will surely lead to depletion in interest.
Nathanael Arkor (Jun 14 2024 at 11:21):That feels naïve to me.
James E Hanson (Jun 14 2024 at 11:21):I already pointed out a factual error in the 'circumlocutions' quote that Mike admitted was a good point. I feel like the issue I pointed out is a pretty obvious one, and I feel like it's pretty clear that it didn't occur to any of the authors of the HoTT book because none of them made a good faith attempt to think about how one might try to do that thing in set theory in a 'natural' way.
James E Hanson (Jun 14 2024 at 11:21):Nathanael Arkor said:
I disagree. Advertising is inherently biased. Of course type theorists prefer type theory.
Okay well then I'm well within my rights to call it disingenuous, because it is.
Nathanael Arkor (Jun 14 2024 at 11:21):At least this problem can be addressed with a bug report to the HoTT Book.
James E Hanson (Jun 14 2024 at 11:22):I already mentions that I was thinking about submitting an issue on GitHub but I also would bet a pretty large amount of money that it wouldn't accomplish anything.
Nathanael Arkor (Jun 14 2024 at 11:23):James E Hanson said:
Nathanael Arkor said:
I disagree. Advertising is inherently biased. Of course type theorists prefer type theory.
Okay well then I'm well within my rights to call it disingenuous, because it is.
Sure, the HoTT Book could give some examples of things that set theory does better than type theory (at least for now). Maybe the authors would concede to add some if you opened an issue. But I also wouldn't blame them if they didn't. (Just as I wouldn't blame a set theory text for not giving the relative advantages of type theory; I don't think it's their responsibility.)
Nathanael Arkor (Jun 14 2024 at 11:23):James E Hanson said:
I already mentions that I was thinking about submitting an issue on GitHub but I also would bet a pretty large amount of money that it wouldn't accomplish anything.
I guess there's only one way to find out :)
Nathanael Arkor (Jun 14 2024 at 11:24):You could even make a pull request with a suggested change. That would be more likely to have an effect, I think.
Nathanael Arkor (Jun 14 2024 at 11:24):It's a lot easier to review a change than to implement one.
James E Hanson (Jun 14 2024 at 11:24):Mike more or less already stated that he doesn't think the other authors will agree to changing the book at this point.
James E Hanson (Jun 14 2024 at 11:24):But also I already know Mike doesn't agree with the first change I would propose, which is more or less removing the incorrect 'circumlocutions' quote.
Nathanael Arkor (Jun 14 2024 at 11:24):If the HoTT Book is immutable at this point, then the entire conversation seems a moot point, no?
James E Hanson (Jun 14 2024 at 11:25):No because by making this argument here I can always point to it later as a reference when explaining why the HoTT book is obnoxious, biased propaganda.
James E Hanson (Jun 14 2024 at 11:26):A lot of arguing on the internet isn't about convincing the other person.
Nathanael Arkor (Jun 14 2024 at 11:26):Why don't you write a short article about the advantages of set theory relative to type theory? I think such a document would be very helpful (I wouldn't know where to look for such an explanation at the moment), and it would be a much better reference point than a Zulip thread.
James E Hanson (Jun 14 2024 at 11:27):I had thought about that too.
Nathanael Arkor (Jun 14 2024 at 11:27):Although I would advise on holding back on words like "obnoxious" and "propaganda" :)
Nathanael Arkor (Jun 14 2024 at 11:28):James E Hanson said:
I had thought about that too.
I'd certainly be happy to read such an article.
James E Hanson (Jun 14 2024 at 11:28):I am losing my filter a bit at this point, I admit.
But I also was hoping (naively) to maybe convince some people here that their rhetoric is harmful and that they should change it.
Nathanael Arkor (Jun 14 2024 at 11:28):I think the ideal solution would be to have an article on the relative merits and demerits of set theory and type theory, which both set theorists and type theorists agree on.
Nathanael Arkor (Jun 14 2024 at 11:29):Part of your issue with the HoTT Book stems from the fact it was written by type theorists, and so is inherently biased.
Nathanael Arkor (Jun 14 2024 at 11:29):But if an article is positively perceived by both communities, that would be perfect.
James E Hanson (Jun 14 2024 at 11:30):Yeah but there are going to be things that they never really agree on. I find the global structure of type theories ugly and artificial, but I admit that to some extent this is probably because of learning set theory first. There's no objective standard for what the global structure of a mathematical universe should be.
Nathanael Arkor (Jun 14 2024 at 11:30):Well, there are at least some objective facts, and some points of dispute. At least if you're explicit about them, the reader can make up their own mind (or at least understand that it is a contentious issue).
Nathanael Arkor (Jun 14 2024 at 11:31):Maybe the best approach is if such a paper is coauthored by both a set theorist and a type theorist.
James E Hanson (Jun 14 2024 at 11:31):But I feel like the HoTT book is not very good at differentiating between aesthetic judgements and factual statements when it comes to criticisms of set theory.
James E Hanson (Jun 14 2024 at 11:31):The other thing is just that I see set theory and type theory as playing different roles.
Nathanael Arkor (Jun 14 2024 at 11:31):James E Hanson said:
But I feel like the HoTT book is not very good at differentiating between aesthetic judgements and factual statements when it comes to criticisms of set theory.
I think having authors from both fields would help with this.
James E Hanson (Jun 14 2024 at 11:32):So I don't even really think a head-to-head comparison is totally warranted.
Nathanael Arkor (Jun 14 2024 at 11:32):But that's fine. An article explaining the roles they play would be just as helpful.
Nathanael Arkor (Jun 14 2024 at 11:33):(I will happily volunteer to proof read the article.)
Nathanael Arkor (Jun 14 2024 at 11:34):(Maybe you already have someone in mind who would make a good coauthor, but if not, I imagine you would get some interest on working on such a project on the TYPES mailing list.)
James E Hanson (Jun 14 2024 at 11:34):Type theories are roughly speaking what you come up with when you want to build a formal system that you can actually prove things in. Set theories are more like what you do when you want to do heavy metamathematics.
You see this dichotomy even within the ecosystem of different type theories. Daily use type theories, like those in Lean, Coq, and Agda, have a lot of extra features added in that are hypothetically (but not always actually) reducible to more primitive notions. On the other hand you have extremely minimalist type theories like System F, where you do awkward coding tricks to do things like build the natural numbers.
James E Hanson (Jun 14 2024 at 11:35):Those minimalist type theories play more of a role in the theoretical side of type theory research.
Todd Trimble (Jun 14 2024 at 11:50):James, could you provide some fuller context for Emily's use of "whacky"? Or is the talk recorded somewhere so that readers can judge for themselves?
Zoltan A. Kocsis (Z.A.K.) (Jun 14 2024 at 11:56):I will try to give a more thought-out answer after I have slept, but I think the core point I am trying to make is that I think that some type / category theorists should tone down their rhetoric because at this point set theory is a fairly marginalized field and their rhetoric is damaging the reputation of set theory as a field.
I earned my PhD from an institution with a strong emphasis on model theory and was fortunate to study set theory under a Hausdorff medalist. It was great, and I think it's fair to say that I have a very favorable view of classical set theory compared to most of my peers (and superiors) here.
However, I find the attribution of the employment struggles of set theorists to the criticisms from category theorists or type theorists so weird that it quickly erodes all my empathy.
Securing a position in a mathematics department when specializing in foundations is very very challenging, with little to no advantage whether one focuses on set theory or type theory. In fact, if you want to work in a math department, being a set theorist is downright easy mode compared to, say, a structural proof theorist; and I think even a type theorist.
If polemics by type theorists had any serious impact on the job prospects of set theorists, I would expect to see the following: the few schools of mathematics which employ type theorists would be the ones to have the fewest set theorists.
In reality, I see the exact opposite. I had a hard time naming a single school of mathematics which employs type theorists but not set theorists (in the end I could think of an otherwise unremarkable institution in Eastern Europe, which employs 2 type theorists in total). The converse was trivially easy: take the Einstein Institute / HUJI.
Truth is, most departments prefer candidates with expertise in core areas like algebra, combinatorics, differential equations, geometry, or number theory, which impacts hiring decisions 1000x more than any academic debate between niche fields ever could. And even if criticism from type theorists somehow factored into these decision (which I don't believe at all!), that would not in itself be reason for them to tone their criticisms down: after all, if these polemical category/type theorists _were_ right in their assertion that something is wrong with set theory (which I don't think they are), then it _would be_ the right move for math departments to hire fewer set theorists. But it's not like set theorists had an easier time finding positions before the IAS year on HoTT: practitioners of the core areas had a dim view of foundational research for at least the last 30 years.
(I also fail to see where set theory and type theory are competing for the same funding sources, but I'm only familiar with the funding situation in my country, Australia, and, well, it's not great for either field here at the moment, or even for the core areas)
James E Hanson (Jun 14 2024 at 12:05):Todd Trimble said:
James, could you provide some fuller context for Emily's use of "whacky"? Or is the talk recorded somewhere so that readers can judge for themselves?
I can't find a recording of the talk. (I believe it was the colloquium talk in October 2023, although she also gave the geometry seminar talk the next week.) It was an offhand comment, rather than something written on a slide or otherwise presented in an emphasized manner, but she didn't elaborate at all and to me the tone of the comment was pretty explicitly negative, rather than something like a joke. I acknowledge that I may be oversensitive to theses kinds of things, but it felt quite derogatory to me and still does.
James E Hanson (Jun 14 2024 at 12:09):Zoltan A. Kocsis (Z.A.K.) This is a really good point, and I will need to think about what you've said. The only thing I think I'll say now is that my comments about set theory 'struggling' or 'declining' were mostly in reference to set theory in the US in particular (on the basis of some discussions I've had about this) and I should have mentioned this. I certainly don't think set theory is in danger of going extinct in Israeli universities any time soon.
Todd Trimble (Jun 14 2024 at 12:12):James E Hanson said:
Todd Trimble said:
James, could you provide some fuller context for Emily's use of "whacky"? Or is the talk recorded somewhere so that readers can judge for themselves?
I can't find a recording of the talk. (I believe it was the colloquium talk in October 2023, although she also gave the geometry seminar talk the next week.) It was an offhand comment, rather than something written on a slide or otherwise presented in an emphasized manner, but she didn't elaborate at all and to me the tone of the comment was pretty explicitly negative, rather than something like a joke. I acknowledge that I may be oversensitive to theses kinds of things, but it felt quite derogatory to me and still does.
Can you approximately recall the sentence in which the word was embedded? It would be one thing to say, "All of set theory is completely whacky" (which I can't imagine her saying), as opposed to something much more narrowly constrained.
David Michael Roberts (Jun 14 2024 at 12:34):Can I also say: pure category theory is not exactly thriving at the expense of set theory. Macquarie University, the last remaining foothold of the once multi-university "Australian CT school" in Sydney, is doing the group there no favours. Cambridge isn't exactly thriving as it once did, from what I know. There's a couple of other universities in the UK with a decent CT presence that really don't have it (or much mathematics) any more. These were real centres with gravitational pull. Maybe it's just the shifting landscape and people are getting jobs elsewhere, or aligned with other disciplines (for instance with computer science or algebraic topology) while still being a straight-up category theorist.
Todd Trimble (Jun 14 2024 at 12:36):There's also the case of Montreal (McGill).
David Michael Roberts (Jun 14 2024 at 12:44):Yes, I was thinking about the Canadians, too, but wasn't quite sure where that was at. My memory of rumours was poorer.
Mike Shulman (Jun 14 2024 at 16:25):Hi again everyone. Having slept a few hours and skimmed the discussion while I was asleep, I don't think I have much to add. After so much taking of quotes out of context and accusations of bad faith I don't feel like I want to continue the conversation, but I'm grateful to others for doing so. I have opened issues relating to the mathematical points that have been raised with the HoTT Book, for which I am thankful regardless of what comes of them:
https://github.com/HoTT/book/issues/1156
https://github.com/HoTT/book/issues/1157
Madeleine Birchfield (Jun 14 2024 at 17:41):Zoltan A. Kocsis (Z.A.K.) said:
Securing a position in a mathematics department when specializing in foundations is very very challenging, with little to no advantage whether one focuses on set theory or type theory. In fact, if you want to work in a math department, being a set theorist is downright easy mode compared to, say, a structural proof theorist; and I think even a type theorist.
On the other hand, there are plenty of type theorists who are in a computer science department at universities, while nearly all set theorists are working out of a mathematics department.
Kevin Carlson (Jun 14 2024 at 18:07):I’d say Zoltan’s “for at least the last 30 years” is extremely conservative. After all, there’s only ever been one Fields medal in any of the subjects currently being argued about. I wouldn’t think to describe foundational topics as having been at the “core” of pure math in a century—since, of course, decades before category theory or anything resembling modern type theory had even been invented.
James E Hanson (Jun 14 2024 at 18:13):Todd Trimble said:
James E Hanson said:
Todd Trimble said:
James, could you provide some fuller context for Emily's use of "whacky"? Or is the talk recorded somewhere so that readers can judge for themselves?
I can't find a recording of the talk. (I believe it was the colloquium talk in October 2023, although she also gave the geometry seminar talk the next week.) It was an offhand comment, rather than something written on a slide or otherwise presented in an emphasized manner, but she didn't elaborate at all and to me the tone of the comment was pretty explicitly negative, rather than something like a joke. I acknowledge that I may be oversensitive to theses kinds of things, but it felt quite derogatory to me and still does.
Can you approximately recall the sentence in which the word was embedded? It would be one thing to say, "All of set theory is completely whacky" (which I can't imagine her saying), as opposed to something much more narrowly constrained.
The statement was about ZFC in specific being 'whacky,' which I still consider obnoxious and inappropriate.
Chris Grossack (they/them) (Jun 14 2024 at 18:15):I've thought about saying something for a while now, but never felt like it was the right time. Since this thread looks like it might be wrapping up soon, though (?) I do want to say something while it's still relevant.
I just want to be another voice saying that I have a lot of close friends who are set theorists, and had I gone to a different grad school I would likely be some kind of set theorist myself right now. Every single one of my set theorist friends has felt attacked by people influenced by ideas in category theory/type theory. I personally see anti-set-theory microaggressions constantly, and frankly I see this thread through that lens. For example, I don't see how someone can possibly read the "circumlocution" comment as anything other than saying "we know how to study cardinals and ordinals better than those silly set theorists", and I don't see how anyone would expect the set theorists to not find that insulting.
Someone came to our community and said they felt repeatedly belittled by certain rhetoric we're using (maybe not individually, but certainly collectively). I've seen it too, and felt repeatedly belittled by it. My friends have seen it too, and felt repeatedly belittled by it. It's embarrassing that the discussion in this thread seems to be focused on explaining to someone hurt why these comments actually weren't hurtful.
The kind thing to do would be to apologize, accept that people are using our ideas hurtfully, and start correcting that going forwards.
Kevin Carlson (Jun 14 2024 at 18:22):For what it's worth I think Chris is fundamentally correct; part of the water supply of many category theorists is a deep commitment to mathematical structuralism which certainly slips out at various times, ones which may be hard to point to with definitive quotes, as actually making fun of mathematical materialism. It is indeed a thin line to toe, since of course we do tend to actually think that mathematical structuralism is "better" in many senses, just as an ethical deontologist thinks that deontology is better than consequentialism--I think it's highly supererogatory and opposed to human nature to ask people not to believe their beliefs are more correct than others'! But it's important to take this kind of thing quite seriously, and avoid making careless jokes or jabs at other people's philosophies (cultures/religions?!) I'll try to keep this in mind myself, especially around people who are (even) more junior than me, and when writing in public.
James E Hanson (Jun 14 2024 at 18:36):Mike Shulman said:
Hi again everyone. Having slept a few hours and skimmed the discussion while I was asleep, I don't think I have much to add. After so much taking of quotes out of context and accusations of bad faith I don't feel like I want to continue the conversation, but I'm grateful to others for doing so. I have opened issues relating to the mathematical points that have been raised with the HoTT Book, for which I am thankful regardless of what comes of them:
https://github.com/HoTT/book/issues/1156
https://github.com/HoTT/book/issues/1157
Mike, there's at least one more purely mathematical points in the HoTT book that I consider inaccurate.
In particular, the 'HoTT Cauchy reals,' which are used in the book as an example of the usefulness of higher inductive types outside of the context of homotopy theory, are something that are fairly trivial to construct in constructive set theory (or non-univalent type theory) as well. All one needs to do is consider the Dedekind reals or the MacNeille reals and look at the smallest Cauchy-closed subfield containing the rationals. This means that the following claim on Page 14 (of hott-ebook-13-g2e736d1.pdf) is in my mind dubious:
In set-theoretic foundations, the definition of the real numbers as equivalence classes of Cauchy sequences requires either the law of excluded middle or the axiom of (countable) choice to be well-behaved. But with higher inductive types, we can give a version of this definition which is well-behaved and avoids any choice principles; see Chapter 11.
In particular, this is a slightly disingenuous statement because it's saying that one particular definition of the Cauchy reals is poorly behaved constructively, but a different definition that can also be done equivalently in comparable constructive set theories is well-behaved. (The other issue of course is just that constructive mathematicians preferred and still prefer the definition of the reals in terms of Dedekind cuts over any of the definitions in terms of Cauchy sequences.)
The general point of course is that you can do quotient-inductive types in something like IZF if you know a size bound on the resulting set ahead of time (something like a surjection from a subset of a given set).
Honestly, given the fact that two of the four bullet points comparing HoTT to set theory introduction of the book are pretty arguably wrong or at the very least misleading, I don't really feel confident in the accuracy of statements about set theory made in the rest of the book.
Eric M Downes (Jun 14 2024 at 18:36):James E Hanson said:
Mac Lane and Lawvere decided that they thought set theory was, for lack of a better term, bad. Mac Lane called set theory 'obsolete' and said that measurable cardinals were 'strange.' Lawvere allegedly called set theory 'Bourgeoisie idealism' at one point... etc.
So... even supposing Bill Lawvere did hate ZFC... because of this, I cannot study ETCS without also hating ZFC?
Lawvere outright quotes Chairman f&$%ing Mao in his paper on (what became) the Lawvere-Tierney Topology. I can use his theorems without becoming a communist! _Mathematics is not politics_; we can completely disagree on the latter and still converge to agreement on the former.... there's literally a theorem about this in computer science! (And this remains true, even when the politics concerns mathematics itself.)
I guess I am just struggling to understand what your objective is here?
My subjective impression is that you are trying to litigate a battle that I absolutely do not care about in relation to a class I am happy is being taught, because I appreciate a diversity of viewpoints: it helps me learn. FWIW, my interest in ZFC has actually grown considerably after reading Tom's ETCS preprint, while reading your arguments has not had the same effect, I'm sorry to say. I don't mean to be rude, but is the enemy you are fighting present in this forum? I don't even see his foot-soldiers.
James E Hanson (Jun 14 2024 at 18:50):@Eric M Downes I don't think you're being rude, or at the very least if you are it's warranted. I am being unpleasant, and I need to think about what I'm trying to accomplish.
Mostly at the moment I feel like Mike's statements about set theory (specifically saying that things like von Neumann ordinals, initial ordinals of cardinalities, and Scott cardinals are 'artificial' and 'unaesthetic') are hostile. If we think of those things as just being technical tools (which certainly the latter two are, in my mind), then this would be like someone who studies non-commutative rings calling Gröbner bases 'artificial' and 'unaesthetic.' I think that would be equally irritating to people who study polynomial rings and use Gröbner bases frequently.
James E Hanson (Jun 14 2024 at 18:56):@Mike Shulman Here is another statement from the introduction that I consider misleading in purely matheamtical terms (but also phrased in an obnoxious way):
Secondly, one of the additional virtues of type theory is its computable character. In addition to being a foundation for mathematics, type theory is a formal theory of computation, and can be treated as a powerful programming language. From this perspective, the rules of the system cannot be chosen arbitrarily the way set-theoretic axioms can: there must be a harmony between them which allows all proofs to be “executed” as programs.
If someone sits down and tries to write a (computably enumerable) constructive set theory that satisfies the disjunction and existence properties, then the same kind of fundamental computational restrictions apply. This is obviously a lot more crass of a way of approaching computation than a practical type theory, but it's something that I've actually spent a fair amount of time thinking about in my own research on computational content in constructive set theory.
The obnoxious aspect of the quote is that it's very hard for me to not read it as implying that the axioms of set theory are merely 'arbitrary,' which I would hope you would agree is not in fact true. On the other hand, as we've already discussed, even type theories with computational content can have a fair amount of arbitrariness (such as Agda's second type universe hierarchy, which has some odd 'artificial' restrictions, such as not being able to form lists).
James E Hanson (Jun 14 2024 at 19:02):And it's not just Agda. Coq has both Prop and SProp. Are we supposed to believe that it's a fundamental and immutable fact about the nature of 'computational truth' that there are precisely two notions of 'proposition'? Lean has its weird issues with non-transitive definitional equality. Isabelle has its somewhat awkward inner/outer syntax distinction. (Lean and Isabelle are both typically used non-constructively but can be used constructively, so I think they are relevant to the discussion.)
Graham Manuell (Jun 14 2024 at 19:29):@James E Hanson What do you suggest that people who sincerely have misgivings about set theory (or at least the usual approaches to it) should do? It does not seem like it would be much of an improvement for them to keep quiet, but still privately maintain their beliefs. This just seems like a way to shut down anyone who is not satisfied with the current accepted foundations of mathematics.
Of course, it is no doubt frustrating when critics of set theory get things wrong in their criticisms. But I do not think most of the category theorists you are complaining about are arguing in bad faith. Ideally they would become experts in set theory before they criticise it, but this seems unrealistic. I guess some kind of dialogue between the camps (as is happening here) might be a good way to try make progress.
I don't think anyone is doing anything wrong when they complain about the natural number 3 being a topology or whatever. And especially anyone advocating a new system is doing so because they find the old system lacking. They must be allowed to do this. You have made a number of criticisms of type theory in this discussion and it is also crucial that you are allowed to do this too.
Madeleine Birchfield (Jun 14 2024 at 19:57):James E Hanson said:
And it's not just Agda. Coq has both
PropandSProp. Are we supposed to believe that it's a fundamental and immutable fact about the nature of 'computational truth' that there are precisely two notions of 'proposition'?
This has been one of my problems philosophically with most dependent type theories used today: the fact that there are two different notions of equality (judgmental equality vs identity type) and thus two different notions of subsingleton/proposition, and (at least) two notions of nearly everything else (sets, fields, n-types, etc).
One dependent type theory I know which avoids all that is objective/weak/propositional type theory, where judgmental equality only exists on the metatheory level and the only equality in the object theory level is the identity type - so sProp simply wouldn't exist there. However, objective type theory has its own problems - for example it doesn't have canonicity (apparently very important for proof assistants). In addition, proofs and definitions become very tedious, because one has to use equivalences and transport everywhere, since one cannot simply say this type or term is judgmentally equal or reduces to this other type or term.
Todd Trimble (Jun 14 2024 at 19:59):The statement was about ZFC in specific being 'whacky,' which I still consider obnoxious and inappropriate.
Well, taking Chris's statement to heart, and adopting a prima facie position that it was at the very least obnoxious, I just wonder why it even came up in her talk, i.e., it would be weird if she just said it out of the blue. But never mind if you don't recall, or would rather not try to recall.
James E Hanson (Jun 14 2024 at 20:09):@Graham Manuell So I don't think this is a perfect analogy because I don't entirely think that it makes sense to literally base the kernels of proof assistants off of set theory (although I think there is more of an argument for that than some people think), but to me criticizing ZFC for junk theorems is like criticizing RISC-V for not having types and garbage collecting. These are of course problems with literally trying to write machine code in RISC-V, but you're not supposed to actually do that.
So given that, why don't we build processors that run Haskell or OCaml on bare metal? There are a couple of obvious reasons, but mostly it's because it's too complicated. Intel has had problems in the past with just implementing IEEE floating point arithmetic correctly on their chips (which is part of the reason they funded the development of HOL Light); are they really supposed to be trying to implement Haskell's IO monad correctly on bare metal when the developers of Haskell themselves got it wrong at one point? No, obviously not. There's a practical reason for the stratification into low-level, austere, untyped machine code and high-level, fully featured, strongly typed programming language.
The promise of set theory was always that it was a simple framework in which it is in principle possible to encode mathematics. The benefit of this simplicity is supposed to be that semantics and syntax are easier to reason about, which means that we can (1) be more philosophically confident in the semantic coherence and therefore probable consistency of the theory, (2) be more able to easily build models of the theory and therefore prove independence results, and (3) have an easier time internalizing syntax.
I would argue that set theory (or as I've recently taken to calling it, set theory plus first-order logic) has succeeded in all three of these points significantly over and above type theory:
My problem with the junk theorem arguments that people put forward is that they don't address this side of the issue at all. They mostly just go ' is a topology, the horror' and stop, completely ignoring the fact that the austerity that leads to that kind of 'low-level garbage' is the result of an intentional design decision with objective, concrete benefits, rather than some foible of antiquity.
James E Hanson (Jun 14 2024 at 20:11):Todd Trimble said:
The statement was about ZFC in specific being 'whacky,' which I still consider obnoxious and inappropriate.
Well, taking Chris's statement to heart, and adopting a prima facie position that it was at the very least obnoxious, I just wonder why it even came up in her talk, i.e., it would be weird if she just said it out of the blue. But never mind if you don't recall, or would rather not try to recall.
She brought it up, if I recall correctly, because the beginning of the talk was sort of explicitly framed in terms of foundations. She made some comment about type theory changing her mind about what mathematics is or something to that effect.
James E Hanson (Jun 14 2024 at 20:15):Another benefit of the above austerity I forgot to mention is conservativity results. We know that ZFC is conservative over ZF, for instance, which means that results like the main result of this paper could in principle have been produced systematically from corresponding ZFC proofs.
James E Hanson (Jun 14 2024 at 20:19):Similarly the HoTT book discusses some homotopy groups of spheres and mentions that the proofs are constructive (see page 391), but homotopy groups of spheres can be encoded (I'm fairly sure) as arithmetic facts (and possibly simpler) about the combinatorics of simplicial sets. Since we know ZFC is conservative over ZF, which is in turn conservative over IZF, we actually already have constructive proofs of these results (in principle), even though our original proofs used choice and LEM.
Madeleine Birchfield (Jun 14 2024 at 20:20):James E Hanson said:
Contrast this with the famous and amusingly titled 2008 type theory paper Type Theory should eat itself by Chapman, which starts its introduction with "This work is a small step towards the long-term goal of the author and many others to internalise the syntax and semantics of recent formulations of type theory."
This has become even harder with the advent of HoTT, since now those working on internalizing the syntax and semantics of type theory in type theory itself have to deal with infinity category theory and the infinite coherence issues that arise there.
Mike Shulman (Jun 14 2024 at 20:54):James E Hanson said:
In particular, the 'HoTT Cauchy reals,' which are used in the book as an example of the usefulness of higher inductive types outside of the context of homotopy theory, are something that are fairly trivial to construct in constructive set theory (or non-univalent type theory) as well. All one needs to do is consider the Dedekind reals or the MacNeille reals and look at the smallest Cauchy-closed subfield containing the rationals.
Is that possible in a predicative theory? To define Dedekind or MacNeille reals you need an object of propositions, which predicatively doesn't have to be the object of all propositions, but if it isn't, I wouldn't expect this construction to give you the Escardo-Simpson-HoTT Cauchy reals.
(The other issue of course is just that constructive mathematicians preferred and still prefer the definition of the reals in terms of Dedekind cuts over any of the definitions in terms of Cauchy sequences.)
Which constructive mathematicians are you talking about? Of course topos theorists prefer the Dedekind reals, but my impression is that traditional "computable" constructivists tend to prefer the Cauchy reals as they are easier to compute with.
James E Hanson (Jun 14 2024 at 20:56):Mike Shulman said:
Which constructive mathematicians are you talking about? Of course topos theorists prefer the Dedekind reals, but my impression is that traditional "computable" constructivists tend to prefer the Cauchy reals as they are easier to compute with.
This was the distinct impression that Andrej gave me when we were writing our topos theory paper.
James E Hanson (Jun 14 2024 at 20:58):Mike Shulman said:
Is that possible in a predicative theory? To define Dedekind or MacNeille reals you need an object of propositions, which predicatively doesn't have to be the object of all propositions, but if it isn't, I wouldn't expect this construction to give you the Escardo-Simpson-HoTT Cauchy reals.
Probably not, but given the fact that the HoTT book doesn't seem to even acknowledge the existence of predicative set theories, I still find it to be a misleading omission.
Madeleine Birchfield (Jun 14 2024 at 20:58):Mike Shulman said:
Which constructive mathematicians are you talking about? Of course topos theorists prefer the Dedekind reals, but my impression is that traditional "computable" constructivists tend to prefer the Cauchy reals as they are easier to compute with.
From what I remember the traditional "computable" constructivists tend to use countable choice as well so the Cauchy reals and Dedekind reals coincide.
Mike Shulman (Jun 14 2024 at 20:59):The HoTT Book is not about set theory, so it's unreasonable to expect it to say very much about all the different kinds of set theories out there.
James E Hanson (Jun 14 2024 at 21:00):That makes it disingenuous that it will pick and choose whichever version of set theory makes its criticism most relevant. If we're just going to take 'set theory' to mean ZFC, then the comments about choice and foundation shouldn't be there.
James E Hanson (Jun 14 2024 at 21:01):Someone reading the HoTT book probably would come away with the impression that there is literally no such thing as constructive set theory. The letters IZF and CZF don't even occur in it.
James E Hanson (Jun 14 2024 at 21:02):Saying things like 'oh set theory isn't constructive' when constructive set theories exist is a bad faith thing to do.
Madeleine Birchfield (Jun 14 2024 at 21:04):James E Hanson said:
Someone reading the HoTT book probably would come away with the impression that there is literally no such thing as constructive set theory. The letters
IZFandCZFdon't even occur in it.
The term 'constructive Zermelo-Frankel set theory' appears at the end of section 10.5 of the HoTT book though.
James E Hanson (Jun 14 2024 at 21:05):Thank you Madeleine. I should have done a more thorough search, but I still find the quote
From this perspective, the rules of the system cannot be chosen arbitrarily the way set-theoretic axioms can: there must be a harmony between them which allows all proofs to be “executed” as programs
to be problematic.
Madeleine Birchfield (Jun 14 2024 at 21:09):Regarding this quote
From this perspective, the rules of the system cannot be chosen arbitrarily the way set-theoretic axioms can: there must be a harmony between them which allows all proofs to be “executed” as programs
The type theory in the HoTT book doesn't even satisfy that quote - the univalence axiom in the HoTT book is arbitrary according to that standard and blocks the execution of proofs as programs, which is why type theorists spent a few years in the early-mid 2010s developing cubical type theory as an alternative to the theory in the HoTT book.
James E Hanson (Jun 14 2024 at 21:10):Yes but to be fair, the next line addresses this.
James E Hanson (Jun 14 2024 at 21:10):We do not yet fully understand the new principles introduced by homotopy type theory, such as univalence and higher inductive types, from this point of view, but the basic outlines are emerging; see, for example, [LH12].
James E Hanson (Jun 14 2024 at 21:11):Out of curiosity, I know that cubical type theory exists, but is there a computational interpretation of book HoTT in particular yet?
Madeleine Birchfield (Jun 14 2024 at 21:13):I'm not sure; Mike Shulman might be able to answer that question though.
Madeleine Birchfield (Jun 14 2024 at 21:23):Back to the quote,
From this perspective, the rules of the system cannot be chosen arbitrarily the way set-theoretic axioms can: there must be a harmony between them which allows all proofs to be “executed” as programs
I really only see this as relevant for those interested in creating and/or using a proof assistant where the concept of program and execution is relevant. Absent implementation in a proof assistant, does it matter to practicing mathematicians whether judgmental equality in type theory is decidable or not or whether axioms block execution of proofs or not, or whether the theory has canonicity or not?
Madeleine Birchfield (Jun 14 2024 at 22:00):@James E Hanson as for neutrality I find Egbert Rijke's textbook on (homotopy) type theory to be much better than the HoTT book, since the textbook merely presents type theory as an alternate foundations of mathematics and doesn't try to argue for if/why type theory is better than set theory, or if/why constructive predicative mathematics is better than classical mathematics
https://arxiv.org/pdf/2212.11082
Mike Shulman (Jun 15 2024 at 04:47):Madeleine Birchfield said:
From what I remember the traditional "computable" constructivists tend to use countable choice as well so the Cauchy reals and Dedekind reals coincide.
That's true for the most traditional ones, but I had the impression that some of them preserved their preference for Cauchy reals even when they considered dropping countable choice. But I could be remembering wrong, so skip it.
Mike Shulman (Jun 15 2024 at 04:55):Note that when the HoTT Book was written (2013), we didn't know whether the HIIT Cauchy reals coincided with the Escardo-Simpson reals, although the possibility was conjectured in the notes to chapter 11. This was proven by Auke Booij in 2017. So I don't think it was so unreasonable at that time to fail to say in the introduction that our construction of Cauchy reals could also be done in impredicative set theory, because we didn't know that it was the same construction. However, now that we do, it does seem reasonable to mention this.
https://github.com/HoTT/book/issues/1158
Mike Shulman (Jun 15 2024 at 05:02):@James E Hanson said:
Honestly, given the fact that two of the four bullet points comparing HoTT to set theory introduction of the book are pretty arguably wrong or at the very least misleading, I don't really feel confident in the accuracy of statements about set theory made in the rest of the book.
These four numbered points are not "comparing HoTT to set theory" in a general way. They are in the section of the introduction about constructivity, and are introduced with the following paragraph:
Fortunately, constructive reasoning is not as hard as it may seem. In some cases, simply by
rephrasing some definitions, a theorem can be made constructive and its proof more elegant.
Moreover, in univalent foundations this seems to happen more often. For instance:
In other words, the sole purpose of these numbered points is to argue that constructive HoTT is easier, or more elegant, than constructive set theory, for a mathematician coming from a classical background. I believe that even with your mathematical corrections (which I thank you for), all four of them still support this conclusion, although the latter two ess strongly. In (iii) the difference is now between simply truncating the universe and manually quotienting the universe by equinumerosity; and in (iv) the difference is that the HIIT construction does not require first constructing the Dedekind reals, and in particular also works predicatively.
Mike Shulman (Jun 15 2024 at 05:14):James E Hanson said:
If someone sits down and tries to write a (computably enumerable) constructive set theory that satisfies the disjunction and existence properties, then the same kind of fundamental computational restrictions apply.
It's true that some restrictions apply, but as far as I know there isn't the same sort of clear "harmony" picture in constructive set theories that there is in type theories. And unlike constructive type theory, constructive set theory is not itself a programming language.
The obnoxious aspect of the quote is that it's very hard for me to not read it as implying that the axioms of set theory are merely 'arbitrary,' which I would hope you would agree is not in fact true.
The specific axioms of particular set theories that people use in practice are not, of course, arbitrary. But that isn't what the quote says: it says that set-theoretic axioms can be chosen arbitrarily. In other words, you can write down an arbitrary collection of axioms about and get a first-order theory, whereas you cannot write down an arbitrary collection of rules and have a "type theory" in the computational sense.
As you say, if you posit that you want your set theory to be constructive, in the sense of the disjunction and existence properties, then that places restrictions on the axioms you can assume. But that is starting with the goal of constructivity. If you read the context, you find that two paragraphs earlier this discussion was introduced with
...type theory does encourage avoiding [LEM and AC] when they are unnecessary, for several reasons.
So this paragraph and the preceding one are arguing that even if we didn't start out with a goal of constructivity, there are separate reasons that type theory pushes us towards it. And yes, there is a difference between being constructive and being a programming language. The disjunction and existence properties are a consequence of the computational properties of type theory; we don't need to start out by desiring them. And the computational behavior of type theory (sans axioms) is necessary for practical implementations of it, in contrast to implementations of set theory where I would expect it suffices to have a "computational" interpretation of the underlying first-order logic.
Mike Shulman (Jun 15 2024 at 05:17):James E Hanson said:
Out of curiosity, I know that cubical type theory exists, but is there a computational interpretation of book HoTT in particular yet?
It depends a bit on what you mean by that, but I think the answer is basically yes. On one hand, in cubical type theory you can define an identity type that satisfies the rules of Book HoTT, and since cubical type theory is computational that gives you a way to compute with Book HoTT. On the other hand there is homotopy canonicity.
Graham Manuell (Jun 15 2024 at 10:40):@James E Hanson I don't know. Even if set theory were better at almost everything I think it would be reasonable to want to study or work in a system where junk theorems do not exist. Just as it might sometimes be desirable to use synthetic geometry. If I were advocating for the use of synthetic geometry for some purpose, I don't think I would necessarily be obligated to mention that for other purposes it might be much better to use analytic geometry instead.
I guess the distinction is that no one would be under the impression that synthetic geometry is good for all purposes, but that if someone advocates for something as a foundation for mathematics you believe that listeners will think it is capable of handling all the metamathematical issues you discuss above but this isn't (yet?) true. Is this an accurate description of your position or is there more to it?
Notification Bot (Jun 18 2024 at 08:15):310 messages were moved from this topic to #theory: category theory > Conflicting foundations by Morgan Rogers (he/him).
Paolo Scarpat (Jul 28 2024 at 08:43):John Baez said:
In September, Tom Leinster will teach a course on set theory at the University of Edinburgh. He'll be doing something new: instead of explaining ZFC, he'll explain [[ETCS]], Lawvere's Elementary Theory of the Category of Sets. But he won't talk about categories, since he's found that it's possible to state the axioms and work with them without first explaining any general concepts from category theory! Anyone interested can get a taste of this in his paper:
but he will be creating course notes with a much more detailed treatment, and make these available.
Is there already a syllabus for this course?
David Michael Roberts (Jul 28 2024 at 09:29):The course is not listed on Tom's page under teaching, yet.
Tom Leinster (Jul 28 2024 at 13:55):Paolo Scarpat said:
Is there already a syllabus for this course?
Sort of. This entry in our university's course catalogue covers instances when the course is taught using ZFC and when it's taught using ETCS. We deliberately made the descriptions loose enough that the lecturer would have the freedom to use any axiom system they wanted. The course runs in alternate years, and the one previous time it ran, it was taught using ZFC.
Our classes begin on 16 September. I'll probably post something publicly once semester gets going. But I have a lot of work to do between now and then!
David Michael Roberts (Jul 28 2024 at 23:27):Summary A first course in axiomatic set theory to include ordinals, cardinals, the axiom of choice developed in the axiom system chosen by the lecturer
Course description Paradoxes in nineteenth century mathematics showed that there is a need to be precise about the foundations of mathematics. Set Theory provides such a foundation. It also provides ways to deal with notions of infinity (through ordinal and cardinal numbers). The course will explore one or more such axiomatic formulations of Set Theory and show how to develop mathematics from these axioms as well as extensions of mathematics through ordinal and cardinal arithmetic. It will look at the axiom of choice and equivalents. Further topics may include model theory, large cardinals and/or independence proofs.
Paolo Scarpat (Jul 29 2024 at 07:57):Nice, thank you.
Tom Leinster (Sep 22 2024 at 09:28):The course has now begun, and I've posted the first chapter of the notes at the -Category Café. I'd suggest leaving comments there rather than here, so that they're all in one place.
David Michael Roberts (Sep 23 2024 at 03:33):Ironically, today I had to have the talk about how sets accidentally being equal, or overlapping, really wasn't a mathematical question. I had defined the tangent space of an affine variety in two different ways—actual tangent hyperplane in affine space at a point, and the Zariski tangent space, defined using pure algebra—and constructed an isomorphism between them, and my student asked "but what if they happen to be equal"?)
Mike Shulman (Sep 23 2024 at 05:56):Must be something in the stars. Last Friday my algebra students asked me a question about graph isomorphism, and when I saw their professor's definition of "graph" I was nonplussed to see that she required the vertex set and edge set to be disjoint. (She also required the vertex set to be nonempty, but I'm used to people getting things like that wrong.)
David Michael Roberts (Sep 23 2024 at 07:26):A bit like having to worry that hom-sets for a category are disjoint (which is actually real problem in ZFC, if one takes the naive view that the hom set from X to Y is literally just the set of functions from X to Y)
Julius Hamilton (Sep 23 2024 at 13:48):I am unable to comment on the n category cafe for some reason so I post my comment here.
It looks really good. I wish I could take that course, actually. I often felt in my first year of studying math more seriously that so many math textbooks bombard you with formal definitions and proofs and do not take the time to investigate all these really subtle questions of conceptual interpretation which to me are what completely makes the difference between understanding something competently and not doing so. The lecture notes actually go into those small details which I think is really important for beginners. I also like that the course is based on students bringing a written question to class; I myself sometimes imagined giving a very different kind of math course in the future where instead of just running through definitions and proofs it would be a totally open ended discussion type class where you can ask any question you want about math. I’ll definitely be following these notes.
Madeleine Birchfield (Sep 23 2024 at 15:00):David Michael Roberts said:
Ironically, today I had to have the talk about how sets accidentally being equal, or overlapping, really wasn't a mathematical question. I had defined the tangent space of an affine variety in two different ways—actual tangent hyperplane in affine space at a point, and the Zariski tangent space, defined using pure algebra—and constructed an isomorphism between them, and my student asked "but what if they happen to be equal"?)
The answer to the question also entirely depends on the foundations and their definition of equality. There are some consistent foundations in which given any isomorphism between two sets one can show that the two sets are equal.
John Baez (Sep 23 2024 at 16:21):Mike Shulman said:
Last Friday my algebra students asked me a question about graph isomorphism, and when I saw their professor's definition of "graph" I was nonplussed to see that she required the vertex set and edge set to be disjoint. (She also required the vertex set to be nonempty, but I'm used to people getting things like that wrong.)
Too bad they left out the one case where it's really safe to say those sets are disjoint. :upside_down:
Tobias Fritz (Sep 23 2024 at 17:47):Sorry if this is off-topic here, but does anyone else have issues with the n-Café's RSS feed? I use Thunderbird as my RSS reader, and it used to work just fine until recently, and all other feeds except for the n-Café still work as of now. But the n-Café itself currently gives me an 'https://golem.ph.utexas.edu/category/atom10.xml is not a valid feed' error. Does anyone else have this issue or know what the problem might be?
It's only thanks to Tom's comment here that I've realized that there is new content on the café.
Nathanael Arkor (Sep 23 2024 at 17:50):The xml feed you link seems to be working for me :thinking:
Tobias Fritz (Sep 23 2024 at 17:55):Thanks! Yes, my browser also displays the link correctly... I've now gotten Thunderbird to tell me what the error is, and it complains about invalid XML in an equation:
image.png
image.png
Tobias Fritz (Sep 23 2024 at 18:02):Actually the w3.org validator displays the same error, so I guess it is indeed wrong syntax.
John Baez (Sep 23 2024 at 18:44):Tobias Fritz said:
Sorry if this is off-topic here, but does anyone else have issues with the n-Café's RSS feed? I use Thunderbird as my RSS reader, and it used to work just fine until recently, and all other feeds except for the n-Café still work as of now. But the n-Café itself currently gives me an 'https://golem.ph.utexas.edu/category/atom10.xml is not a valid feed' error. Does anyone else have this issue or know what the problem might be?
No, only Jacques Distler would know: he's the guy who runs the n-Cafe. I'll email him. @Tom Leinster recently emailed him about other new problems with the n-Cafe, so I'll join that thread.
It's only thanks to Tom's comment here that I've realized that there is new content on the café.
Ah, maybe that's part of why my new posts on the moduli space of physical frameworks have received a depressing paucity of responses.
Tobias Fritz (Sep 23 2024 at 18:47):Great, thank you! I'll try to catch up a bit.
John Baez (Sep 23 2024 at 21:35):Jacques says the RSS feed should be working now. Give it a try, @Tobias Fritz.
Tobias Fritz (Sep 24 2024 at 04:11):Wow, that was quick :astonished: Yes, it works, and I had not realized before that the comments feed is actually threaded -- awesome!
Tom Leinster (Sep 27 2024 at 13:02):Chapter 2 is now up.
David Michael Roberts (Sep 28 2024 at 10:45):I tried commenting at the Café, @Tom Leinster but it got eaten and didn't appear. I wanted to just remark for the purposes of those reading along and learning who are wanting to know: the category-theoretic description of the structure so far might be of interest. So you have a cartesian closed category such that 1 is a separator, and with some object O such that there are no functions 1 -> O.
I'm feeling a little lazy, but I should check if with just these axioms it shows that O is strict initial (the vacuity of there being no elements in O makes we wary of applying well-pointedness!), and so then one could rephrase it it terms of "there is a strict initial object 0 and 1 is not iso to it.
David Michael Roberts (Sep 28 2024 at 11:15):Gah, you say that in the notes at this point one cannot prove all empty sets isomorphic, so of course you don't yet have an initial object.
Vincent Moreau (Sep 28 2024 at 11:27):Indeed, there are examples even among posetal CCCs, as exemplified by the 3-element chain
which is a well-pointed CCC such that there is no morphism . In a posetal CCC, having a morphism means that is terminal, which gives a lot of examples for your question.
Tom Leinster (Sep 28 2024 at 11:40):@David Michael Roberts Jacques Distler, who as you know runs the Café, has been doing some major work behind the scenes recently, and the problem with your comment may have been a consequence of that. In any case, I've mailed him to report the error message that your comment generated. No idea what the issue was.
Vincent Moreau (Sep 28 2024 at 11:41):On the other hand, suppose that we want to go in the opposite direction: instead of considering a posetal CCC, we consider a well-pointed category with terminal object such that there exists a unique object such that there is no morphism . In that case, we can show that is weakly initial, as for any object ,
and by well-pointedness, this morphism is unique so is initial. In particular, this applies to CCCs.
David Michael Roberts (Sep 28 2024 at 12:16):Thanks, @Tom Leinster !
David Michael Roberts (Sep 28 2024 at 12:18):@Vincent Moreau I don't see how to rule out O having non-identity endomorphisms...
David Michael Roberts (Sep 28 2024 at 12:19):Or that is down to any map out of O being equal to any other by vacuity of the wellpointedness condition? It's late here and I'm not braining much.
David Michael Roberts (Sep 28 2024 at 12:21):Feels like some classical logic reasoning here, which is perfectly appropriate for the context, but sometimes I have to actively engage the double-negation elimination module in my brain.
Vincent Moreau (Sep 28 2024 at 12:23):David Michael Roberts said:
Or that is down to any map out of O being equal to any other by vacuity of the wellpointedness condition? It's late here and I'm not braining much.
Exactly
David Michael Roberts (Sep 28 2024 at 12:44):Ok. Though assuming uniqueness of O is of course too strong from an ETCS pov, even if it's true in material set theories...
Vincent Moreau (Sep 28 2024 at 12:58):Indeed, I just wanted to give a sufficient condition in which you could deduce the fact that is initial, and which thus would rule out the counter-example that I first mentioned.
Tom Leinster (Sep 28 2024 at 16:31):@David Michael Roberts I just posted your comment on the Café. Jacques has had a look at the problem and it's to do with control characters, which I think in your case means it was related to the dashes in your comment. Anyway, we can proceed with the mathematical conversation over there.
David Michael Roberts (Sep 29 2024 at 12:44):Thanks again, @Tom Leinster ! I guess I am in the habit of using the correct dash-types—and didn't realise it would mess up the comment.... :-/
Mike Shulman (Sep 29 2024 at 16:24):It shouldn't!
Tom Leinster (Sep 29 2024 at 19:03):No, it shouldn't! And obviously it's not your fault. Jacques is mystified as to how your comment (or more specifically the dash characters in it) was accepted and yet caused the system to choke.
John Baez (Sep 29 2024 at 20:20):What kind of dashes, @David Michael Roberts? The usual
- -- ---
or some funky unicode ones? I want to see if the problem is fixed.
David Michael Roberts (Sep 29 2024 at 20:43):@John Baez an em-dash character, yes.
John Baez (Sep 29 2024 at 21:27):Did you enter an em-dash character in UNICODE, or did you do what I always do, which is write ---?
John Baez (Sep 29 2024 at 21:28):I find the nLab is quite unforgiving when it comes to anything but the most basic UNICODE, at least when posting articles (which is subtly different from posting comments, for some mysterious reason).
David Michael Roberts (Sep 29 2024 at 21:47):I used the Mac keyboard shortcuts to write an em-dash. I can only presume this is Unicode. I don't know if the n-Café converts the TeX commands for en- and em-dashes to the correct glyphs.
David Michael Roberts (Sep 29 2024 at 21:48):The nLab and nForum are running different software, so I'm not surprised that they process stuff differently. I guess I could instead look up the HTML commands for the dashes and use those on the Café....
John Baez (Sep 29 2024 at 21:51):I see. You're living a life of danger. When posting articles on the n-Cafe, the main way I get stuck in endless error message is to cut-and-paste people's text containing symbols like unicode emdashes:
—
curly quotation marks:
“ ”
or apostrophes:
’
John Baez (Sep 29 2024 at 21:53):I have to root these out and replace them with basic ASCII symbols:
---
" "
'
David Michael Roberts (Sep 30 2024 at 01:07):Gosh, now I can't even post a comment not using Unicode.... Here's my input verbatim:
Another thing to note for people ok with categories: assume we have the category Set, and are trying to instead characterise it, rather than axiomatise it.
Assume that the category $C$ described by the axioms so far is locally small (which will probably follow from later axioms, but for now I have to assume separately). Then the global points functor $Hom(1,-): C\to Set$ is faithful, preserves cartesian products and terminal objects, and sends $O$ to $\emptyset$. So far the full subcat $C$ of $Set$ consisting of just an initial and a terminal object seems to be a model, as it is cartesian closed subcat.
John Baez (Sep 30 2024 at 05:17):I had no trouble posting this comment verbatim, but I deleted it because I didn't want to post it under my name. If you want me to post it and say it's from you, I can do that.
David Michael Roberts (Sep 30 2024 at 06:52):Weird, it worked now.
Tom Leinster (Oct 04 2024 at 16:13):Chapter 3 is now up.
Tom Leinster (Oct 11 2024 at 10:45):Chapter 4: Subsets is now up.
Tom Leinster (Oct 18 2024 at 15:38):Chapter 5: Relations is now up. It is about relations, but I should have called it "Specifying subsets and functions", because that's what it's really all about.
David Michael Roberts (Oct 18 2024 at 23:50):@Tom Leinster Typo in Example 5.1.16 ? It refers to an X but without defining it - I think it should be |R instead.
Tom Leinster (Oct 19 2024 at 18:00):Thanks, David.
Todd Trimble (Oct 19 2024 at 19:06):Tom, I plan to dig in when I have more time. I hope you're getting good feedback from the students!
Tom Leinster (Oct 20 2024 at 19:39):I look forward to your comments, Todd!
Tom Leinster (Oct 20 2024 at 19:44):I'm getting lots of feedback from the students (which is one sense of "good feedback"!). As I think I mentioned at the Café, each of the students is supposed to bring one written question to each class, based on the reading they've done. There are 53 students enrolled, so in principle that's 53 questions twice a week, each revealing a point they find difficult. In practice it's much less than that, but still, it's an absolutely invaluable guide to what I could do better next time.
Tom Leinster (Oct 26 2024 at 14:08):Chapter 6: Gluing is now up.
Tom Leinster (Nov 01 2024 at 14:27):And here's Chapter 7: Number systems.
After this, there are three more chapters to go: well ordered sets, the axiom of choice, and cardinal arithmetic.