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.