[FOM] reducing higher to second order?

[Harvey Friedman]

On 12/17/03 4:27 PM, "Todd Wilson" <twilson at csufresno.edu> wrote:

> I have seen passing references in the literature to a reduction of
> higher-order logic to second-order logic, but none of the sources I
> have at hand make any mention of it.  Can anyone supply a statement of
> this reduction and/or point me to where it was first (or most
> perspicuously) established?

Here are two formulations.

1. There is a (primitive) recursive function that maps sentences in higher
order logic into sentences in second logic such that a given sentence in
higher order logic is satisfiable (under the usual semantics for higher
order logic) if and only if it its value is satisfiable (under the usual
semantics for second order logic). Furthermore, this is straightforwardly
provable in any fragment of ZF which directly formalizes the semantics for
higher order logic, such as Zermelo set theory.

2. There is an explicitly given (primitive) recursive function accomplishing
1 that is fully intelligible and informative.

I'm no historian, but what about Tarski?

Harvey Friedman