Comparing Kripke-Joyal semantics of toposes to model-theoretic satisfaction

Question

Let $\mathcal E$ be a topos and $\varphi$ a statement formulating a property of toposes. There are two ways of checking whether $\mathcal E$ satisfies $\varphi$:

1. Consider the first-order language $L$ of a category. Each topos can be considered as an $L$-structure. So, using standard model-theoretic notions, one can consider the satisfaction relation, $\mathcal E\models \varphi$.

2. Using the Kripke-Joyal semantics, one can look at whether $\varphi$ is true in the internal language of $\mathcal E$.

Roughly, one difference between 1. and 2. is that in 1. only the notions "object", "arrow", and "composition" occuring in $\varphi$ are interpreted in $\mathcal E$, while the logic is interpreted on the meta level. However, in 2. also the logic (i.e., the quantifiers $\forall$ and $\exists$ and $\land, \lor, \neg, \dots$) are interpreted in $\mathcal E$.

Strictly speaking, this is not an appropriate comparison because in 1. $\varphi$ is a first-order $L$-sentence and in 2. $\varphi$ is a sentence in higher-order logic. However, in spirit 1. and 2. feel similar, because the give a way of looking whether a statement is true in a topos.

Is there some way of comparing 1. and 2., and can one say anything interesting about this comparison?

In particular, I wonder whether the following works: given a sentence $\varphi$ in higher-order logic, can one assign to it a sentence $\varphi'$ in first-order logic such that $\varphi$ is true in the internal language of $\mathcal E$ if and only if $\mathcal E\models \varphi'$ in the model-theoretic sense? (And what about the other way round?)

Answer 1

As you observe yourself, the question does not quite make sense as $\phi$ in 1. is a formula in the first order language of a category and in 2. $\phi$ is a formula in higher order logic (something like the Mitchel-Benabou language).

The only framework I can think of where this question makes perfect sense is if you interpret "internal logic" in the sense of Mike Shulman "Stack semantics" as in his paper https://arxiv.org/abs/1004.3802.

Here you interpret "the first-order language of categories" as in def. 3.1 of the paper linked above, and the stack semantics is an extention of the Kripke-Joyal semantics that is also formulated in that language (where the higher order part come from the fact that you can quantify on objects).

In this case, as pointed out by Andrej Bauer, the Kripke-Joyal semantics (or rather its extention called the stack semantics) turns a formula $\phi$ in this language to a formula $\phi'$, so that "$\phi$ hold internally in $\mathcal{E}$" if and only if $\mathcal{E}$ satisfies $\phi'$).

Of course $\phi'$ is in general different from $\phi$, though I believe $\phi'' = \phi'$.

In any case, not every formula arise as a $\phi'$ (i.e. corresponds to an "internal property"). For example, the validity of such formulas are always local properties: if $\mathcal{E}$ satisfies $\phi'$ then every slice $\mathcal{E}/X$ also satisfies $\phi'$; and conversely if $\mathcal{E}/X$ satisfies $\phi'$ for a family of objects covering the terminal, then $\mathcal{E}$ also satisfies $\phi'$.