extension of regular logic The internal language of some categories (such as abelian categories) support only a fraction of first order logic. But every category can be fully faithfully embedded into a category of presheaves, and any such presheaf category is a topos and supports full higher order logic. If I am able to proof that some sentence $\phi$ using HOL and if $\phi$ is a sentence which is in the regular first order fragment of HOL, does then also $\vdash \phi$ hold in first order regular logic?
Is there some other way to exploit the embedding of a regular category into its presheaf category on a logical level?
 A: The correct way of doing this is to embed regular categories into categories of sheaves.
We have the following fact:
Proposition.
Let $\mathcal{C}$ be a small regular category and let $\mathcal{E}$ be the category of all functors $X : \mathcal{C}^\textrm{op} \to \textbf{Set}$ such that, for every regular epimorphism $p : A \twoheadrightarrow B$ in $\mathcal{C}$, $X (p) : X (B) \to X (A)$ is the equaliser of the evident parallel pair $X (A) \rightrightarrows X (A \times_B A)$.
Then:

*

*$\mathcal{E}$ is a Grothendieck topos.

*The Yoneda embedding $\mathcal{C} \to [\mathcal{C}^\textrm{op}, \textbf{Set}]$ factors through $\mathcal{E}$, i.e. every representable presheaf on $\mathcal{C}$ is in $\mathcal{E}$.

*The Yoneda embedding $\mathcal{C} \to \mathcal{E}$ preserves regular epimorphisms.

From the above fact we deduce that any sentence in the internal language of $\mathcal{C}$ as a regular category is true in $\mathcal{C}$ if and only if it is true in $\mathcal{E}$.
Here, it is crucial that we use $\mathcal{E}$ and not $[\mathcal{C}^\textrm{op}, \textbf{Set}]$: the Yoneda embedding $\mathcal{C} \to [\mathcal{C}^\textrm{op}, \textbf{Set}]$ does not preserve regular epimorphisms in general.
Since this holds for all (small) regular categories $\mathcal{C}$, we deduce that topos HOL is a conservative extension of regular logic.
Since you mentioned abelian categories, I would be remiss if I did not mention the Freyd–Mitchell embedding theorem, which is a much stronger result: it says every small abelian category $\mathcal{A}$ embeds as an exact full subcategory of the category of $R$-modules, for some (non-commutative) ring $R$ (depending on $\mathcal{A}$, of course).
