Does interpretability generalize model theory?

Question

I recently was wondering about how one could in some sense generalize model theory to the case where the meta theory is not a set theory. I just stumbled across this answer about interpretability ( https://math.stackexchange.com/a/315451/463016 ) and was curious if this does in some sense do that, or if not, whether there is something else that does?

Answer 1

Yes, if you take the perspective of categorical logic. The key idea of categorical logic is that to every flavor of logic, you can associate some categorical structure. Every theory $T$ of the logic is represented by a category $C_T$ with that structure, a model of $T$ is a functor $C_T \to \mathrm{Set}$ which preserves the structure in the appropriate way, and an interpretation of $T$ in $T'$ is a functor $C_T \to C_{T'}$, which again preserves the structure appropriately.

So models and interpretations are the same kinds of things. More broadly, given any category $D$, you can call a structure-preserving functor $C_T\to D$ a model of $T$ in $D$ or an interpretation of $T$ in $D$. And more radically, you can view every structured category as a theory and every structure-preserving functor as a model/interpretation.

The simplest example of this paradigm is Lawvere theories (categories with finite products), which captures equational logic. The categorical structure capturing classical first-order logic is more complicated: these categories are called Boolean pretoposes.

I should note that while conceptually one can erase the distinction between models and interpretations, in practice the categories (like Set) that are appropriate for models and the categories (like $C_T$) that are appropriate for interpretations tend to have a different flavor.

For example, there's a big difference between a model of $T$ in Set and an interpretation of $T$ in set theory (let's say ZFC for concreteness). In Set, the objects are sets and the arrows are functions. In $C_{\mathrm{ZFC}}$, the objects are definable sets relative to ZFC (i.e. definable classes) and the arrows are definable functions (i.e. definable class functions). This distinction is the main point of Malice Vidrine's answer.

Answer 2

I want to first preface this by mentioning that it's been a while since I used any of this stuff, so I may need to edit this for silly mistakes a couple of times.

While it's true that there are interpretations of theories into set theory that don't coincide with the existence of models (such as the interpretation of $\mathsf{ZFC}$ in $\mathsf{ZF}$), the converse (that there are models that don't admit description as instances of some syntactic translation) may also be true, I think. For a model with carrier set $M$, the natural thing to do is take "$x\in M$" as the translation of "$\mathrm{Dom}(v)$"; but under most treatments, the translation of $\mathrm{Dom}(v)$ is allowed to have exactly one free variable, so you'd need to be able to express $M$ as a closed abstract. (Perhaps someone else can fill in the gap here about what can be proven about the existence of indefinable models.)

Nevertheless, you can apply interpretability without knowing too much about semantics, and you can ask things like "does $S$ have an interpretation in $\mathsf{PA}$" when you can't necessarily ask "does it have a model in $\mathsf{PA}$," for example.

Additional comments

To answer what $\mathrm{Dom}(v)$ represents, let's assume that this predicate is in the language of the theory $S$, and its translation is in the language of the the theory $T$. The translation (which I denote $i(\mathrm{Dom}(v))$ following the linked post) is meant to delineate, in the universe of $T$, the "sub-universe" in which $S$ is interpreted. That is, for any model $\mathcal{M}\vDash T$ and any $\varphi$ in the language of $S$, every quantifier in the translation $i(\varphi)$ will be restricted to $\{x\in M\;|\;\mathcal{M}\vDash\ulcorner i(\mathrm{Dom}(v))\urcorner[x]\}$. For example, in the $\mathsf{ZFC}$-into-$\mathsf{ZF}$ example, we can interpret "$\mathrm{Dom}(v)$" (once we add it to the language of $\mathsf{ZFC}$) as "$v\textrm{ is constructible}$."

The reason $i(\mathrm{Dom}(v))$ is not allowed to have any variables beyond $v$ is simply that for any sentence $\varphi\in S$, $i(\varphi)$ is also supposed to be a sentence with $T\vdash i(\varphi)$. If the translation adds on new variables, this breaks down and takes closed formulae to open ones. (However, it is permissible that $i(\mathrm{Dom}(v))$ have no free variables, contrary to what I recalled when I commented.)

I hope this answers your question a little, and if it doesn't, I hope it's informative in other ways.