Hyperdoctrines and Monadic Second Order Logic

Question

This question is essentially the question I asked on Mathoverflow.

Monadic Second Order (MSO) logic is second order logic with quantification over unary predicates. That is, quantification over sets. There are several MSO logics that are fundamental to structures studied in computer science.

Question 1. Is there a categorical semantics for Monadic Second Order Logics?

Question 2. Treatments of categorical logic often talk about "higher order intuitionistic logic." Am I right to assume that they are referring to higher order functions, rather than quantification over second order predicates?

Question 3. (Added, 08 Nov 2013, after Neel's answer) My understanding of first-order quantification (in terms of the presentation of Pitts mentioned below) is that it is defined with respect to the pullback $\pi^*$ of a projection morphism $\pi$. Specifically, universal quantification is interpreted as the right adjoint of $\pi^*$ and existential quantification is interpreted as the left adjoint of $\pi^*$. These adjoints have to satisfy some conditions, which I have sometimes seen referred to as Beck-Chevalley and Frobenius-Reciprocity conditions.

Now if we want to quantify over predicates I assume I'm in a Cartesian closed category, the picture is nearly the same, except that $X$ below has a different structure from before.

$$ \exists_{I,X}, \forall_{I,X}: P_C(I\times X) \to P_C(I) $$

Is that right?

I believe my mental block was because I was previously dealing with first-order hyperdoctrines and did not need the category to be Cartesian closed and did not consider it later.

Background and Context. I have been working with the presentation of categorical logic by Andy Pitts in his Handbook of Logic in Computer Science article, but I'm also familiar with the treatment of Tripos theory in his doctoral dissertation, as well as the notes of Awodey and Bauer. I started out studying Crole's Categories for Types and the book by Lambek and Scott but it's been a while since I consulted the last two texts.

For motivation, I am interested in the kind of MSO logics appearing in the theorems below. I do not want to deal with a logic that is expressively equivalent to one of these. Meaning, I do not want to encode monadic predicates in terms of higher order functions and then deal with another logic, but I'm happy to study a semantics that includes such an encoding under the hood.

1. (Buechi and Elgot Theorem) When the universe of structures is finite words over a finite alphabet, a language is regular exactly if it is definable in MSO with an interpreted predicate for expressing consecutive positions.
2. (Buechi's Theorem) When the universe of structures is $\omega$-words over a finite alphabet, a language is $\omega$-regular exactly if it is definable in MSO with an appropriate interpreted predicate.
3. (Thatcher and Wright Theorem) A set of finite trees is recognizable by a bottom-up finite tree automaton exactly if it is definable in MSO with an interpreted predicate.
4. WS1S is the Weak Monadic Second order theory of One Successor. Formulae define sets of natural numbers and second order variables can only be interpreted as finite sets. WS1S can be decided by finite automata by encoding tuples of natural numbers as finite words.
5. (Rabin's Theorem) S2S is the Second order theory of Two Successors. S2S can be decided by Rabin automata.

Answer 1

1. I don't know!

2. No, your assumption is not right. You can quantify over higher-order functions and predicates in IHOL (in fact, predicates are just functions into a type of propositions). The setup looks a bit like this:

   $$ \begin{array}{llcl} \mbox{Sort} & \omega & ::= & \omega \to \omega \;\; | \;\; \omega \times \omega \;\; | \;\; 1 \;\;|\;\; \mathrm{prop} \;\;|\;\; \iota\\ \mbox{Term} & t & ::= & x \;\;|\;\; \lambda x.t \;\;|\;\; t\;t' \;\;|\;\; (t,t) \;\; | \;\; \pi_1(t) \;\;|\;\; \pi_2(t) \;\;|\;\; () \\ & & | & p \Rightarrow q \;\;|\;\; \top \;\;|\;\; p \wedge q \;\;|\;\; \bot \;\;|\;\; p \vee q \\ & & | & \forall x:\omega.p \;\;|\;\; \exists x:\omega.p \;\;|\;\; t =_\omega t' \\ & & | & f(\vec{t}) \end{array} $$

You give the usual typing rules to judge the well-formedness of a term. The first line of terms are the usual simply-typed lambda calculus, the second two lines are the propositions of higher-order logic (typed as elements of $\mathrm{prop}$), and the third line are whatever constants you use to form individuals (elements of $\iota$).

Then the idea is that you want to extend the Kripke semantics for first-order intuitionistic logic to higher-order logic, by extending the hyperdoctrine semantics with additional structure. A first-order hyperdoctrine is a functor $P : C^\mathrm{op} \to \mathrm{Poset}$ between a category $C$ with products (used to interpret the terms in context), and a category of posets (the truth value lattices), satisfying some conditions to make substitution work right.

To get to IHOL, you additionally assert that

1. $C$ is cartesian closed (to model the ability to quantify over function types), and
2. $C$ has an internal Heyting algebra $H$ satisfying the property that for every $\Gamma \in C$, $\mathit{Obj}(P(\Gamma)) \simeq C(\Gamma, H)$. You use $H$ to model $\mathrm{prop}$, and the isomorphism tells you that terms of type $\mathrm{prop}$ really do correspond to truth values.

This structure is almost an "elementary topos". If you additionally require that $P(\Gamma)$ is a poset of subojects of $\Gamma$, then you're there. (This essentially says that you can add a comprehension principle to your logic.)