In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics. Higher-order logics with their standard semantics are more expressive, but their model-theoretic properties are less well-behaved than those of first-order logic.
First-order logic quantifies only variables that range over individuals; second-order logic, in addition, also quantifies over sets; third-order logic also quantifies over sets of sets, and so on. For example, the second-order sentence ∀P. (0∈P ∧ ∀i. i∈P → i+1∈P) → (∀n. n∈P) expresses the principle of mathematical induction. Higher-order logic is the union of first-, second-, third-, ... order logic; i.e. it admits quantification over arbitrarily deep nested sets.
Higher-order simple predicate logic
The term "higher-order logic", abbreviated as HOL, is commonly used to mean higher order simple predicate logic. Here "simple" indicates that the underlying type theory is simple, not polymorphic or dependent.
There are two possible semantics for HOL. 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 categorical axiomatizations of the natural numbers, and of the real numbers, which are impossible with first-order logic. However, by a result of Gödel, HOL with standard semantics does not admit an effective, sound and complete proof calculus.
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. 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. 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.
Higher order logics include the offshoots of Church's Simple Theory of Types and the various forms of Intuitionistic type theory. Gérard Huet has shown that unifiability is undecidable in a type theoretic flavor of third-order logic, that is, there can be no algorithm to decide if an arbitrary equation between third-order (let alone arbitrary higher-order) terms has a solution.
- First-order logic
- Second-order logic
- Higher-order grammar
- Intuitionistic Type Theory
- Many-sorted logic
- Typed lambda calculus
- Jacobs, 1999, chapter 5
- Menachem Magidor and Jouko Väänänen. "On Löwenheim-Skolem-Tarski numbers for extensions of first order logic", Report No. 15 (2009/2010) of the Mittag-Leffler Institute.
- Alonzo Church, A formulation of the simple theory of types, The Journal of Symbolic Logic 5(2):56–68 (1940)
- Gérard P. Huet (1973). "The Undecidability of Unification in Third Order Logic". Information and Control 22: 257–267.
- Gérard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Universite de Paris VII.
- Gérard Huet (2002). "Higher Order Unification 30 years later". In V. Carreño and C. Muñoz and S. Tahar. Proceedings, 15th International Conference TPHOL. LNCS 2410. Springer. pp. 3–12.
- Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed, Kluwer Academic Publishers, ISBN 1-4020-0763-9
- Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press., ISBN 0-19-825029-0
- Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell, ISBN 0-631-20693-0
- Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press, ISBN 0-521-35653-9
- Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3.
- Andrews, Peter B, Church's Type Theory in Stanford Encyclopedia of Philosophy.
- Miller, Dale, 1991, "Logic: Higher-order," Encyclopedia of Artificial Intelligence, 2nd ed.
- Herbert B. Enderton, Second-order and Higher-order Logic in Stanford Encyclopedia of Philosophy, published Dec 20, 2007; substantive revision Mar 4, 2009.