Editing Higher-order logic (section)

== Semantics ==
There are two possible semantics for higher-order logic.

In the ''standard'' or ''full semantics'', quantifiers over higher-type objects range over ''all'' possible objects of that type. For example, a quantifier over sets of individuals ranges over the entire [[powerset]] of the set of individuals. Thus, in standard semantics, once the set of individuals is specified, this is enough to specify all the quantifiers. HOL with standard semantics is more expressive than first-order logic. For example, HOL admits [[Morley's categoricity theorem|categorical]] axiomatizations of the [[natural number]]s, and of the [[real number]]s, which are impossible with first-order logic. However, by a result of [[Kurt Gödel]], HOL with standard semantics does not admit an [[computable function|effective]], sound, and [[Gödel's completeness theorem|complete]] [[proof calculus]].<ref>Shapiro 1991, p.&nbsp;87.</ref> The model-theoretic properties of HOL with standard semantics are also more complex than those of first-order logic. For example, the [[Löwenheim number]] of [[second-order logic]] is already larger than the first [[measurable cardinal]], if such a cardinal exists.<ref>[[Menachem Magidor]] and [[Jouko Väänänen]]. "[http://www.math.helsinki.fi/logic/people/jouko.vaananen/JV96.pdf On Löwenheim-Skolem-Tarski numbers for extensions of first order logic]", Report No. 15 (2009/2010) of the Mittag-Leffler Institute.</ref> The Löwenheim number of first-order logic, in contrast, is [[Aleph nought|ℵ<sub>0</sub>]], the smallest infinite cardinal. 

In '''Henkin semantics''', a separate domain is included in each interpretation for each higher-order type. Thus, for example, quantifiers over sets of individuals may range over only a subset of the [[powerset]] of the set of individuals. HOL with these semantics is equivalent to [[many-sorted first-order logic]], rather than being stronger than first-order logic. In particular, HOL with Henkin semantics has all the model-theoretic properties of first-order logic, and has a complete, sound, effective proof system inherited from first-order logic.