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: learning: questions

Topic: classifying toposes

Leopold Schlicht (Sep 01 2021 at 15:12):

Given a geometric theory $\mathbb T$, why is it natural (from the point of view of categorical logic) to consider its classifying topos $\mathcal E_\mathbb T$?

What is totally natural (from the point of view of categorical logic) is to construct the syntactic geometric category $\mathcal C_\mathbb T$ of $\mathbb T$ and prove that the geometric functors $\mathcal C_\mathbb T\to\mathcal C$ correspond to the $\mathbb T$-models in $\mathcal C$, for any geometric category $\mathcal C$. (I barely know anything about the history, but this could be very close to Lawvere's idea of "functorial semantics", from what I've picked up.) But note that the syntactic category $\mathcal C_\mathbb T$ is a geometric category and not a Grothendieck topos.

To get from $\mathcal C_\mathbb T$ to the classifying topos $\mathcal E_\mathbb T$, I think what one does is that one equips $\mathcal C_\mathbb T$ with a "syntactic" Grothendieck topology and then sets $\mathcal E_\mathbb T$ to be the topos of sheaves on that site. Employing Diaconescu's theorem, one should get the equivalence between geometric morphisms $\mathcal E_\mathbb T\to\mathcal E$ and $\mathbb T$-models in $\mathcal E$, for each Grothendieck topos $\mathcal E$.

However, it seems to me that this works just by accident, and I don't see any a priori reason that forces one to come up with Grothendieck toposes instead of geometric categories when just interested in categorical logic. Also, I think it's quite surprising that each Grothendieck topos is the classifying topos of some geometric theory.

So what I want is: convince me that what I wrote in the last paragraph is wrong! :-) It would be really cool if Grothendieck's original conception of space -- Grothendieck toposes and geometric morphisms -- naturally shows up in categorical logic, and not just modifications of that concept adjusted to logic (like elementary toposes and logical morphisms).

Zhen Lin Low (Sep 01 2021 at 15:33):

I think there's an easier (in the sense of being more direct) construction: the exact completion of the geometric syntactic category is the classifying topos. So all you're adding is quotients – which, if you think about it, don't really exist in geometric logic.

Morgan Rogers (he/him) (Sep 01 2021 at 15:52):

There's also a motivation of bridging the gap between classical model theory and categorical logic here: if you'll concede that Grothendieck toposes represent "mathematical universes" where one can perform all of the (constructive...) categorical operations inherited from sets, then these are the categories where we want to consider models of our theories.
At that point, either we can leverage Zhen Lin Low's argument to reason that passing to the exact completion is more than sensible, since any geometric functor to a topos will canonically factor through that, or you can consider the universal property of the classifying topos as a representability property regarding pseudofunctors on the bicategory of Grothendieck toposes (cf Part B of Sketches of an Elephant), and having a representing object in the same context as you are examining the models of your theory has some convenient theoretical consequences.

Nathanael Arkor (Sep 01 2021 at 15:59):

This is a point I believe had confused me previously too. What is the right way to see this relationship 2-categorically, i.e. the relationship between the 2-category of geometric categories, and the 2-category of Grothendieck topoi (without recourse to syntax or theories)?

Morgan Rogers (he/him) (Sep 01 2021 at 16:06):

Grothendieck toposes are geometric categories, so we have a full inclusion of 2-categories of G'toposes into geometric categories, having a left adjoint (which turns out to amount to exact completion). As for how large the distinction is, I have little grasp on it, and I lack the means to articulate it too!

Nathanael Arkor (Sep 01 2021 at 16:09):

Thanks. It makes me curious in what other syntactic/logical settings this phenomenon arises.

Nathanael Arkor (Sep 01 2021 at 16:14):

If it's the case that this works for any reflective sub-2-category, then presumably one would want to choose the "nicest" such sub-2-category to work within for the purpose of classifying constructions. Does the 2-category of Grothendieck topoi have some universal property with respect to the 2-category of geometric categories, I wonder?

Leopold Schlicht (Sep 03 2021 at 17:46):

Zhen Lin Low said:

I think there's an easier (in the sense of being more direct) construction: the exact completion of the geometric syntactic category is the classifying topos. So all you're adding is quotients – which, if you think about it, don't really exist in geometric logic.

What's the motivation for considering the exact completion of the syntactic category?

Leopold Schlicht (Sep 03 2021 at 17:56):

For instance, I've never seen people talking about some kind of completion of the (cartesian closed) syntactic category of a theory in the $\lambda$-calculus. So why should one consider a completion in the case of geometric theories and geometric categories?

Leopold Schlicht (Sep 03 2021 at 18:01):

Morgan Rogers (he/him) said:

There's also a motivation of bridging the gap between classical model theory and categorical logic here: if you'll concede that Grothendieck toposes represent "mathematical universes" where one can perform all of the (constructive...) categorical operations inherited from sets, then these are the categories where we want to consider models of our theories.

If you are interested in geometric theories, then geometric categories are the natural kind of universes in which the models of your theories live. Your argument explains why it is natural to consider toposes when wanting to interpret higher-order logic. But that's not what my question is about.

Mike Shulman (Sep 03 2021 at 19:53):

One possible answer is that maybe we aren't actually interested in geometric theories as usually formulated, but rather in "geometric-with-quotients" theories. Any syntactic geometric theory can trivially be regarded as a geometric-with-quotients theory that doesn't use the quotients, just as an algebraic theory can trivially be regarded as a theory in $\lambda$-calculus that doesn't use the function-types, and its syntactic category qua geometric-with-quotients theory will be the exact completion of its syntactic category qua geometric theory. This is an instance of a very general notion of "change of doctrine" or "enrichment of structure".

Mike Shulman (Sep 03 2021 at 19:54):

In this case it happens that geometric logic is expressive enough that every geometric-with-quotients theory is Morita equivalent to (the extension to a geometric-with-quotients theory of) some geometric theory.

Mike Shulman (Sep 03 2021 at 19:56):

Another, related, answer, is that by lifting our geometric theories to geometric-with-quotients theories we obtain more morphisms between them. A semantic morphism of geometric theories (i.e. a geometric functor between syntactic categories) has to send sorts of one theory to, essentially, subobjects of products of sorts of the other. But I'm sure there are natural examples where we'd like to have a "morphism" between such theories but it should really only send sorts of one to quotients of subobjects of products of sorts of the other. So that would be a morphism of geometric-with-quotients theories --- i.e. a geometric morphism of classifying toposes --- but not a morphism of geometric theories.

Morgan Rogers (he/him) (Sep 05 2021 at 09:27):

Leopold Schlicht said:

Morgan Rogers (he/him) said:

There's also a motivation of bridging the gap between classical model theory and categorical logic here: if you'll concede that Grothendieck toposes represent "mathematical universes" where one can perform all of the (constructive...) categorical operations inherited from sets, then these are the categories where we want to consider models of our theories.

If you are interested in geometric theories, then geometric categories are the natural kind of universes in which the models of your theories live. Your argument explains why it is natural to consider toposes when wanting to interpret higher-order logic. But that's not what my question is about.

I would agree that geometric categories have the minimal structure required to interpret geometric logic. On the other hand, the reason that geometric logic was developed in the first place was because it is the fragment of logic which is respected by geometric morphisms, which is to say morphisms of toposes. I would challenge you to present me with a geometric category which is not a Grothendieck topos and which is not simply constructed as the syntactic category of a geometric theory.

Leopold Schlicht (Sep 05 2021 at 12:42):

Morgan Rogers (he/him) said:

I would challenge you to present me with a geometric category which is not a Grothendieck topos and which is not simply constructed as the syntactic category of a geometric theory.

Shouldn't every geometric category $\mathcal C$ be the syntactic category of some geometric theory (such as the "internal language" of $\mathcal C$)? (I haven't thought about any details though.)

Leopold Schlicht (Sep 05 2021 at 12:48):

@Mike Shulman Thanks, that helps a lot!

You talk about semantic morphisms between theories. Can these be formulated syntactically ("has to send sorts of one theory to, essentially, subobjects of products of sorts of the other" sounds quite syntactic!)?

I've also always wondered: can Morita equivalence of geometric theories be characterized syntactically using a notion of syntactic translation between theories?

Morgan Rogers (he/him) (Sep 05 2021 at 14:16):

Leopold Schlicht said:

Morgan Rogers (he/him) said:

I would challenge you to present me with a geometric category which is not a Grothendieck topos and which is not simply constructed as the syntactic category of a geometric theory.

Shouldn't every geometric category $\mathcal C$ be the syntactic category of some geometric theory (such as the "internal language" of $\mathcal C$)? (I haven't thought about any details though.)

Indeed, but my point is that we have relatively few ways of constructing geometric categories. So even if you're interested in geometric categories, most of the examples of such that you will have access to will either be toposes or the syntactic categories of geometric theories, and from experience I can tell you that the latter are very hard to construct explicit models in unless you have an alternative presentation of them.

Mike Shulman (Sep 05 2021 at 14:23):

Leopold Schlicht said:

You talk about semantic morphisms between theories. Can these be formulated syntactically ("has to send sorts of one theory to, essentially, subobjects of products of sorts of the other" sounds quite syntactic!)?

I've also always wondered: can Morita equivalence of geometric theories be characterized syntactically using a notion of syntactic translation between theories?

Yes, these are both certainly possible, but the semantic approach is so much easier that it's not common to write it out syntactically.

Leopold Schlicht (Sep 07 2021 at 17:54):

Thanks!
A topos has power objects. For what does one need them when interpreting geometric-with-quotients theories? Probably for the quotients, but I don't have the knowledge to check that immediately myself. Anyway, it still feels like a topos has too much structure to correspond to geometric (or geometric-with-quotients) theories.

Jon Sterling (Sep 07 2021 at 18:02):

The existence of power objects is more a miraculous consequence of the exactness and presentability of topoi... But both of these are intertwined with geometric theories.

However, power objects are not part of the structure of a topos qua classifying-topos-of-a-geometric-theory, i.e. they are not preserved by restriction along geometric morphisms.

Leopold Schlicht (Sep 07 2021 at 18:08):

Jonathan Sterling said:

However, power objects are not part of the structure of a topos qua classifying-topos-of-a-geometric-theory, i.e. they are not preserved by restriction along geometric morphisms.

Yes, but then, why is it natural to demand their existence when studying geometric theories?

Jon Sterling (Sep 07 2021 at 18:11):

I don't think I understand what you mean by "demand their existence"...

Jon Sterling (Sep 07 2021 at 18:15):

It is exactly the same scenario as the following fact about posets: "If a poset has infinite joins, then it has infinite meets". If we start studying posets with infinite joins, we never "demanded the existence of" infinite meets but they are there whether we like it or not. With that said, we can tell the difference between structure we "demand to exist" and structure that just arises emergently by looking at what is preserved by morphisms.

Mike Shulman (Sep 07 2021 at 18:58):

Perhaps also worth noting is that the miracle Jon mentions depends on the existence of power objects in Set. If you work in a predicative foundation where power objects don't exist in Set, then neither do they exist in "Grothendieck toposes", by which I mean categories of sheaves on sites, or equivalently the categorical semantics of geometric-with-quotients theories. So from the perspective of geometric (-with-quotients) logic, the existence of power objects is sort of accidental and irrelevant.

Leopold Schlicht (Sep 08 2021 at 19:06):

Jonathan Sterling said:

It is exactly the same scenario as the following fact about posets: "If a poset has infinite joins, then it has infinite meets". If we start studying posets with infinite joins, we never "demanded the existence of" infinite meets but they are there whether we like it or not. With that said, we can tell the difference between structure we "demand to exist" and structure that just arises emergently by looking at what is preserved by morphisms.

That's illuminating, thanks!
Mike Shulman said:

Leopold Schlicht said:

You talk about semantic morphisms between theories. Can these be formulated syntactically ("has to send sorts of one theory to, essentially, subobjects of products of sorts of the other" sounds quite syntactic!)?

I've also always wondered: can Morita equivalence of geometric theories be characterized syntactically using a notion of syntactic translation between theories?

Yes, these are both certainly possible, but the semantic approach is so much easier that it's not common to write it out syntactically.

And with these syntactic translations (with respect to quotients!) the category of Grothendieck toposes is equivalent to the category of geometric theories? (I hope that that's the last question of that kind, so that I am not too annoying, but I think these questions are quite essential to get the big picture.)

Mike Shulman (Sep 08 2021 at 19:18):

It should be. I don't know if the details are written out anywhere.

Leopold Schlicht (Sep 08 2021 at 19:49):

Thanks!

Leopold Schlicht (Sep 14 2021 at 18:17):

Is there a completion 2-functor from coherent categories to pretoposes, similar to the "enrichment of structure" from geometric categories to Grothendieck toposes (exact completion)? As Zhen Lin Low pointed out in another thread, each pretopos is a coherent site, and hence yields a coherent topos. Does the composition "coherent category $\to$ pretopos $\to$ coherent topos" agree with the exact completion of a coherent category considered as a geometric category?

Mike Shulman (Sep 14 2021 at 18:21):

Yes: https://ncatlab.org/nlab/show/pretopos+completion

Mike Shulman (Sep 14 2021 at 18:22):

But "the exact completion of a coherent category considered as a geometric category" doesn't make sense, since a coherent category is not necessarily a geometric category.

Mike Shulman (Sep 14 2021 at 18:23):

By the way, I don't think the relevant operation on geometric categories is literally "exact completion" in the classical sense of "the exact completion of a regular category" that just adds quotients -- just as to get from a coherent category to a pretopos one has to add finite coproducts as well as quotients, to get from a (small) geometric category to a Grothendieck topos one has to add infinite coproducts as well as quotients.

Mike Shulman (Sep 14 2021 at 18:24):

What is true is that if you start with a syntactic coherent theory, you can regard it trivially as a syntactic geometric theory that just doesn't happen to use any of the infinitary aspects of geometric logic. Then the classifying toposes of these two theories coincide. (This distinction is one of the reasons I am generally against conflating syntactic and semantic "theories".)

Leopold Schlicht (Sep 14 2021 at 18:29):

Mike Shulman said:

But "the exact completion of a coherent category considered as a geometric category" doesn't make sense, since a coherent category is not necessarily a geometric category.

Oh sorry, I mean: Does the "coherent category $\to$ pretopos $\to$ coherent topos" completion of a geometric category considered as a coherent category agree with the "exact" completion of a geometric category into a Grothendieck topos?

Mike Shulman (Sep 14 2021 at 18:33):

Ah, there the answer is no. If you forget the geometric-ness of a geometric category, then add it back in again freely, you get something different.

Leopold Schlicht (Sep 14 2021 at 18:56):

This would also mean that each Grothendieck topos is coherent. So sorry again, I think what I was really trying to ask was whether the composition "coherent category $\to$ pretopos $\to$ coherent topos" agrees with the "exact" completion of a coherent category completed into a geometric category (if there is a notion of completing a coherent category into a geometric category).

Mike Shulman (Sep 14 2021 at 18:59):

In that case the answer is yes. You can compose the universal properties to show that they have the same one (both represent coherent functors from a coherent category to toposes), hence are equivalent.

Leopold Schlicht (Sep 14 2021 at 19:20):

I don't know what you mean by "compose the universal properties", because there's an implicit forgetful 2-functor from coherent toposes to Grothendieck toposes at the end of one of the 2-functors we are comparing. If all functors involved were free functors then I could guess what you mean and I would agree.

Mike Shulman (Sep 14 2021 at 19:42):

I mean both constructions are a left (bi-)adjoint to the forgetful functor from Grothendieck toposes (and inverse image functors) to coherent categories.

Leopold Schlicht (Sep 14 2021 at 19:57):

The 2-functor "coherent category $\to$ geometric category $\to$ Grothendieck topos" surely is. But how do you know that "coherent category $\to$ pretopos $\to$ coherent topos $\to$ Grothendieck topos" is?

Mike Shulman (Sep 14 2021 at 20:59):

The coherent topos of a pretopos is the category of sheaves for its coherent topology, hence is the classifying topos for finitely continuous functors that preserve finite covering families. But that's the same as coherent functors.

Leopold Schlicht (Sep 14 2021 at 21:05):

Thanks!

Leopold Schlicht (Sep 15 2021 at 14:43):

Is the "topos of sheaves of a pretopos equipped with the coherent topology" construction the left adjoint of the forgetful functor "coherent topos $\to$ pretopos"?

Mike Shulman (Sep 15 2021 at 19:15):

What are the morphisms in your category of coherent toposes?

Mike Shulman (Sep 15 2021 at 19:19):

It's a left adjoint (modulo size issues) of the forgetful functor from Grothendieck toposes to pretoposes, and it is coherent. So the answer is yes if your category of coherent toposes is a full subcategory of Grothendieck toposes (and inverse image functors).

Leopold Schlicht (Sep 19 2021 at 12:45):

Ah, thanks!

Leopold Schlicht (Jan 18 2022 at 15:30):

Mike Shulman said:

One possible answer is that maybe we aren't actually interested in geometric theories as usually formulated, but rather in "geometric-with-quotients" theories. Any syntactic geometric theory can trivially be regarded as a geometric-with-quotients theory that doesn't use the quotients, just as an algebraic theory can trivially be regarded as a theory in $\lambda$-calculus that doesn't use the function-types, and its syntactic category qua geometric-with-quotients theory will be the exact completion of its syntactic category qua geometric theory.

Actually, what is a geometric-with-quotients theory? Probably a geometric theory, where we allow the formation of quotient types. But what is a quotient type, has this been defined somewhere in the literature?

I had the following idea: whenever $X$ is a type and $\phi(x,y)$ a formula in the context $x\colon X, y\colon X$, then there should be a type $X/\phi$. (Then "types" and "formulas" are defined at the same time using mutual induction, which I don't really like.)

Intuitively, this should be interpreted as the quotient of $X$ by the equivalence relation generated by $\{(x,y)\in X\times X\mid\phi(x,y)\}$. Formally, here is an idea how to interpret this in any topos, but I am not quite sure if it works: There is a Galois connection between equivalence relations and epimorphisms, whose fixed points (on either side) are called "effective". In a topos all equivalence relations and all epimorphisms are effective, hence there's a perfect one-to-one correspondence between epimorphisms and equivalence relations. Now take the equivalence relation generated by the subobject $\{(x,y)\in X\times X\mid\phi(x,y)\}$ (which exists because in a topos the subobject posets have arbitrary infima, right?) and consider the codomain of the corresponding epimorphism.

However, in another thread you talk about quotients in a pretopos. But then the subobject posets don't necessarily have arbitrary infima, so how do we interpret quotient types?

The syntactic category of a theory has as objects all expressions ("subsets") of the form $\{x\in A\mid \phi(x)\}$ for each type $A$. You remark that the exact completion of the geometric syntactic category is equivalent to the geometric-with-quotients syntactic category. But note that these are quite different constructions:

1. When considering the exact completion of the geometric syntactic category, we start with objects of the form $\{x\in A\mid \phi(x)\}$, and then we complete them under quotients.
2. When considering the geometric-with-quotients syntactic category, we start with a collection of types closed under "quotient" types, and then we consider subsets $\{x\in A\mid \phi(x)\}$ of these.

Is there an intuitive reason why they are the same?

And are they in turn equivalent to allowing the formation of "subset types" $\{x\in A\mid \phi(x)\}$ offhand?

This is an instance of a very general notion of "change of doctrine" or "enrichment of structure".

Where can I read about that? (But the questions above are more important.)

Mike Shulman (Jan 18 2022 at 17:09):

In this context, "quotient" means "quotient by an equivalence relation". Quotient types in first-order logic are discussed in Jacobs' book Categorical logic and type theory, among other places. Quotient types in dependent type theory can be found in the HoTT Book, among other places.

Mike Shulman (Jan 18 2022 at 17:09):

In finitary first-order logic or in an arbitrary pretopos it's not possible to generate an equivalence relation from an arbitrary relation, but it can be done as soon as you have countable coproducts or unions, as in particular is the case in geometric logic: construct the reflexive-transitive-symmetric closure as a union of all finitary powers of the relation and its opposite.

Mike Shulman (Jan 18 2022 at 17:10):

As for why the two constructions are the same, one reason is that they have the same universal property. If you want something more concrete, intuitively any subset of a quotient is also a quotient of a subset and vice versa (see [[subquotient]]).

Mike Shulman (Jan 18 2022 at 17:12):

I don't know of a very general reference for "change of doctrine". You can get some sense of it from reading about cartesian / regular / coherent / geometric theories in the Elephant. I wrote a bit about it in a different context here.

Peiyuan Zhu (Jan 18 2022 at 19:07):

Is there a way I can see why this is true? (from http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/classifying+topos#ForLinearOrders) image.png

Peiyuan Zhu (Jan 18 2022 at 19:08):

That the classifying toposes of linear intervals are simplicial sets

Peter Arndt (Jan 18 2022 at 23:11):

That is the content of Section VIII.8 of MacLane/Moerdijk, Sheaves in Geometry and Logic.

Morgan Rogers (he/him) (Jan 19 2022 at 08:15):

While Mac Lane and Moerdijk are quite thorough in exploring this example, I feel that they fail to highlight the aspects of the arguments which work for classifying toposes more generally. In particular, the mechanism by which the theory of total orders is found is mysterious.

Leopold Schlicht (Jan 19 2022 at 13:55):

Mike Shulman said:

In this context, "quotient" means "quotient by an equivalence relation". Quotient types in first-order logic are discussed in Jacobs' book Categorical logic and type theory, among other places.

Thanks! What are the other places? In particular, is there a text explaining quotient types in first-order logic (not dependent type theory) without using the word "fibration"? (Skimming through Jacobs' book I have the feeling I am lacking the necessary background on "fibrations", but I don't want to read chapter 1, because that seems to be a lot of work.)

In finitary first-order logic or in an arbitrary pretopos it's not possible to generate an equivalence relation from an arbitrary relation, but it can be done as soon as you have countable coproducts or unions

But then, how do you interpret quotients in an arbitary pretopos (here you talk about quotients in the logic of a pretopos)? Is it better to have, say, a Boolean pretopos for talking about quotients?

As for why the two constructions are the same, one reason is that they have the same universal property. If you want something more concrete, intuitively any subset of a quotient is also a quotient of a subset and vice versa (see [[subquotient]]).

Thanks!

Zhen Lin Low (Jan 19 2022 at 14:46):

Pretoposes have effective quotients of _equivalence relations_. If you already have an equivalence relation it is not necessary to take the equivalence-relation-closure, so nothing infinite is needed.

Mike Shulman (Jan 19 2022 at 15:42):

Right, that's why I said

In this context, "quotient" means "quotient by an equivalence relation".

Mike Shulman (Jan 19 2022 at 15:43):

Since the semantics of first-order logic intrinsically involves fibrations, or equivalent things such as indexed categories / hyperdoctrines, I doubt you'll find a semantic discussion of quotients in first-order logic that doesn't use these words.

Mike Shulman (Jan 19 2022 at 15:45):

I don't know if anyone has written down the syntax without any reference to semantics, since it's a very semantically motivated notion. But you could try to read Jacobs and just ignore the semantic parts.

Leopold Schlicht (Jan 19 2022 at 16:06):

Zhen Lin Low said:

Pretoposes have effective quotients of _equivalence relations_. If you already have an equivalence relation it is not necessary to take the equivalence-relation-closure, so nothing infinite is needed.

Alright. But how would you define quotients syntactically in the doctrine corresponding to pretoposes? My approach (which is essentially Jacobs', see page 283) in the context of toposes was to add a type $X/R$ for each type $X$ and each formula $R(x,y)$ in the context $x\colon X, y\colon X$. How would you interpret that in an arbitrary pretopos?

Requiring $R$ to be "provably a equivalence relation" isn't elegant from a syntactic point of view, because then the set of types doesn't depend on the signature (consisting of basic types, function symbols, relation symbols, and so on) alone but really on the theory (which determines which formulas are provable). (And this is weird because a theory should be formulated in a fixed signature.)

Mike Shulman (Jan 19 2022 at 17:01):

No, it's not elegant, but it's unavoidable. Isn't that what Jacobs does?

Leopold Schlicht (Jan 19 2022 at 17:44):

Jacobs writes on page 283:

Thus, given a type $\sigma$ with a (binary) relation $R$ on $\sigma$, we can form the quotient type $\sigma/R$. Notice that we do not require that $R$ is an equivalence relation.

Mike Shulman (Jan 19 2022 at 17:46):

Ah, okay, I didn't remember that. But he does consider rules that do require R to be an equivalence relation, like "effective quotients" on p284, so you could just add that condition to the formation rule too.

Leopold Schlicht (Jan 19 2022 at 17:52):

But how do you define "theory" then? Usually a theory consists of a signature $L$ and a set of $L$-sentences. If the set of sentences depends on which sentences are provable, this is a bit circular, isn't it?

Mike Shulman (Jan 19 2022 at 18:09):

Dependent type theory has the same problem. You give a well-ordered list of "generators" which could be base types, atomic formulas, or axioms, each of which is well-typed in the theory generated by the previous generators.

Leopold Schlicht (Jan 20 2022 at 11:46):

This idea is fascinating, thanks!

Leopold Schlicht (Feb 05 2022 at 18:17):

Does that imply that one can stop at the second stage in the sense that we can define a theory to be a 4-tuple $(L_1, T_1, L_2, T_2)$, where $L_1$ is a usual signature, $T_1$ is a usual theory in the signature $L_1$, $L_2$ is the union of $L_1$ and the set of all quotients of types in $L_1$ by $T_1$-provable equivalence relations, and $T_2$ is a theory in the signature $L_2$?

Leopold Schlicht (Feb 05 2022 at 18:19):

Also, why should the list be well-ordered, why wouldn't linearly ordered suffice?

Mike Shulman (Feb 06 2022 at 17:40):

Probably you can stop at the second stage if your only goal is to present all pretoposes. But in practice one may be interested in more general theories, even if they are Morita-equivalent to some two-stage one.

Mike Shulman (Feb 06 2022 at 17:40):

I think well-ordering is necessary in order for the definitions of signature and theory to be non-circular.

Leopold Schlicht (Feb 07 2022 at 12:51):

Thanks!

When my only goal is to present all pretoposes I can just as well stop at the first stage, too! :P

The goal I had in mind was rather different: Given a usual first-order theory $T$, how can we define the "syntactic pretopos of $T$" without any "pretopos completion" construction?

If we identify $T$ with the induced theory (in the above sense) $(L_1, T, L_2, \emptyset)$, then this makes sure that there are enough types to make the syntactic category a pretopos (and not a coherent/logical theory).

Leopold Schlicht (Feb 07 2022 at 12:57):

Mike Shulman said:

I think well-ordering is necessary in order for the definitions of signature and theory to be non-circular.

For that requiring well-foundedness might be enough. Are there any reasons one wants to require the ordering to be total as well?

Also, can you give a reference that uses the "well-ordered list of generators" definition of theories? I'm not familiar with the dependent type theory literature except the HoTT book, so that I never stumbled across that approach.

Leopold Schlicht (Feb 07 2022 at 13:03):

Does the "well-ordered list of generators" approach have the disadvantage to yield to problems when one works in an intuitionistic meta theory? Even if one considers an ordinary (stage 1) theory $T$, then there might be no way to well-order the signature of $T$, so that one cannot convert it into a well-ordered-list-of-generators-theory!

Mike Shulman (Feb 07 2022 at 16:03):

Yes, well-foundedness should be enough, and in an intuitionistic metatheory one should probably do it that way (which would solve your last question too, since any collection of generators with no dependency could be given a flat well-founded relation). However, in practice the distinction is fairly academic since most real-world theories are finite.

Mike Shulman (Feb 07 2022 at 16:05):

One reference that uses a well-founded partial ordering is the definition of cartesian theories in Sketches of an Elephant, D1.3.4(b).

Leopold Schlicht (Feb 07 2022 at 16:27):

Thanks! Is this concept of a well-founded-list-of-generators-theory often used in the dependent type theory and HoTT literature (or only implicitly)? This is something I would expect to find in the Appendix "Formal type theory" of the HoTT book, but I can't.

Mike Shulman (Feb 07 2022 at 18:27):

Since dependent type theory is powerful enough by itself to be a foundation for all of mathematics, it's not as common to consider "theories" in it specified by generators and axioms as it is for weaker doctrines like first-order logic. Moreover, even when people do talk about theories, it's more common to use the "fully embodied" sort rather than presenting them in terms of generators. I can't think offhand of a reference that does it.

Nathanael Arkor (Feb 07 2022 at 21:48):

it's not as common to consider "theories" in it specified by generators and axioms as it is for weaker doctrines like first-order logic

I haven't been following along, but logical frameworks are relatively common in computer science, and are essentially based on this principle for dependent type theories, if I understand your point correctly.

Mike Shulman (Feb 07 2022 at 22:13):

Yes, that's true, thank you. Can you think of a reference that explicitly defines a "theory in a logical framework" in this style, syntactically, with well-founded list of generators/axioms?

Leopold Schlicht (Feb 08 2022 at 12:30):

Thanks!

What do you mean by the "fully embodied" sort, Mike?

I guess one needs to define HoTT theories in order to talk about the "internal language of an elementary $(\infty,1)$-topos" (and to prove that this construction induces an "equivalence" between elementary $(\infty,1)$-toposes and HoTT theories, eventually).

Nathanael Arkor (Feb 08 2022 at 13:47):

Mike Shulman said:

Yes, that's true, thank you. Can you think of a reference that explicitly defines a "theory in a logical framework" in this style, syntactically, with well-founded list of generators/axioms?

Though it's not entirely explicit, both Harper–Honsell–Plotkin's A Framework for Defining Logics and Harper's An equational formulation of LF essentially do this. More explicitly (though not presented as a logical framework), Cartmell's thesis is also essentially based on this idea.

Mike Shulman (Feb 08 2022 at 18:24):

By "embodied" I meant a definition along the lines of "an algebraic theory is a finite-product category" rather than "an algebraic theory consists of a set of base types, a set of generating function symbols, etc.".

Leopold Schlicht (Feb 09 2022 at 12:11):

I see!

Leopold Schlicht (Feb 11 2022 at 14:14):

Mike Shulman said:

Any syntactic geometric theory can trivially be regarded as a geometric-with-quotients theory that doesn't use the quotients, just as an algebraic theory can trivially be regarded as a theory in $\lambda$-calculus that doesn't use the function-types [...] This is an instance of a very general notion of "change of doctrine" or "enrichment of structure".

What if we consider the syntactic category of a $\lambda$-theory (which is a cartesian closed category) as a category with finite products. Which algebraic theory does that category correspond to? Is that related to Morleyization?

Jon Sterling (Feb 11 2022 at 15:05):

Mike Shulman said:

Yes, that's true, thank you. Can you think of a reference that explicitly defines a "theory in a logical framework" in this style, syntactically, with well-founded list of generators/axioms?

The thesis of John Cartmell is the first example of what you are describing; and the thesis of Taichi Uemura would be a more modern example, right?

Mike Shulman (Feb 11 2022 at 17:01):

Leopold Schlicht said:

What if we consider the syntactic category of a $\lambda$-theory (which is a cartesian closed category) as a category with finite products. Which algebraic theory does that category correspond to? Is that related to Morleyization?

I don't think it has a clever description.

Mike Shulman (Feb 11 2022 at 17:02):

Jonathan Sterling said:

The thesis of John Cartmell is the first example of what you are describing; and the thesis of Taichi Uemura would be a more modern example, right?

Thanks. Does Uemura do it syntactically as well as semantically?

Leopold Schlicht (Feb 11 2022 at 17:49):

Thanks! Is Morleyization the same as considering the syntactic category of a first-order theory, which is a Heyting category, as a coherent category?

Mike Shulman (Feb 11 2022 at 18:43):

I don't think so.