Internal logic of locally strongly finitely presentable categories There is a duality between locally strongly finitely presentable categories and (Cauchy complete) cartesian categories, i.e. multisorted algebraic theories. The internal logic of cartesian categories is well known to be first-order equational logic. What is the internal logic of locally strongly finitely presentable categories? It should at least subsume "exact logic" (i.e. have finite conjunction, existential quantification, and quotients of equivalence relations), since the category of models for any multisorted algebraic theory is exact. However, it may not be describable as fragment of first-order logic, because although there exist arbitrary disjunctions, conjunction does not distributive over disjunction.
 A: The comments are getting a bit long (sorry, that is largely my fault), so I think it's worth expanding on Jiří Rosický 's point, which comes very close to completely answering the question.
Adamek, Lawvere, and Rosicky introduced the notion of an algebraically exact category in How algebraic is algebra?, giving a precise definition of what it means for a category to have all of the "exactness" properties enjoyed by (possibly multisorted) varieties (= algebraic categories = locally strongly finitely-presentable) categories. The definition is conceptually illuminating: the forgetful functor $Var \to Cat$ has a left adjoint, and an algebraically exact category is defined to be a pseudoalgebra for the induced pseudomonad on $Cat$.
They observed that every algebraically exact category $\mathcal C$ has the following properties:

*

*$\mathcal C$ has limits.


*$\mathcal C$ has sifted colimits.


*$\mathcal C$ is Barr-exact.


*finite limits commute with filtered colimits in $\mathcal C$.


*regular epimorphisms are stable under products in $\mathcal C$.


*filtered colimits distribute over products in $\mathcal C$.\


*(This one must apparently follow from the rest: regular epis are stable under pullback.)
They conjectured that these properties completely characterize the algebraically exact categories. This conjecture was proven under various additional assumptions by these and other authors, until it was finally proven in full generality by Garner in A characterization of algebraic exactness (see Garner for a full bibliography).
Upshot: It would seem the appropriate internal logic would be "whatever you can express using the above properties". In particular, Barr-exactness gives a good fragment of logic. Stability of regular epis under pullback probably lets you do a reasonable amount more. Perhaps others can elaborate on / correct these statements.
Side note: I would assume that only the "finitary" fragment of the above properties would be relevant to building an internal logic as it's usually conceived. I would be interested to be proven wrong about that though!
