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: our papers

Topic: categorical completeness

Hugo Jenkins (Feb 24 2022 at 07:03):

This post concerns my senior thesis ( https://arxiv.org/abs/2111.05998 ). Right now, I am wondering whether I have wasted a colossal amount of time, and I would appreciate any feedback from people knowledgeable in categorical logic on the following points.

What I have done is an explicit deduction of Gödel’s Completeness Theorem “via” categorical logic. By this I mean that I defined the syntactic category of a first-order theory $T$ completely syntactically, letting its objects be formulas of the language, and morphisms be $T$-provable equivalence classes of definable maps; verified the coherent category axioms proof-theoretically; invoked a categorical completeness theorem; and translated the output back to a model in the “classical” sense. The specific theorem invoked assumes a coherent category only, not a pretopos, which I do not have.

While it might seem quite laughable to do this in view of the Henkin proof of completeness, let’s just accept that I did, for some reason. I don’t know exactly why. Part of it was the personal challenge of making everything work out perfectly strictly.

The main source was Lurie’s categorical logic notes, and in particular the remarks on the last page here, which basically served as my outline. Question: does anyone see a point in carrying this out (besides personal satisfaction)? It is obviously “back-compiled”. Is it possible that there is an analogy to something that actually needs to be done in Homotopy Type Theory? Isn’t the construction of syntactic categories something of interest there?

I’m also curious whether there could be a conceptual elucidation of one thing in particular. Most of the definable maps I needed turned out to be instances of “substitution” in the following sense: suppose we’re given first-order formulas $\varphi (x_1, \dots x_n)$ and $\psi(y_1, \dots y_m)$ with the indicated free variables, and we happen to have a map $f:\{y_1, \dots y_m\} \to \{x_1, \dots x_n\}$ between these f.v. sets such that (under $T$) the formula $\varphi$ logically implies $\psi(f(y_j))$ (a substitution). Then we get an associated definable map $\tilde{f}:\phi \to \psi$ in the syntactic category. (See section 3.1 “Special Morphisms“.) Why is this? And why are the projections and inclusions in Syn(T) examples of these morphisms? Is there a notion of what a “variable” is which turns this into a contravariant functor? I have read on StackExchange the statement that “in categorical logic free variables are generalized elements”, but don’t understand what this means.

Thank you for any feedback. All the best,
Hugo

Morgan Rogers (he/him) (Feb 24 2022 at 07:13):

Two things:

First, you should check out Section D1, especially D1.5, of Johnstone's Sketches of an Elephant: A topos theory compendium, where you can find the kind of approach to completeness for first order logic via syntactic categories that you describe.

Second, you should talk to @Joshua Wrigley; he did some work in the first year of his PhD (last year) to show that one can use a site with just the substitution maps you describe as an alternative site for the classifying topos of a theory. He'll be able to give you the insight you're after. Also, he's more logically inclined than me, so you might find his enthusiasm motivating.

Morgan Rogers (he/him) (Feb 24 2022 at 07:43):

From the tone of the Ending Remarks of that thesis, it seems like you were disappointed with the outcome. It's clear that you put a lot of work into it, but at some point you lost sight of why you were bothering?
To me, categorical logic demonstrates that we don't have to use sets as the default semantics of our formal systems. Not only can we interpret them in any category with enough structure, but the syntax provides for us a canonical such category, which even contains a "universal" model of the theory we've built! Building the syntactic category is similar in spirit to Henkin's method of building a model out of the syntax, but the structure of the logic is built into it. I suspect a fragment of that picture was what got you interested in this in the first place :)

Joshua Wrigley (Feb 24 2022 at 13:41):

Hi Hugo, I'll message you later to "impart" some of that enthusiasm Morgan mentioned, but for now I'll direct you to this recording of a talk I gave a while back on precisely on this idea of which arrows in the syntactic category are strictly necessary. As you've noticed, only what you've dubbed "special arrows", those coming from substitutions, are needed to generate the whole classifying topos of a geometric theory. Moreover, one doesn't need to consider provable equivalence classes of special morphisms. Suppose that the theory is single-sorted. What one ends up calculating is an internal locale of the classifying topos of objects [FinSets,Sets], that is the classifying topos of the empty theory with a single sort (cf. Theorem D3.2.5 from the elephant). This is indicative of a wider study in progress of relative topos theory that I'd be very happy to gush over if you have any questions!

Ivan Di Liberti (Feb 24 2022 at 16:15):

D3.2.5 has been widely dicussed recently on MO: https://mathoverflow.net/questions/415688/equivalence-between-geometric-theories-and-frames-internal-to-the-free-topos/

Graham Manuell (Feb 24 2022 at 21:38):

Ivan Di Liberti said:

D3.2.5 has been widely dicussed recently on MO: https://mathoverflow.net/questions/415688/equivalence-between-geometric-theories-and-frames-internal-to-the-free-topos/

I'm also a fan of this result. Joyal gave a nice series of talks on this at the TACL summer school in 2019.

You should maybe point out in your answer that Heyt refers to the category of complete Heyting algebras.

Hugo Jenkins (Feb 25 2022 at 19:42):

Morgan Rogers (he/him) said:

From the tone of the Ending Remarks of that thesis, it seems like you were disappointed with the outcome. It's clear that you put a lot of work into it, but at some point you lost sight of why you were bothering?
To me, categorical logic demonstrates that we don't have to use sets as the default semantics of our formal systems. Not only can we interpret them in any category with enough structure, but the syntax provides for us a canonical such category, which even contains a "universal" model of the theory we've built! Building the syntactic category is similar in spirit to Henkin's method of building a model out of the syntax, but the structure of the logic is built into it. I suspect a fragment of that picture was what got you interested in this in the first place :)

Yes. I guess what is most interesting to me is the idea that from some presented syntactic/combinatorial object (like a theory $T$, or a formal calculus itself), we can produce a category which serves as an “invariant”. This is what I am thinking of the syntactic category, or the universal model, as. But I don’t think I have any meaningful sense yet of what it encodes or how it is could actually be used for distinguishing essentially different objects.

I know that the classifying topos exists, but I don’t believe it can really rely on letting objects be formulas and morphisms be provable equivalence classes of ``functional formulas’’, ect blah blah blah as I have done.

I need to look at these resources. Thanks very much. Re:the “invariant” idea, maybe I should also spend some time looking at Lawvere’s thesis? Isn’t that where it first appeared, for essentially algebraic theories?

Morgan Rogers (he/him) (Feb 28 2022 at 17:30):

I haven't read Lawvere's thesis, and I can't speak with authority on the history of this perspective. But I can talk about classifying toposes a little. The point is that, while they are formally constructed exactly as you have seen with a "syntactic site" constructed from formulas-in-context and equivalence classes of provably functional formulas, we can identify other constructions of equivalent toposes. In other words, we have a topos whose abstract properties are guaranteed by the syntactic construction, but we also have ways to concretely calculate in and on that topos thanks to the other presentations.
There have been some discussions of classifying toposes here indicating that Morita equivalence for geometric theories is a fairly fine equivalence relation, but having access to toposes we can concretely work with can (thanks to modern developments) be much more convenient than arguing directly about syntax.