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

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

• If I understand you correctly, the Kripke-Joyal semantics does precisely what you are asking for: it translates the internal validity of a statement $\phi$ expressed in higher-order logic to an external statement giving equivalent conditions that refer to the structure of the topos $\mathcal{E}$. Aug 14, 2021 at 17:28

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