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

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

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