I am currently doing some work using a categorical semantics of first-order logic. The specific semantics I am using is due to Andrew Pitts, as described in:

Categorical Logic, Andrew M. Pitts, chapter in theHandbook of Logic in Computer Science, Volume VI, 1995.

In this treatment, the syntax uses terms-in-context and formulae-in-context, instead of just terms and formulae. A context of a term is, loosely, the set of free variables in the term and their types. A formula in classical first-order logic is interpreted using a category $\mathcal{C}$ with finite products, and a contravariant functor $\mathit{Prop}_\mathcal{C}$ from $\mathcal{C}$ to the category of posets and monotone functions. Propositional connectives are characterized in terms of meets and joins in the category and (generalized) quantifiers arise as adjoints of projections.

This semantics has the property that over the category of sets, satisfaction agrees with satisfaction in the Tarskian sense. This property is important for the work I am doing.

* Question.* Is there a categorical treatment of (Monadic) Second-Order Logic with the same property? Ideally, a categorical semantics that is transparent in the sense that it is almost obvious that it agrees with the Tarskian semantics on the category of sets (or a Boolean topos, which I expect is what I need).

My impression is that the term *higher-order* in categorical logic typically applies to higher-order functions rather than uninterpreted predicates. Please let me know if this impression is incorrect.

For your information,I am aware that there are slightly different treatments of these concepts starting from Lawvere's *Adjointness in Foundations* paper and I've consulted the work of Makkai and Reyes, Lambek and Scott, Crole, course notes by Awodey and Bauer and the work of Pitts on Tripos theory.