What are some interesting hyperdoctrines that are not classical models?

Question

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.)

Answer 1

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$.

Answer 2

Given any theory $T$, we have a hyperdoctrine $H(T)$ (the "syntactic hyperdoctrine for $T$"), where (in the single sorted case) the $n^{\text{th}}$ lattice is the lattice of formulas in $n$ free variables, up to equivalence modulo $T$.

As Zhen Lin's answer shows, in fact every hyperdoctrine is the syntactic hyperdoctrine for some theory (the "full theory" of the hyperdoctrine).

Now what is a morphism of hyperdoctrines? It's an interpretation of theories. That is, a morphism of hyperdoctrines $H(T)\to H(T')$ gives a translation of formulas relative to $T$ into formulas relative to $T'$, which preserves the logical structure, i.e., an interpretation of $T$ in $T'$. More generally, any morphism of hyperdoctrines $H\to H'$ can be viewed as an interpretation of the full theory of $H$ in the full theory of $H'$.

When we view a traditional model $M$ of $T$ as a hyperdoctrine under $H(T)$, we form the hyperdoctrine $H(M)$ where (in the single sorted case) the $n^{\text{th}}$ lattice is $\mathcal{P}(M^n)$. And we get a morphism of hyperdoctrines $H(T)\to H(M)$ mapping a formulas relative to $T$ to its evaluation in $M$ (the set of tuples in $M$ satisfying the formula). Note that we can also view this as an interpretation of $T$ in the full theory of $M$: This theory has relation symbols for every subset of $M^n$ for all $n$, and the interpretation sends a formula to the relation symbol naming its evaluation in $M$. This is one of the features of categorical logic: it puts the notion of "model of a theory" and "interpretation of theories" on the same footing.

Ok, so addressing your question: if a "hyperdoctrine for $\mathsf{PA}$" is a hyperdoctrine $H$ equipped with a morphism $H(\mathsf{PA})\to H$, then we have initial hyperdoctrine for $\mathsf{PA}$ (which is the syntactic hyperdoctrine $H(\mathsf{PA})$ itself) and all the standard models of $\mathsf{PA}$ in the form $H(M)$. What else? Well, we have a "hyperdoctrine for $\mathsf{PA}$" for every interpretation of $\mathsf{PA}$ into a theory $T$. For example, the standard interpretation of $\mathsf{PA}$ in $\mathsf{ZFC}$ gives a morphism of hyperdoctrines $H(\mathsf{PA})\to H(\mathsf{ZFC})$. And in a precise sense, every hyperdoctrine for $\mathsf{PA}$ has this form, since every morphism of hyperdoctrines can be viewed as an interpretation of theories. The terminal hyperdoctrine for $\mathsf{PA}$ is the interpretation of $\mathsf{PA}$ in the inconsistent theory.

So typical hyperdoctrines for $\mathsf{PA}$ include things like $H(T)$ where $T$ is a stronger theory than $\mathsf{PA}$ (obtained by adding axioms) or $H(T)$ where $T$ is an expansion of $\mathsf{PA}$ to include extra structure. In the comments, you wrote that you were hoping for something like "there's a hyperdoctrine for $\mathsf{PA}$ of only the decidable predicates". This doesn't make sense, since any hyperdoctrine for $\mathsf{PA}$ must interpret all the predicates definable in $\mathsf{PA}$, not just the decidable ones.

I've been intentionally vague about some details here (like what counts as a morphism of hyperdoctrines), hoping that a more high level view will help get your thinking on the right track.

Answer 3

Every hyperdoctrine is "syntactic", in the sense that given any hyperdoctrine you can construct a theory whose syntactic hyperdoctrine is equivalent to the one you start with. Thus, hyperdoctrines correspond not to models (i.e. complete theories) but rather (deductively closed) theories.

Suppose we have a hyperdoctrine, that is, a cartesian monoidal category $\mathcal{S}$ and a contravariant functor $\Omega$ from $\mathcal{S}$ to the category of boolean algebras satisfying certain axioms (corresponding to logical axioms for $\exists$ and $=$). Consider the following (multisorted) theory $T$.

• The sorts are the objects in $\mathcal{S}$.
• For each tuple $(X_1, \ldots, X_n, Y)$ (where $n \ge 0$) of objects in $\mathcal{S}$ and each morphism $X_1 \times \cdots \times X_n \to Y$ in $\mathcal{S}$ we have an $n$-ary function symbol of the same name and type.
• For each tuple $(X_1, \ldots, X_n)$ of objects in $\mathcal{S}$ and each element of $\Omega (X_1 \times \cdots \times X_n)$ we have an $n$-ary relation symbol of the same name and type.
• We introduce as axioms equations encoding projections and composition in $\mathcal{S}$.
• For every morphism $\langle f_1, \ldots, f_n \rangle : X_1 \times \cdots \times X_m \to Y_1 \times \cdots \times Y_n$ in $\mathcal{S}$, every tuple $(R_1, \ldots, R_p)$ of elements in $\Omega (X_1 \times \cdots \times X_m)$, and every $S \in \Omega (Y_1 \times \cdots \times Y_n)$, if $R_1 \wedge \cdots \wedge R_p \le \langle f_1, \ldots, f_n \rangle^* S$ then we introduce the axiom $$R_1 (x_1, \ldots, x_m) \land \cdots \land R_p (x_1, \ldots, x_m) \Rightarrow S (f_1 (x_1, \ldots, x_m), \ldots, f_n (x_1, \ldots, x_m))$$ Similarly, if $\langle f_1, \ldots, f_n \rangle^* S \le R_1 \vee \cdots \vee R_p$ then we introduce the axiom $$S (f_1 (x_1, \ldots, x_m), \ldots, f_n (x_1, \ldots, x_m)) \Rightarrow R_1 (x_1, \ldots, x_m) \lor \cdots \lor R_p (x_1, \ldots, x_m)$$
• For every object $X$ in $\mathcal{S}$, if $R \in \Omega (X \times X)$ is the hyperdoctrinal equality then we introduce the axiom $R (x_1, x_2) \Rightarrow (x_1 = x_2)$.

And so on. I think it is clear that there is a "tautological" morphism from the syntactic hyperdoctrine of $T$ to $(\mathcal{S}, \Omega)$ defined by sending the generators back to the objects/morphisms/elements of the same name, and that this is an equivalence of hyperdoctrines.