What is the theorem that shows that second-order logic is the ceiling of model characterization?

Question

I was reading this blog posting and the following claim was made:

...[T]here's tricks for making second-order logic encode any proposition in third-order logic and so on. If there's a collection of third-order axioms that characterizes a model, there's a collection of second-order axioms that characterizes the same model. Once you make the jump to second-order logic, you're done - so far as anyone knows (so far as I know) there's nothing more powerful than second-order logic in terms of which models it can characterize.

I think I've heard similar claims before -- that second-order logic provides us all the resources we could have for characterizing models.

Is this claim correct? What is the theorem associated with this claim?

Answer 1

I believe the result you are looking for is mentioned here: http://plato.stanford.edu/entries/logic-higher-order/#4

More specifically, we have the following result of Hintikka (1955): For each formula φ of higher-order logic (in a language with finitely many non-logical symbols), we can effectively find a sentence ψ of second-order logic (in the language of equality) such that φ is valid if and only if ψ is valid.

The basic notion is that the powerset operation is definable in second order logic, which allows for the simulation of higher order logics.