Higherorder logic
In mathematics and logic, a higherorder logic is a form of predicate logic that is distinguished from firstorder logic by additional quantifiers and, sometimes, stronger semantics. Higherorder logics with their standard semantics are more expressive, but their modeltheoretic properties are less wellbehaved than those of firstorder logic.
The term "higherorder logic", abbreviated as HOL, is commonly used to mean higherorder simple predicate logic. Here "simple" indicates that the underlying type theory is simple, not polymorphic or dependent.^{[1]}
Contents
Quantification scope
Firstorder logic quantifies only variables that range over individuals; secondorder logic, in addition, also quantifies over sets; thirdorder logic also quantifies over sets of sets, and so on.
Higherorder logic is the union of first, second, third, …, nthorder logic; i.e., higherorder logic admits quantification over sets that are nested arbitrarily deeply.
Semantics
There are two possible semantics for higher order logic.
In the standard or full semantics, quantifiers over highertype 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 firstorder logic. For example, HOL admits categorical axiomatizations of the natural numbers, and of the real numbers, which are impossible with firstorder logic. However, by a result of Gödel, HOL with standard semantics does not admit an effective, sound, and complete proof calculus.^{[2]}
The modeltheoretic properties of HOL with standard semantics are also more complex than those of firstorder logic. For example, the Löwenheim number of secondorder logic is already larger than the first measurable cardinal, if such a cardinal exists.^{[3]} The Löwenheim number of firstorder logic, in contrast, is ℵ_{0}, the smallest infinite cardinal.
In Henkin semantics, a separate domain is included in each interpretation for each higherorder 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 manysorted firstorder logic, rather than being stronger than firstorder logic. In particular, HOL with Henkin semantics has all the modeltheoretic properties of firstorder logic, and has a complete, sound, effective proof system inherited from firstorder logic.
Examples and properties
Higher order logics include the offshoots of Church's Simple theory of types^{[4]} and the various forms of Intuitionistic type theory. Gérard Huet has shown that unifiability is undecidable in a type theoretic flavor of thirdorder logic,^{[5]}^{[6]}^{[7]} that is, there can be no algorithm to decide whether an arbitrary equation between thirdorder (let alone arbitrary higherorder) terms has a solution.
Up to a certain notion of isomorphism, the powerset operation is definable in secondorder logic. Using this observation, Hintikka established in 1955 that secondorder logic can simulate higherorder logics in the sense that for every formula of a higher orderlogic one can find an equisatisfiable formula for it in secondorder logic.^{[8]}
The term "higherorder logic" is assumed in some context to refer to classical higherorder logic. However, modal higherorder logic has been studied as well. According to several logicians, Gödel's ontological proof is best studied (from a technical perspective) in such a context.^{[9]}
See also
 Firstorder logic
 Secondorder logic
 Higherorder grammar
 Higherorder logic programming
 Intuitionistic Type Theory
 Manysorted logic
 Typed lambda calculus
 Modal Logic
Notes
 ^ Jacobs, 1999, chapter 5
 ^ Shapiro 1991, p. 87.
 ^ Menachem Magidor and Jouko Väänänen. "On LöwenheimSkolemTarski numbers for extensions of first order logic", Report No. 15 (2009/2010) of the MittagLeffler Institute.
 ^ Alonzo Church, A formulation of the simple theory of types, The Journal of Symbolic Logic 5(2):56–68 (1940)
 ^ Huet, Gérard P. (1973). "The Undecidability of Unification in Third Order Logic" (PDF). Information and Control. 22 (3): 257–267. doi:10.1016/s00199958(73)90301x.
 ^ Huet, Gérard (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.) (in French). Universite de Paris VII.
 ^ Huet, Gérard (2002). "Higher Order Unification 30 years later". In Carreño, V.; Muñoz, C.; Tahar, S. Proceedings, 15th International Conference TPHOL (PDF). LNCS. 2410. Springer. pp. 3–12.
 ^ entry on HOL

^ Fitting, Melvin (2002). Types, Tableaus, and Gödel's God. Springer Science & Business Media. p. 139. ISBN 9781402006043.
Godel's argument is modal and at least secondorder, since in his definition of God there is an explicit quantification over properties. [...] [AG96] showed that one could view a part of the argument not as secondorder, but as thirdorder.
References
 Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed, Kluwer Academic Publishers, ISBN 1402007639
 Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for SecondOrder Logic". Oxford University Press., ISBN 0198250290
 Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell, ISBN 0631206930
 Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press, ISBN 0521356539
 Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0444501703.
 Benzmuller, Christoph; Miller, Dale (2014). "Automation of HigherOrder Logic". In Gabbay, Dov M.; Siekmann, Jörg H.; Woods, John. Handbook of the History of Logic, Volume 9: Computational Logic. Elsevier. ISBN 9780080930671.
External links
 Andrews, Peter B, Church's Type Theory in Stanford Encyclopedia of Philosophy.
 Miller, Dale, 1991, "Logic: Higherorder," Encyclopedia of Artificial Intelligence, 2nd ed.
 Herbert B. Enderton, Secondorder and Higherorder Logic in Stanford Encyclopedia of Philosophy, published Dec 20, 2007; substantive revision Mar 4, 2009.