Is it possible to build a category whose arrows are model-theoretic interpretations in such a way that:
- the presence or absence of parameters is handled in an elegant way.
- the notion of a definable interpretation has a definition that's categorical and doesn't appeal to the concrete implementation of an interpretation.
I think we can define an interpretation in the following way.
This presentation exactly follows the presentation given in Wikipedia, except that I'm baking whether parameters are allowed into my concrete representation of an interpretation.
Let an interpretation $(b, n, i)$ from $A$ to $B$ be a triple consisting of $b$ which is $0$ or $1$, a positive integer $n$, and a binary relation $i \subset A^n \times B$ subject to the following constraints.
- $i$ is right-total. For all $b$, $i^{\leftarrow}(b)$ is not empty.
- $i$ is left-unique. For all $a$, $i^{\rightarrow}(a)$ has cardinality $0$ or $1$.
- If $b$ is $0$, every $0$-definable subset of $A^n$ is $0$-definable in $B$.
- If $b$ is not $0$, every with-parameters-definable subset of $A^n$ is with-parameters-definable in $B$.
There are a couple of small things that I don't really like about this way of talking about what an interpretation is:
- Interpretations with parameters and interpretations without parameters live in separate realms. We can compose them and get a relation that is left-unique and right-total, but it won't necessarily be an interpretation. I think this is because we're controlling whether parameters are allowed at the level of the interpretation, rather than choosing it independently for the source and destination.
- The multiplicity thing seems like it would be handled better by defining a notion of raising a structure to a given power $A^n$ rather than adding additional content that lives alongside the interpretation.
Here's one idea I had for how to do this, which I'll call a quasimodel, which is just the carrier of a model (i.e. a set) equipped with a boolean lattice of definable sets.
Let's define the notation $[A, U, n]$ where $A$ is a first-order structure, $U$ is the set of the parameters of $A$, and $n$ is a positive integer to be the quasimodel $((A'')^n, \Lambda(n))$ where $A''$ is the carrier of $A$ and $\Lambda(n)$ is the lattice of $A$-definable subsets with $n$ free variables.
In this setting, an interpretation $i : [A, U, n] \rightarrow^p [B, V, k]$ where $\rightarrow^p$ denotes a surjective partial function is just a partial function from $A$ to $B$ such that for all $\alpha$ in the lattice of $[A, U, n]$, $i^{\rightarrow}(\alpha)$ is in the lattice of $[B, V, k]$.
So, I think we can reasonably collect our quasimodels into a class of objects and make interpretations the maps between them.
We also have a notion of definability, which I think can be construed as follows:
$i : [A, U, n] \to^p [A, U, k]$ is definable if and only if the graph of the interpretation (an ($1+n+k$)-ary relation) is in $[A, U, 1+n+k]$.
We might be able to open this definition up a little bit and define $i : [A, U, n] \to^p [A, U'', k]$ to be definable when it is in $[A, U \cap U'', 1+n+k]$.
However, I can't figure out how to express this in a way that's more categorical.
Best Answer
I've been meaning to write an answer for some time, expanding on user Dabouliplop's comments.
There is indeed a satisfying categorical treatment of interpretations, coming (unsurprisingly) from categorical logic. This will be a long answer, so I've broken it into sections. I'll first describe a category of interpretations between theories, and then explain how to obtain from this a category of interpretations between structures, as you desire.
For any first-order theory $T$, there is a category $C_T$, called the syntactic category of $T$. Its objects are first-order formulas, up to provable equivalence modulo $T$, and its arrows are definable functions, up to provable equivalence modulo $T$. More formally, if $\varphi(x)$ and $\psi(y)$ are formulas, we first rename the variables as necessary to make sure that $x$ and $y$ are disjoint tuples of variables. Then an arrow $[\varphi(x)]\to [\psi(y)]$ is represented by a formula $\theta(x,y)$ such that $T\models \forall x\, (\varphi(x)\to \exists^! y\, (\psi(y)\land \theta(x,y)))$, and two such formulas $\theta(x,y)$ and $\theta'(x,y)$ represent the same arrow if $T\models \forall x\, \forall y\, ((\varphi(x)\land \psi(y))\rightarrow (\theta(x,y)\leftrightarrow \theta'(x,y)))$.
The syntactic category $C_T$ can be equipped with the structure of a Boolean category. Essentially, this structure corresponds to the logical structure of formulas. For example, subobjects have meets and joins and complements in the subobject lattice (and, or, and not), and pullbacks have left and right adjoints (the quantifiers). Conversely, it turns out that every Boolean category is equivalent to one of the form $C_T$ for some (multi-sorted) first-order theory $T$.
Now if $C$ and $D$ are Boolean categories, then a functor $F\colon C\to D$ is a Boolean functor if it preserves all the structure of Boolean categories. A Boolean functor between syntactic categories, $I\colon C_T\to C_{T'}$ gives a translation from formulas in the language of $T$ to formulas in the language of $T'$, which preserves the logical structure and the truths of $T$. That is, it's an interpretation of $T$ in $T'$.
Well, really it's a definition of $T$ in $T'$, where a definition is a special type of interpretation that doesn't allow quotients by definable equivalence relations. To get to the general notion of interpretation, we have a few options:
On the logical side, we could replace $T$ and $T'$ with their canonical expansions $T^{\mathrm{eq}}$ and $(T')^{\mathrm{eq}}$ which eliminate imaginaries. Now a definition of $T^{\mathrm{eq}}$ in $(T')^{\mathrm{eq}}$ is the same as an interpretation of $T$ in $T'$. The syntactic category $C_{T^{\text{eq}}}$ has the additional structure of a Boolean pretopos, which is a Boolean category admitting "quotients" by internal equivalence relations.
On the categorical side, we could replace $C_T$ and $C_{T'}$ with their pretopos completions, introducing new "quotients". Witing $\widehat{C}$ for the pretopos completion of $C$, a morphism of pretoposes $\widehat{C_T}\to \widehat{C_{T'}}$ corresponds to an interpretation of $T$ in $T'$.
Finally, we could beef up the definition of the syntactic category directly, allowing an object to be a pair $(\varphi(x),E(x,x'))$, where $E$ is a formula which $T$ proves defines an equivalence relation on $\varphi(x)$, and adjusting the notion of arrow appropriately. The resulting syntactic category, call it $C'_T$, is a Boolean pretopos, and again we work with pretopos morphisms.
It turns out that all three of these are essentially the same: $C'_T$, $\widehat{C_T}$, and $C_{T^{\mathrm{eq}}}$ are all equivalent as Boolean pretoposes. To make the notation simpler, let's just write $C_T$ for the pretopos assigned to the theory $T$.
What about models? The category $\mathsf{Set}$ can also be equipped with the structure of a Boolean pretopos. A pretopos morphism $M\colon C_T\to \mathsf{Set}$ assigns a set to each formula, in such a way that the logical structure is preserved (e.g., meets of subobjects correspond to intersections). That is, it's exactly a model of $T$. To me, this is one of the most interesting things about categorical logic: interpretations and models are the same kind of thing, namely structure-preserving functors.
Now if $I\colon C_{T'}\to C_T$ is the pretopos morphism corresponding to an interpretation of $T'$ in $T$. Then for any model $M\colon C_T\to \mathsf{Set}$, we can compose to get a model $M\circ I\colon C_{T'}\to \mathsf{Set}$. This is the map from models of $T$ to models of $T'$ obtained from the interpretation.
In other words, the contravariant functor $\mathrm{Mod}$ from theories to classes, assigning to each theory its class of models, is represented by the pretopos $\mathsf{Set}$, in the sense that $\mathrm{Mod}(-)\cong \mathrm{Hom}_{\mathsf{BoolPreTop}}(C_{-},\mathsf{Set})$.
Now what about a category of interpretations between structures? Well, an interpretation of $A$ in $B$ is just the same thing as an interpretation of the complete theory $\mathrm{Th}(A)$ in the complete theory $\mathrm{Th}(B)$ which happens to transform the model $B$ into the model $A$.
Now remember, $A$ is a model of its complete theory, i.e. a pretopos morphism $A\colon C_{\mathrm{Th}(A)}\to \mathsf{Set}$. Similarly, we have $B\colon C_{\mathrm{Th}(B)}\to \mathsf{Set}$. An interpretation $I\colon C_{\mathrm{Th}(A)}\to C_{\mathrm{Th}(B)}$ acts on models by composition, so it transforms $B$ into $A$ exactly when $B\circ I = A$.
Let's write $\mathsf{CBPT}$ for the category of complete Boolean pretoposes. This is the subcategory of Boolean pretoposes consisting of the complete theories.
It's now apparent that we can identify the category of structures and interpretations between them with the slice category $\mathsf{CBPT}/\mathsf{Set}$. An object is a pretopos morphisms from a complete Boolean pretopos to $\mathsf{Set}$ (a structure, viewed as a model of its complete theory) and an arrow is a pretopos morphism (an interpretation) which composes correctly with the models.
Finally, what about parameters? Well, an interpretation of $A$ in $B$ which uses arbitrary parameters from $B$ is the same thing as a parameter-free interpretation of $A$ in $B$ where we view $B$ as a structure in the language with a constant symbol for every element of $B$. In general, if we want to consider interpretations in $B$ using parameters from a subset $C\subseteq B$, we just need to name the elements of $C$ by constant symbols.
So every structure appears "many times" in the slice category $\mathsf{CBPT}/\mathsf{Set}$, once for each choice of which elements are named by constant symbols, and you can view morphisms into each of these objects as interpretations allowing different sets of parameters.