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.
Leopold Schlicht (Sep 05 2021 at 12:23):What's the most natural categorical structure corresponding to first-order logic? What kind of category should the syntactic (classifying) category of a first-order theory be (so what's the right analogue of the Lindenbaum–Tarski algebra of a propositional theory)? I've picked up several keywords:
What's conceptually the difference between these approaches?
Matteo Capucci (he/him) (Sep 05 2021 at 14:10):An Heyting pretopos is what you get by 'realizing' a first-order hyperdoctrine in its quotient completion, i.e. by using the hyperdoctrine to generate a pretopos embodying the same logic (I can elaborate). Indeed, any pretopos gives a first-order hyperdoctrine of subobjects and these two constructions form an adjunction.
[N.B.: definitions here a bit slippery: you surely need your hyperdoctrine to be at least extensive to get a pretopos (and I don't know what 'first-order' is taken to mean in this context), but the intuitions are right: pretopoi and first-order hyperdoctrines both embody a first-order intuitionistic (that's the 'Heyting' part) theory]
Matteo Capucci (he/him) (Sep 05 2021 at 14:10):I can elaborate on the details if you want
Mike Shulman (Sep 05 2021 at 14:21):In general, there isn't just one "right" analogue. The differences are that a hyperdoctrine maintains a semantic separation between types and propositions, while a Heyting category incarnates propositions as subobjects of types, and a pretopos adds coproducts and quotients.
Fawzi Hreiki (Sep 05 2021 at 15:56):Depending on your definition, pretoposes and Heyting categories are particular cases of hyperdoctrines (namely those where the psuedofunctor/fibration is the subobject one)
Fawzi Hreiki (Sep 05 2021 at 15:57):The benefit of working with a Heyting category rather than a more general Heyting hyperdoctrine is that the logic already comes packaged with the category so-to-speak
Leopold Schlicht (Sep 07 2021 at 18:05):Thanks!
I guess probably there's only one canonical notion of "translation between first-order theories" or "interpretation of one first-order theory in another". (Although I can't find a Wikipedia page on that notion, for instance. So probably that's not an established notion, which is weird, because I think this concept is quite fundamental.)
When I talk about the right kind of categorical structure corresponding to first-order logic I mean a type of category such that the category of all categories of that type is equivalent to the category of first-order theories and translations between them. Which of the three categories (pretoposes, Heyting categories, first-order hyperdoctrines) satisfies this requirement? Are the other two categories equivalent to some other notion of "theories and translations between them"? If yes, which?
Mike Shulman (Sep 07 2021 at 18:59):Each of them corresponds to a different notion of "translation".
Mike Shulman (Sep 07 2021 at 19:02):When you translate theory A to theory B, you can choose whether to interpret each base type in A as either (0) a base type in B, (1) an arbitrary type in B, (2) a subobject of a type in B, or (3) a subquotient of a type in B. (Maybe you could just choose a quotient too, but I'm not sure what that would correspond to categorically.) Choices (1), (2), and (3) yield respectively notions of translation that correspond to morphisms of first-order hyperdoctrines, Heyting categories, and Heyting pretoposes. (In all cases I'm assuming that primitive propositions in A are mapped to arbitrary propositions in B.)
Leopold Schlicht (Sep 08 2021 at 18:56):That's amazing! So the underlying class of objects of the theories-category the category of pretoposes / Heyting categories / first-order hyperdoctrines is equivalent to is in each case the class of all first-order theories, but the morphisms are different?
You mentioned Heyting pretoposes. What about pretoposes? (EDIT: That also occurs in another thread.)
What are the morphisms between Heyting pretoposes?
Mike Shulman (Sep 08 2021 at 19:21):Sorry, I meant Heyting pretoposes here. Heyting pretoposes are the completions of Heyting categories under coproducts and quotients, so they're the right thing to look at when talking about first-order logic. Their functors are just functors of Heyting categories, which automatically also preserve coproducts and quotients. Plain pretoposes are for coherent logic, not first-order logic.
Leopold Schlicht (Sep 08 2021 at 19:53):Thanks!
Leopold Schlicht (Jan 29 2022 at 13:25):Mike Shulman said:
When you translate theory A to theory B, you can choose whether to interpret each base type in A as either (0) ..., (1) ..., (2) ..., or (3) a subquotient of a type in B.
What do you mean by "type" here? Isn't a quotient of a type in B also a type in B? And isn't a subtype of a type in B also a type in B?
Are the "types in B" you are talking about closed under coproducts?
And why in that particular order (first quotient type, then subtype)? Why not allowing coproducts of quotients of subtypes of types in B too (and so on)?
Mike Shulman (Jan 29 2022 at 15:57):A "type" is a syntactic object here. So if the theory in question doesn't include subtypes or quotient types, which is usually the case, then no. It's more common to include coproduct types, but if we don't, then to get morphisms of pretoposes we would have to use subquotients of coproducts as you suggest.
Mike Shulman (Jan 29 2022 at 15:57):A "subquotient" is either a subobject of a quotient or a quotient of a subobject; the two are the same in reasonable categories.
Mike Shulman (Jan 29 2022 at 15:58):Similarly, in a pretopos a coproduct of subtypes, quotients, or subquotients is also a subtype, quotient, or subquotient or a coproduct. So there's a "canonical form" and you don't have to keep iterating.
Leopold Schlicht (Jan 29 2022 at 17:24):Thanks, that's enlightening!
Similarly, in a pretopos a coproduct of subtypes, quotients, or subquotients is also a subtype, quotient, or subquotient or a coproduct.
I guess the last "or" should be an "of". :grinning_face_with_smiling_eyes:
Mike Shulman (Jan 29 2022 at 17:53):yes