On Sun, Dec 3, 2017 at 8:12 AM, Neil Barton <bartonna@gmail.com> wrote:
though---here we are expected to take the *class* of all well-founded extensional accessible pointed graphs, and note that ZFC holds within this class. Whilst I'm happy that the lemmas showing that the required graphs exist in the category Set are categorial, it seems to me that to isolate all these and talk about the *class* of all of them requires some material-set-theoretic machinery. Is there a *purely categorial* way of talking about this `collection' of subgraphs in Set? Or have I missed something?
This is one of the reasons I don't like the term "categorical" (or "categorial") set theory: it suggests that ETCS is somehow a different "kind of theory" than ZFC which "uses categories instead of sets". Actually ETCS and ZFC are both ordinary first-order theories, and we can discuss their models and translations between them just as we would for any other first-order theories. (Well, it's a bit more natural to formulate ETCS as a dependently typed first-order theory, but that's not really relevant to the point.) If we want to prove that two theories are equiconsistent by constructing a model of each one from a model of the other, then this construction can only happen in the metatheory, since otherwise we would instead be proving the consistency of one theory inside the other one. A model of ZFC consists of a collection of things (a "set" in the metatheory, whose elements are the "sets" of the model) equipped with a membership relation satisfying axioms. A model of ETCS consists of two collections of things (two "sets" in the metatheory, whose elements are the "sets" and "functions" of the model) equipped with domain, codomain, composition, and so on satisfying axioms. The two constructions back and forth happen in the metatheory, and they are, like most of mathematics, structural, which means it doesn't matter whether the "sets" of the *metatheory* obey ZFC or ETCS. So no, the construction doesn't require any "material" set-theoretic machinery, but it does require some set-theoretic machinery in the metatheory, which should not be surprising. (On the other hand, if we instead view the "construction" as a syntactic translation of ZFC-formulas into ETCS-formulas, then we don't need to talk about models at all, and less is required of the metatheory.)
extra axiom to be added to ETCS+: ``Set contains an well-founded extensional accessible pointed graphs such that...[list the APG ZFC axioms].''. Is this acceptable in a *pure* categorial framework, or do you think that presupposes some material set theory?
One could certainly suppose such an axiom, and any axiom you add to ETCS will be an axiom of ETCS and therefore structural. But this particular axiom would be making ETCS stronger by essentially adding a kind of universe to it, and it's not necessary for the translation to ZFC, which as I said generally happens in the metatheory.
I suppose there is also the question of how to recover the cumulative hierarchy in this framework---in the paper you sent me this is done with a non-categorial theory of ordinals (possibly given by material set theory).
One might use a ZF-like set theory as the metatheory since it's more familiar, but actually the construction of the cumulative hierarchy in a topos is, like most of mathematics, also structural, so it doesn't matter what choice you make. There's nothing "non-categorial" about ordinals as long as you define them correctly (transitive well-founded relations) to free them of dependence on the global membership predicate. But the ordinals in that construction are indeed external to the topos. On the other hand, the point of the theorems following that construction in my paper is that one doesn't need to use external ordinals, but can recover essentially the same model by building accessible pointed graphs internally.
(This relates to a more general question I have concerning categorial foundations: Are there people who claim we should do foundational research *solely* in the language of category theory, or does almost everyone accept that the `external' (possibly material set-theoretic) perspective is also allowed? So, for example, when considering the category of sheaves over a topological space, whilst I could take a purely categorial outlook, nonetheless sometimes I might want to just look at the equivalence class of an open set U relative to a point i in the topological space defined in material set theory.
I don't understand how the latter is an example of the former. Are you talking about the "etale space" associated to a sheaf? That makes perfect sense internally and structurally/categorially.
It *seems* to me (without any deep arguments for the claim) that material set theory is just better suited to certain roles (such as the formulation of large cardinal hypotheses) whilst structural set theory better suited to systematising the algebraic roles we want sets to perform.
Surprisingly many large cardinal hypotheses can be formulated in a purely structural way. But it's true that there are plenty of notions in ZFC-theory that would (at least apparently) be awkward to formulate structurally. One particularly striking one is Godel's constructible universe L; I've never seen any sort of category-theoretic explanation of that. (Which is not to say that one can't exist; I consider this to be an important open problem.) Another thing that's a bit awkward in actually using ETCS as a formal foundation for mathematics is that there is no *single object* in ETCS that can be defined to be (say) "a group". In ZFC a group (or any structure) can be formally defined as a tuple consisting of the carrier set(s) and the operations or other structure on them, and such a tuple is itself (by Kuratowski encoding) a set, hence an object of the foundational theory ZFC. But in ETCS, sets cannot be *elements* of other sets or tuples, so there is no way to "package up" an entire structure into a single object; we have to do the "tupling up" in the metatheory. Type theory is a better foundation than ETCS for this sort of thing. As for ETCS, I think that one of the most important things it can do better than ZFC is (especially in its intuitionistic version) function as an internal language for toposes. The cumulative hierarchy or accessible-pointed-graphs construction is a hack to interpret ZFC in part of a topos, but it's not the natural way to go about it and it doesn't even see all of the topos in general. So overall, yes, I would agree that the two perspectives are best viewed as complementary. Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]