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!