[FOM] reducing higher to second order?

[H. Enderton]

Todd Wilson wrote:  
>I have seen passing references in the literature to a reduction of
>higher-order logic to second-order logic, but ...

I think of that as Montague's result, but Vaught and (independently)
Hintikka might be mentioned.

Lemma:  In second-order logic, you can express "A is the power set
of B" (using a binary predicate symbol to simulate epsilon).

Consequence:  The set of validities of k-order logic is recursively
isomorphic to the set of second-order validities.

Here k can have quite a variety of values.  Need not be finite!

I'll send a reference later, when I'm in the office.

Vaught once commented that studying second-order logic was like
"studying the standard model of set theory."  That is because
by iterating the above lemma (into the tranfinite), you can describe
a fair amount of the cumulative hierarchy.

--Herb Enderton