Category Theory
Zulip Server
Archive

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.

Stream: deprecated: logic

Topic: ∃∀∃ statements in geometric logic

Morgan Rogers (he/him) (Apr 07 2022 at 12:32):

A fragment of logic often considered in topos theory is geometric logic. A geometric theory is based on a signature as one might expect (one may have finitary relation symbols, function symbols, or both), and we are allowed to construct formulae by finitary conjunctions, existentials, and arbitrary ("small") disjunctions [note that disjunctions and conjunctions aren't allowed to be dependent here]. Axioms of a geometric theory are "sequents", taking the form $\phi \vdash_{\vec{x}} \psi$, where $\phi,\psi$ are geometric formulas and $\vec{x}$ is a 'context' containing all of the free variables (with types consisting of sorts) appearing in $\phi$ or $\psi$. The intended interpretation of this is "for all possible values of the variables in $\vec{x}$, if $\phi$ holds, then $\psi$ holds".

Since the formulas are allowed to be built with existential quantifiers but not universal quantifiers, this generally enables us to construct formulae presenting first order (infinitary) ∀∃ statements. However, extending these to ∃∀∃ statements seems impossible in general.

Consider, for example, the theory of categories (this is an essentially algebraic theory, and considering it as such we will only build the 1-category of categories as models of the theory in Set). An extension of this theory is the theory of categories having a terminal object. If we expand the signature for the theory of categories to include the terminal object as a constant, we have no problem expressing this as a geometric theory. However, the result is the theory of categories with a chosen terminal object. If I want to present the theory of categories with an unspecified terminal object, I need an ∃∀∃ statement, "there exists an object $t$ such that for all objects there exists a unique morphism from that object to $t$". Is it possible to express this in geometric logic?

The reason I suspect this should be the case is that there is a localic geometric morphism from the classifying topos for "categories with a terminal object" to the classifying topos for categories. The surjection-inclusion factorization of this morphism produces a subtopos of the latter topos, which classifies a quotient of the theory of categories (a theory obtained by just adding axioms); this subtopos is the minimal subtopos such that every category with a chosen terminal object has a classifying morphism (as a category, ignoring the chosen terminal object) which factors through the subtopos. First-glance intuition says that this subtopos should classify the theory of categories having an unspecified terminal object!
On the other hand, it being possible might amount to the claim that given a category with at least one terminal object I can always choose one, which taken altogether looks like an unreasonable choice principle. Any suggestions?

David Michael Roberts (Apr 07 2022 at 13:05):

The category C having a terminal object is expressible as the functor from C to 1 having a right adjoint functor. You could instead express it as the existence of a right adjoint anafunctor, which amounts to a functor from a contractible groupoid such that (condition). Not completely sure it would help, but anafunctors were invented to de-choiceify operations defined only up to unique isomorphism via a universal property (eg binary products: having a product functor amounts to choosing a product for each pair, etc etc).

Another idea is to get a fibrational description, a la Bénabou. Maybe Streicher's notes on fibrations (on the arXiv) has a working definition. Can't think offhand what the quantifier complexity is for a cartesian lift to exist, though.

Last, the inner existential is in this case more like $\exists !$, which means you can treat the $\forall \exists$ more like an operation. I'd personally think of the first existential in terms of internal logic/stack semantics, which means passing up a surjection, which feels very geometric to me. If you are thinking about $\exists \forall \exists$ more generally, though this won't help.

Graham Manuell (Apr 07 2022 at 13:07):

Here's a possible solution. Consider the theory of categories with an additional unary relation (i.e. subobject) R of the type of objects. Add an axiom that says every element of R is terminal and another saying that R is inhabited.

Graham Manuell (Apr 07 2022 at 13:16):

I think this approach should actually work for all $\exists\forall\exists$ statements.

Morgan Rogers (he/him) (Apr 07 2022 at 15:00):

Adding a relation symbol is still typically a localic extension, though: any homomorphism of the structure carrying the extra unary relation must preserve that relation, whereas generic functors do not preserve terminal objects. In other words, adding a relation to the theory isn't the same as just adding an axiom.

Morgan Rogers (he/him) (Apr 07 2022 at 15:21):

@David Michael Roberts your first few suggestions sound too category specific to be right to me, and the essential uniqueness definitely won't help: as I mentioned, I'm dealing with 1-theories and so only have the 1-category if categories at my disposal, and there can be several (isomorphic but not equal) terminal objects in a category.

I realise now that even $\exists\forall$ statements are tricky... an example would be to consider the theory of monoids, and wanting to extend this to a theory of monoids having a right absorbing element. "There exists an r such that for all m, rm=r". How would one express this as a geometric sequent? (Or several sequents?)

Graham Manuell (Apr 07 2022 at 15:21):

Yes. True. I don't know what the subtopos is, but this does seem to work for dealing with $\exists \forall \exists$ statements at least. I imagine that the subtopos is going to be a slightly weaker condition than existence, but I'm not sure.

Mike Shulman (Apr 07 2022 at 15:48):

I conjecture that this surjection-inclusion factorization is the classifying topos for categories having the property that any finitely presented subcategory can be extended to one in which there is a terminal object (of the subcategory).

Morgan Rogers (he/him) (Apr 07 2022 at 17:12):

That seems sensible, I was coming around to the same conclusion on my journey home for the monoid example. Finite formulas can only see finitely presented subcategories, and this remains true for infinite disjunctions. Thanks for the speculation, folks!

Mike Shulman (Apr 07 2022 at 17:17):

I remember thinking about the similar situation of the map from the classifying topos of monoids to the classifying topos of semigroups, and concluding that the intermediate factor was the classifying topos of semigroups in which any finitely generated sub-semigroup has an identity element.

David Michael Roberts (Apr 07 2022 at 20:18):

Yeah, sorry, my brain is too much in the semantics side.