Categorical Semantics for Second-Order Logics

Question

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 the Handbook 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.

Answer 1

I think the main references for this are Jacobs's book Categorical Logic and Type Theory (Chapter 8), and also Crole's Categories for Types.

The rough idea is to do categorical logic over the `algebraic theory of types'. That is, you consider a category whose objects are finite products of a certain object $\mathit{Type}$, and whose morphisms $A \to \mathit{Type}$ are thought of as types with free type variables in $A$. Then, models are fibrations over such categories, of which you ask for more structure to be able to quantify over predicates. By carefully tuning what you demand, you may obtain quantification over all kinds of higher-order predicates, but there are ways of sticking to second-order logic.

Regarding your terminological question about the term `higher-order', I'd say `higher-order' refers both to higher-order functions and to quantification over higher-order predicates, as in, e.g., System $F\omega$. This is of course annoying.