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: conceptual completeness

Leopold Schlicht (Aug 28 2021 at 21:08):

In topos theory there are at least two results that are called "completeness theorems":

1. Deligne's completeness theorem: Every coherent topos has enough points.
2. Makkai's conceptual completeness theorem: The 2-functor from the 2-category of pretoposes to the 2-category of ultracategories that sends a pretopos $\mathcal C$ to the ultracategory $\mathrm{Mod}(\mathcal C)$ of pretopos morphisms from $\mathcal C$ to $\mathbf{Set}$ is fully faithful.

There's a very enlightening post on MathOverflow explaining why 1. is called a "completeness" theorem: https://mathoverflow.net/a/68342.

But in which sense is 2. a "completeness" theorem? Does it imply Gödel's completeness theorem too? (Informally speaking, the theorem states that a first-order theory $\mathbb T$ can be recovered from the category $\mathrm{Mod}(\mathbb T)$ of its models, but it seems to me that this doesn't imply that every consistent theory has a model.)

Zhen Lin Low (Aug 29 2021 at 04:50):

If a theory has no models then its category of models is empty. But you can reconstruct the theory from the category of models, so the theory must have been inconsistent to begin with. What's the problem?

Leopold Schlicht (Aug 29 2021 at 11:59):

Thanks. So if the syntactic pretopos of $\mathbb T$ is equivalent to the syntactic pretopos of $\{\bot\}$, this implies that $\mathbb T$ is inconsistent? In general, what does it mean for two first-order theories $\mathbb T$ and $\mathbb S$ to have equivalent syntactic pretoposes? Does it mean that $\mathbb T$ and $\mathbb S$ are "bi-translatable" in the sense that there are two "translations" $\mathbb T\to\mathbb S$ and $\mathbb S\to\mathbb T$ that are inverse to each other, for some suitable notion of "translation". Is there an established definition of a "translation" between first-order theories, (if yes) where can I find it, and has it something to do with the notion of bi-interpretability from model theory?
Can one prove something like that the category of pretoposes is equivalent to the category of first-order theories with translations? (The above suggests that at least there's a fully faithful embedding of first-order theories into pretoposes.)

Also, what was Deligne's motivation for proving a completeness theorem in algebraic geometry?

Zhen Lin Low (Aug 29 2021 at 12:30):

A consistent theory will have in its syntactic pretopos non-isomorphic initial and terminal objects, whereas the syntactic pretopos of an inconsistent theory is trivial. I do not think it is appropriate to use morphisms of syntactic pretoposes as the morphisms of a category of general first-order theories. Maybe it is appropriate for coherent theories.

Zhen Lin Low (Aug 29 2021 at 12:32):

As for Deligne, having enough points makes it a lot easier to transfer results from classical mathematics. I feel it is in the same vein as, say, the Freyd–Mitchell embedding theorem for abelian categories.

Fawzi Hreiki (Aug 29 2021 at 12:40):

Well, and also many toposes of sheaves in algebraic geometry are coherent.

Fawzi Hreiki (Aug 29 2021 at 12:41):

It’s always nice to know when a space has enough points (in the vein of the Nullstellensatz)

Spencer Breiner (Aug 29 2021 at 13:25):

Zhen Lin Low said:

I do not think it is appropriate to use morphisms of syntactic pretoposes as the morphisms of a category of general first-order theories. Maybe it is appropriate for coherent theories.

More appropriate under a Boolean assumption, since in that case $\neg,\Rightarrow,\forall$ are definable from the pretopos structure.

Leopold Schlicht (Aug 31 2021 at 21:25):

Thanks!

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

Zhen Lin Low said:

I do not think it is appropriate to use morphisms of syntactic pretoposes as the morphisms of a category of general first-order theories.

Why?

As for Deligne, having enough points makes it a lot easier to transfer results from classical mathematics. I feel it is in the same vein as, say, the Freyd–Mitchell embedding theorem for abelian categories.

When you are talking about "transfering results from classical mathematics", what do you mean? (The internal language of toposes comes to mind, but I doubt Deligne has used it, so I don't know what you mean.) Also, why is it similar to the Freyd–Mitchell embedding theorem?

Zhen Lin Low (Sep 05 2021 at 14:13):

Geometric morphisms are designed/defined to preserve finitary conjunctions and infinitary disjunctions, but first order logic has other connectives!

Zhen Lin Low (Sep 05 2021 at 14:20):

Regarding transferring results from classical mathematics, it is not necessary to understand or use logic. That's in some sense a great advantage of the category theoretic approach because it is unnecessary to appeal to formal proofs or syntactic objects etc.; you can just treat classical results as black boxes. The Freyd–Mitchell embedding theorem can be considered a way of transferring certain simple results about modules to general abelian categories – specifically, anything you can construct or prove that is preserved by exact additive functors can be transferred. In the same way Deligne's theorem tells you that anything you can construct or prove that is preserved by the inverse image functor of a geometric morphism can be transferred from Set to a coherent topos.

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

Zhen Lin Low said:

Geometric morphisms are designed/defined to preserve finitary conjunctions and infinitary disjunctions, but first order logic has other connectives!

I think pretopos morphisms also preserve effective epimorphisms, if that changes anything.

But this sounds like pretoposes and pretopos morphisms are not the right categorical setting for first-order logic. I still don't understand the relationship between pretoposes and first-order logic.

Zhen Lin Low said:

Regarding transferring results from classical mathematics, it is not necessary to understand or use logic. That's in some sense a great advantage of the category theoretic approach because it is unnecessary to appeal to formal proofs or syntactic objects etc.; you can just treat classical results as black boxes.

What do you mean by "transferring results from classical mathematics"? Do you mean the internal language of toposes? I doubt it existed at the time Deligne was proving his theorem.

The Freyd–Mitchell embedding theorem can be considered a way of transferring certain simple results about modules to general abelian categories – specifically, anything you can construct or prove that is preserved by exact additive functors can be transferred. In the same way Deligne's theorem tells you that anything you can construct or prove that is preserved by the inverse image functor of a geometric morphism can be transferred from Set to a coherent topos.

I don't understand that analogy. The Freyd–Mitchell embedding theorem states something like "each abelian category is a subcategory of some category of modules". Deligne's theorem isn't of the form "each (coherent) topos can be embedded into some concrete topos", or is it?

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

Yes, pretoposes are at least "a" right setting for coherent logic, but not really for full first-order logic. Heyting pretoposes would be.

Jens Hemelaer (Sep 07 2021 at 19:40):

Leopold Schlicht said:

I don't understand that analogy. The Freyd–Mitchell embedding theorem states something like "each abelian category is a subcategory of some category of modules". Deligne's theorem isn't of the form "each (coherent) topos can be embedded into some concrete topos", or is it?

I think that the following holds:
a Grothendieck topos $\mathcal{E}$ has enough points if and only if there is a functor $F : \mathcal{E} \to \mathbf{Sets}$ such that $F$ is faithful and preserves colimits and pullbacks. I believe such a functor $F$ is also called a "bag of points". The idea is that if you have a set $S$ of enough points, then you can construct $F$ by setting $F(X) = \bigsqcup_{p \in S} p^*(X)$. Conversely, if you have such a functor $F$, then for every element $x \in F(1)$ you have a point $p_x$ where $p_x^*(X)$ is the preimage of $x$ along the map $F(X) \to F(1)$... and these points $p_x$ then form a set of enough points for $\mathcal{E}$.

Zhen Lin Low (Sep 07 2021 at 22:16):

Alternatively, a Grothendieck topos $\mathcal{E}$ has enough points if and only if there is a set $S$ and a functor $\mathcal{E} \to \textbf{Set}^S$ that preserves colimits, finite limits, and is conservative. (This is almost literally the definition!) Such a functor is automatically faithful, so it is fair to call it an embedding, but it is not necessarily full.

Zhen Lin Low (Sep 07 2021 at 22:23):

An example of the kind of classical mathematics you can transfer using this embedding: well, you can get quite far in the construction of the homotopy theory of simplicial sheaves this way. In fact Ken Brown does exactly this in his 1973 paper, albeit for sheaves on topological spaces – a class of sites that tautologically has enough points! – rather than sheaves on coherent sites.

Morgan Rogers (he/him) (Sep 08 2021 at 07:29):

Jens Hemelaer said:

Leopold Schlicht said:

I don't understand that analogy. The Freyd–Mitchell embedding theorem states something like "each abelian category is a subcategory of some category of modules". Deligne's theorem isn't of the form "each (coherent) topos can be embedded into some concrete topos", or is it?

I think that the following holds:
a Grothendieck topos $\mathcal{E}$ has enough points if and only if there is a functor $F : \mathcal{E} \to \mathbf{Sets}$ such that...

That should be $\mathbf{Sets}/X$, where $X$ corresponds to a sufficient set of points.

Jens Hemelaer (Sep 08 2021 at 07:58):

Morgan Rogers (he/him) said:

That should be $\mathbf{Sets}/X$, where $X$ corresponds to a sufficient set of points.

I really meant $\mathbf{Sets}$ here, to make the link with concrete categories. Any Grothendieck topos $\mathcal{E}$ is concretizable (there is a faithful functor $F : \mathcal{E} \to \mathbf{Sets}$), but Grothendieck toposes with enough points are concretizable in a special way: you can ask additionally that $F$ preserves colimits and pullbacks.

Morgan Rogers (he/him) (Sep 08 2021 at 07:59):

Ah I should have read more carefully, so you're composing with the dependent sum functor $\mathbf{Sets}/X \to \mathbf{Sets}$!

Jens Hemelaer (Sep 08 2021 at 08:07):

Yes! I think for the cohomological applications that @Zhen Lin Low mentions, the faithful functor to $\mathbf{Sets}/X$ is typically used though, because it is less complicated and you can make sure that all finite limits are preserved and not only pullbacks.

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

Mike Shulman said:

Yes, pretoposes are at least "a" right setting for coherent logic, but not really for full first-order logic. Heyting pretoposes would be.

Thanks! So the category of pretoposes is equivalent to the category of coherent theories?

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

Well, for one possible definition of "the category of coherent theories" at least.

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

I.e. the one that defines a morphism of coherent theories to be a morphism between their corresponding pretoposes, or back-compiles that into some kind of syntactic monster. (-:

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

Thanks!

Leopold Schlicht (Sep 09 2021 at 11:42):

@Jens Hemelaer and @Zhen Lin Low: Ah, I see, thank you so much for your explanations.

Leopold Schlicht (Dec 29 2021 at 13:15):

Zhen Lin Low said:

If a theory has no models then its category of models is empty. But you can reconstruct the theory from the category of models, so the theory must have been inconsistent to begin with. What's the problem?

This only shows that Makkai's theorem implies that there is no consistent theory without set-theoretic models. Completeness is something stronger: if $T\models\varphi$, then $T\vdash \varphi$. In a classical setting "consistent $\Rightarrow$ there is a model" implies completeness: if not $T\vdash \varphi$, then $T\cup\{\neg\varphi\}$ is consistent, since otherwise $T\cup\{\neg\varphi\}\vdash \bot$, hence $T\vdash \neg\neg\varphi$ and thus $T\vdash \varphi$. But in the last step we use double negation elimination -- a rule of inference not available in the logic of pretoposes.

This is the only way I see how to deduce the completeness theorem from Makkai's theorem: if one additionally knows that the construction sending an ultracategory $\mathcal M$ to the pretopos of ultrafunctors $\mathcal M\to \mathbf{Set}$ is right adjoint to $\mathcal C\mapsto \mathrm{Mod}(\mathcal C)$, then one can conclude that the unit $\mathcal C\mapsto \mathrm{Ultrafun(\mathrm{Mod(\mathcal C), \mathbf{Set}})}$ is an equivalence. Unwinding the definitions one probably sees that the fully faithfulness of that functor $\mathcal C\mapsto \mathrm{Ultrafun(\mathrm{Mod(\mathcal C), \mathbf{Set}})}$ is a reformulation of Gödel's completeness theorem.

Is there anything else one can say about the relationship between Deligne's theorem and Makkai's theorem (despite noting that Makkai's theorem implies Gödel's completeness theorem, in the sense discussed above, and that Gödel's completeness theorem in turn implies Deligne's theorem)?

And is there a way to deduce Gödel's completeness theorem from Makkai's theorem as formulated in the first post in this thread (without knowing about the left adjoint of $\mathrm{Mod}$)?

Mike Shulman (Dec 29 2021 at 18:03):

Your original question was about "Godel's completeness theorem" which is a statement about classical logic. Intuitionistic logic does not satisfy a completeness theorem for set-models, only for models in arbitrary categories, which is proven in a very different and more tautological way.