Interesting Hyperdoctrines Beyond Classical Models

categorical-logiclo.logic

Short version: what are some interesting hyperdoctrines for classical (not intuitionistic) first-order logic, that are not models in the traditional sense? (Where the terminal and initial hyperdoctrines are "uninteresting".)

Long version:

The categorical semantics of first-order logic are given by hyperdoctrines. This is in contrast with the traditional semantics in terms of model theory.

In brief, in the traditional picture, we think of the semantics of a first-order theory as being some set $U$ ("the universe") plus an interpretation of every constant symbol / function symbol / predicate symbol in that universe (so, eg, for the unary function symbol $f$, the model provides $[\![f]\!] : U \to U$, and so on and so forth.) We can then interpret every proposition in the theory, interpreting (for example) $f x = x$ as the subset of $U$ where $[\![f]\!]$ is fixed.

By contrast, in the categorical style, we think of the semantics of a first-order theory T as being a hyperdoctrine plus some interpretations for the symbols and etc, which I'll call a "hyperdoctrine for T". This is more-or-less a stream of lattices, equipped with some strucures relating the lattices to one another, plus interpretations for the various symbols in terms of the lattices. Roughly speaking, the nth lattice is thought of as the possible interpretations of a proposition with n variables free, and the structures relating the lattices are about substitution and quantification.

The latter framework is more general. For instance, we can turn a traditional model for a theory T into a hyperdoctrine for T by letting the nth lattice be the lattice of all subsets of $U^n$. But we also have new hyperdoctrines: most notably a terminal one, corresponding to the choice where every lattice in the stream is the trivial (one-object) lattice; and the initial one, corresponding to the syntax.

And presumably, the categorical semantics also add a whole host of more interesting "new models". Like, presumably there are hyperdoctrines (for, say, 1st order arithmetic) that assert some combination of sentences, that no traditional model asserts. (Such combinations must necessarily be infinite, on account of the traditional completeness theorem, but still. (ETA: Not quite; see the comments below.)) And, like, yes, the terminal and initial hyperdoctrines show us some boring ways that this is true, but surely this newfound generality does more than just bolt a new "initial" and "terminal" model onto the traditional models. So, what are some of these new models?

(Ideally in the classical setting; I know we can get topological models and stuff if we consider intuitionistic logic, but it still seems to me that even classically we must have additional interesting hyperdoctrines, and I'd like to know what they are.)

(Ideally I'm looking for hyperdoctrines that feel motivated in their own right, more like "the lattices contain only the propositions that satisfy the following natural property" than "well given any hyperdoctrine we can generate a new one by bolting on a spandrel; just do that to the initial model". My apologies for the vagueness of this constraint. What I'm really after here are intuitions about how hyperdoctrines expand the space of models.)

(If I'm wrong in my assumption that there are interesting hyperdoctrines aside from the initial and terminal one, I'd also be happy to hear about that.)

Best Answer

Maybe I am wrong, but it seems to me that the other answers are misunderstanding the question. The emphasis on syntactic hyperdoctrines seems to me beside the point.

A (classical, first-order) hyperdoctrine is a categorical (semantic) structure, consisting of a category $C$ and a functor $P: C \to \rm BoolAlg$ together with adjoints and a Beck-Chevalley condition. It seems to me that the OP wants to consider a particular construction of such a hyperdoctrine as follows: given a set $U$, let $C$ be the full subcategory of $\rm Set$ determined by the objects $U^n$, and let $P(U^n)$ be the powerset of $U^n$. Let's call this hyperdoctrine ${\rm Set}|_U$.

For a particular theory $T$ (which, in general, should be multi-sorted) and hyperdoctrine $C$, one can then consider the notion of a "model of $T$ in $C$". This consists of an interpretation function assigning an object of $C$ to each sort of $T$, a morphism of $C$ to each function symbol of $T$, and a predicate in some $P(X)$ to each relation symbol of $T$, such that the axioms of $T$ are "satisfied". I think this is what the OP means by a "hyperdoctrine for $T$". One can rephrase this in a more highbrow way by building a "syntactic hyperdoctrine" $S_T$ out of $T$ and saying that a model of $T$ in $C$ is a morphism of hyperdoctrines $S_T \to C$, but that isn't necessary.

It seems to me that the OP is asking whether there are any interesting models of $T$ in hyperdoctrines $C$ not of the form ${\rm Set}|_U$ (and also where $C$ is not terminal and not the initial $T$-hyperdoctrine $S_T$).

There are some fairly trivial answers to that question. One, which I think appears in the other answers, is that for any theory $T'$ extending $T$, there is a canonical model of $T$ in $S_{T'}$. Another is that instead of models in ${\rm Set}|_U$, we can consider models in $\rm Set$ itself; if $T$ has only one (base) sort then any such model factors uniquely through some ${\rm Set}|_U$, so it is not very different (but if $T$ has more than one sort, then this more general kind of model is the "correct" one to think about).

However, I think the most satisfying answer is that

You can replace $\rm Set$ by any (Boolean) category.

In other words, given any category $C$, you can define a hyperdoctrine over $C$ where $P(X)$ is the poset of subobjects of $X\in C$. If $C$ is a Boolean category, this will be a classical first-order hyperdoctrine, call it ${\rm Sub}(C)$. Then you can consider models of any theory $T$ in ${\rm Sub}(C)$, and they will be new, different, and interesting, and can satisfy principles that don't hold in $\rm Set$.

You get many more interesting models if you generalize to intuitionistic logic, in which case you use Heyting categories instead of Boolean categories and every elementary topos is an example. This leads to the whole field of topos theory and the categorical semantics of internal languages. But there are also interesting Boolean categories other than $\rm Set$, such as ${\rm Set}^X$ for any set $X$, or even for any groupoid $X$.

Related Question