Higher-order logics

In ordinary predicate—or so-called first-order—logic the objects x that ∀_x and ∃_x range over are variables of the kind used as arguments to functions (or predicates) such as f[x]. To set up second-order logic, however, one imagines also being able to use ∀_f and ∃_f where f is a function (say the head of f[x]). And then in third-order logic one imagines using ∀_g and ∃_g where g appears in g[f][x].

Early formulations of axiom systems for mathematics made little distinction between first- and second-order logic. The theory of types used in Principia Mathematica introduced some distinction, and following the proof of Gödel's Completeness Theorem for first-order logic in 1930 (see page 1152) standard axiom systems for mathematics (as given on pages 773 and 774) began to be reformulated in first-order form, with set theory taking over many of the roles of second-order logic.

In current mathematics, second-order logic is sometimes used at the level of notation, but almost never in its full form beyond. And in fact with any standard computational system it can never be implemented in any explicit way. For even to enumerate theorems in second-order logic is in general impossible for a system like a Turing machine unless one assumes that an oracle can be added. (Note however that this is possible in Henkin versions of higher-order logic that allow only limited function domains.)