2
$\begingroup$

The ETCS axioms give conditions on a category for it to be a category of sets. These axioms can be written out in first order language, resulting in a finite axiomatisation of the category of sets. Given a model of ZFC one can form the associated category of sets and this will satisfy the axioms. On the other hand, the axioms do not require a priori defined sets. (The existence of a model of the ETCS axioms then is probably on par with the assuption there exists a model of the ZFC axioms) The appropriate definition of map between ETCS categories is a geometric morphism.

Is it possible to define geometric morphisms elementarily? In first order language?

Then one can define the category of ETCS categories and consider the relations between models. This is related to my previous question.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

Yes, it is possible. Precisely, we can write down a first-order theory for which a model is a pair of ETCS-models and a geometric morphism between them (am I right in thinking this is what you're asking for?).

To do this, on top of axiomatising “a pair of models of ETCS”, you add some extra function symbols for the adjunction. The conditions of functoriality, etc. are easily written algebraically; the adjunction can be expressed in various ways, of which the simplest to write down is probably the triangle-inequalities form. “Preserving finite limits”, when you write it out, is also just a scheme of first-order conditions; if you want to reduce it to a finite axiomatisation, note that it's enough to ask for preservation of finite products and equalisers (by the usual proof that all finite limits can be constructed from these).

This said, I disagree somewhat with an implicit premise of your question. You say: “Then one can define the category of ETCS categories…” But to do this, you don't need to show that geometric morphisms can be defined in first-order terms. To talk about “the category of ETCS categories”, you already need to be working in a meta-theory with some sort of notion of set or similar (eg types, etc.); and so don't need the definitions of the morphisms to be first-order.

The foundational advantage of a first-order axiomatisation of widgets is that you can then study a single widget without needing any meta-theory. But to study the collection of all widgets (as a category or whatever else), you still need a meta-theory.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Is NBG a sufficient meta-theory to study the category of all models of ETCS+(some large cardinal axiom)? $\endgroup$
    – Harry Gindi
    Commented Oct 20, 2010 at 2:22
  • 1
    $\begingroup$ Absolutely! But tbh, it's probably overkill. To do basic model theory of any first-order logical system, assuming you want the usual completeness theorem and things, your minimal metatheory is probably something like ZC (I don't believe you need replacement, though I wouldn't swear to this); a reverse-mathematician could surely sharpen this up a bit. If you want to prove existence of models, then replacement is enough: sets of cardinality bounded by any strong limit cardinal (eg $2^{2^{\ddots ^ \omega}}$) give a model of bounded Zermelo set theory, and hence of ETCS. (cont’d) $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Oct 20, 2010 at 2:41
  • 1
    $\begingroup$ On the other hand, for large cardinal axioms, as usual, you get what you pay for: the more you put into your meta-theory, the more you'll get back in existence of models. I'm not sure if the distinction between ZFC-style and NBG-style is particularly relevant here: the advantage one might expect in NBG, that it might allow one to talk about class models, is (if I'm not mistaken) illusory: how do you define satisfaction of formulas in putative class models? (Satisfaction is a recursive definition, and one can't generally recurse over classes, thanks to the restriction on comprehension) $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Oct 20, 2010 at 2:53
  • $\begingroup$ So a theory can only model theories weaker than it? $\endgroup$
    – Harry Gindi
    Commented Oct 20, 2010 at 3:58

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .