(For simplicity, all languages are relational.)
In analogy with first-order languages, say that a second-order language is a set of relation symbols of two kinds: first-order relation symbols and second-order relation symbols. Both types of symbols have a notion of arity; the arity of a first-order relation symbol is a natural number, and the arity of a second-order relation symbol is a finite string of natural numbers.
Given a second-order language $\Sigma=\langle\Sigma_1,\Sigma_2\rangle$ (with $\Sigma_i$ denoting the set of $i$th-order symbols of $\Sigma$), a $\Sigma$-structure is defined in the obvious way: as a triple $\mathcal{A}=(A; \mathfrak{I}_1,\mathfrak{I}_2)$ such that
-
$A$ is a (nonempty) set,
-
$\mathfrak{I}_1$ is a map sending each $R\in\Sigma_1$ with arity $n$ to a subset of $A^n$, and
-
$\mathfrak{I}_2$ is a map sending each $S\in\Sigma_2$ with arity $\alpha$ to a subset of $\mathcal{P}(A^{\alpha(1)})\times…\times\mathcal{P}(A^{\alpha(\vert\alpha\vert)})$.
There is an obvious semantics for second-order logic over a structure in a second-order language (note that this extends the "full"/"standard" semantics, rather than the Henkin semantics, for second-order logic in the context of first-order languages). I'm curious whether Craig interpolation holds in this broader framework:
Suppose $\varphi,\theta$ are $\mathsf{SOL}$-sentences in second-order languages $\Sigma,\Pi$ respectively such that $\varphi\models\theta$. Must there be a $\mathsf{SOL}[\Sigma\cap\Pi]$-sentence $\delta$ such that $\varphi\models\delta$ and $\delta\models\theta$?
Craig interpolation for $\mathsf{SOL}$ is trivial in the context of first-order languages, since we can appropriately quantify out the non-shared symbols. But that doesn't work here. In fact, I suspect that the answer is negative via an easy construction, but I don't immediately see it.
(Incidentally, it's possible that my restriction to relational languages is less benign for these purposes than it appears. I'm happy to generalize in the obvious way to allow function symbols!)
Best Answer
This is just an expansion of Emil Jerabek's comments above; I've made it CW to avoid reputation gain, and will delete this if he posts an answer of his own.
Craig interpolation can be rephrased as a "syntactic separation" property: the statement $$\varphi\models\psi$$ can be rephrased as $$\emptyset\models\exists\mathfrak{R}(\varphi[\mathfrak{R}])\rightarrow\exists\mathfrak{S}(\varphi[\mathfrak{S}])$$ for some appropriate objects $\mathfrak{R},\mathfrak{S}$ corresponding to the uncommon parts of the languages of $\varphi,\psi$ respectively. Now if our "base logic" is first-order then this is broadly speaking where the story ends, but using second-order logic as our "base" gives us a lot more power.
Specifically, since we can pin down $\mathcal{N}=(\mathbb{N};+,\times)$ up to isomorphism, we can "localize" the syntactic separation result above into a separation result for sets of natural numbers: if "fully-second-order" logic had the Craig interpolation property then any two disjoint $\Sigma^2_1$ subsets of $\mathcal{N}$ could be separated by a second-order-definable set of naturals, but this is impossible (by Tarski) since the usual-second-order theory of $\mathcal{N}$ is $\Delta^2_1$.
This raises a natural follow-up question:
The point of the "not too strong" requirement is that there is an obvious extension of $\mathsf{SOL}$ which has the interpolation property for second-order languages - third-order logic (which then loses interpolation for third-order languages, and so forth)!