My question regards the expressive power of second-order logic as compared with third-order logic. Throughout, I am working in the standard or full semantics of higher-order logics (so not the Henkin semantics).
My question is this: are there third-order formulas $\varphi$ and models $\mathcal{M}_1$ and $\mathcal{M}_2$ such that $\mathcal{M}_1$ and $\mathcal{M}_2$ agree on all second-order formulas but $\mathcal{M}_1 \vDash \varphi$ while $\mathcal{M}_2 \nvDash \varphi$? That is, is third-order logic strictly more expressively powerful than second-order logic?
Any reference pointers would be highly appreciated! I've looked through the standard sources (e.g., Shapiro's Foundations without Foundationalism Chp. 6, the entry in the Handbook of Phil Logic, the SEP article, etc.) but with no luck. It is a well-known result from Hintikka that there's an effective translation $\tau$ from third-order logic to second-order logic such that for any $\varphi$ in third-order logic, $\varphi$ is valid iff $\tau(\varphi)$ is valid. These sources cite this theorem, but this doesn't quite answer the question posed above, since the proof doesn't require checking $\neg\varphi$'s satisfiability and $\tau(\neg\varphi)$'s satisfiability in the same model. Apparently there's also a theorem stating that the smallest cardinal not describable by an $n$th-order logic is describable by the $n+1$th-order logic. If someone could point to a reference where this is proven, that would be great. But how big is this cardinal? Are we even guaranteed the existence of such undescribable cardinals for second-order logic? Thanks!
(Hi!)
Yes, model-by-model third-order logic is strictly stronger than second-order logic (and similarly for $n$ and $n+1$).
Since you mention it, I'll sketch the route via ordinals (and when I refer to an ordinal $\gamma$, I mean the linear order $(\gamma, \in)$). First, note that all the logics we're looking at are set-sized: for any language (= set of nonlogical symbols) $\Sigma$, there are set-many - in fact, $(\aleph_0\cdot\vert\Sigma\vert)$-many - second-order, third-order, etc. formulas. This means that there are only set-many second- or third-order theories in a given language; so since there is a proper class of structures in any language, we're always going to have indistinguishable structures.
For instance, for $\mathcal{L}_n$ = $n$th-order logic, there are at most continuum-many ordinals $\alpha$ which are characterized by their $\mathcal{L}_n$-theory (that is, such that for all ordinals $\beta$, $Th_{\mathcal{L}_n}(\alpha)=Th_{\mathcal{L}_n}(\beta)\iff \alpha=\beta$). And there are at most countably many ordinals which are characterized (amongst all ordinals) by some single $\mathcal{L}_n$-sentence.
Now, as to the meat of your question, here's a sketch of an answer. $\mathcal{L}_n$-equivalence can be described via higher-order Ehrenfeucht-Fraisse games - just play the corresponding usual EF-game on the iterated powersets of the structures in question. It's not too nasty to use this characterization to show that there is a sentence $\varphi$ of $\mathcal{L}_{n+1}$ such that an ordinal $\beta$ satisfies $\varphi$ iff $\beta$ is $\mathcal{L}_n$-equivalent to some proper initial segment. This then lets us describe - in $\mathcal{L}_{n+1}$ - the least $\beta$ which is $\mathcal{L}_n$-equivalent to some smaller ordinal. But then we're done.