Leon Chwistek and Frank P. Ramsey proposed this as a simplification of the complicated and clumsy ramified theory of types specified in the Principia Mathematica by Alfred North Whitehead and Bertrand Russell.
However, by a result of Kurt Gödel, HOL with standard semantics does not admit an effective, sound, and complete proof calculus.
[2] The model-theoretic properties of HOL with standard semantics are also more complex than those of first-order logic.
[3] The Löwenheim number of first-order logic, in contrast, is ℵ0, the smallest infinite cardinal.
In Henkin semantics, a separate domain is included in each interpretation for each higher-order type.
According to several logicians, Gödel's ontological proof is best studied (from a technical perspective) in such a context.