Editing Higher-order logic

{{Short description|Formal system of logic}}
In [[mathematics]] and [[logic]], a '''higher-order logic''' (abbreviated '''HOL''') is a form of logic that is distinguished from [[first-order logic]] by additional [[Quantification (logic)|quantifiers]] and, sometimes, stronger [[semantics of logic|semantics]]. Higher-order logics with their standard semantics are more expressive, but their [[Model theory|model-theoretic]] properties are less well-behaved than those of first-order logic.

The term "higher-order logic" is commonly used to mean '''higher-order simple predicate logic'''. Here "simple" indicates that the underlying [[type theory]] is the ''theory of simple types'', also called the ''simple theory of types''. [[Leon Chwistek]] and [[Frank P. Ramsey]] proposed this as a simplification of ''ramified theory of types'' specified in the ''[[Principia Mathematica]]'' by [[Alfred North Whitehead]] and [[Bertrand Russell]]. ''Simple types'' is sometimes also meant to exclude [[type polymorphism|polymorphic]] and [[dependent type|dependent]] types.<ref>Jacobs, 1999, chapter 5</ref>

== Quantification scope ==
{{redirect|Ordered logic|the unrelated term in linear logic|Noncommutative logic}}

First-order logic quantifies only variables that range over individuals; ''[[second-order logic]]'', also quantifies over sets; ''third-order logic'' also quantifies over sets of sets, and so on. 

''Higher-order logic'' is the union of first-, second-, third-, ..., ''n''th-order logic; ''i.e.,'' higher-order 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 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.

== Properties ==
Higher-order logics include the offshoots of [[Alonzo Church|Church]]'s [[simple theory of types]]<ref name="church">[[Alonzo Church]], [https://www.jstor.org/stable/2266170 ''A formulation of the simple theory of types''], [[The Journal of Symbolic Logic]] 5(2):56&ndash;68 (1940)</ref> and the various forms of [[intuitionistic type theory]]. [[Gérard Huet]] has shown that [[Unification (computer science)#Higher-order unification|unifiability]] is [[Undecidable problem|undecidable]] in a [[Intuitionistic type theory|type-theoretic]] flavor of third-order logic,<ref>{{cite journal |last=Huet |first=Gérard P. |date=1973 |title=The Undecidability of Unification in Third Order Logic |journal=[[Information and Control]] |doi=10.1016/s0019-9958(73)90301-x |volume=22 |issue=3 |pages=257–267 |doi-access= }}</ref><ref>{{cite thesis |type=Ph.D. |last=Huet |first=Gérard |date=Sep 1976 |title=Resolution d'Equations dans des Langages d'Ordre 1,2,...ω |language=French |publisher=Universite de Paris VII|url=https://www.researchgate.net/publication/213879499}}</ref><ref>{{cite journal | url=http://www.sciencedirect.com/science/article/pii/0304397581900402/pdf?md5=ebe7687d034498bb76c4ea9c5df56f84&pid=1-s2.0-0304397581900402-main.pdf | author=Warren D. Goldfarb | title=The Undecidability of the Second-Order Unification Problem | journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]] | volume=13 | pages=225&ndash;230 | year=1981 | issue=2 | doi=10.1016/0304-3975(81)90040-2 }}</ref><ref>{{cite book |last=Huet |first=Gérard |date=2002 |editor1-last=Carreño |editor1-first=V. |editor2-last=Muñoz |editor2-first=C. |editor3-last=Tahar |editor3-first=S. |chapter=Higher Order Unification 30 years later |title=Proceedings, 15th International Conference TPHOL |volume=2410 |pages=3–12 |publisher=Springer |series=LNCS |chapter-url=http://pauillac.inria.fr/~huet/PUBLIC/Hampton.pdf }}</ref> that is, there can be no algorithm to decide whether an arbitrary equation between second-order (let alone arbitrary higher-order) terms has a solution.

Up to a certain notion of [[isomorphism]], the powerset operation is definable in second-order logic. Using this observation, [[Jaakko Hintikka]] established in 1955 that second-order logic can simulate higher-order logics in the sense that for every formula of a higher-order logic, one can find an [[equisatisfiability|equisatisfiable]] formula for it in second-order logic.<ref>[http://plato.stanford.edu/entries/logic-higher-order/#4|SEP entry on HOL]</ref>

The term "higher-order logic" is assumed in some context to refer to ''[[classical logic|classical]]'' higher-order logic. However, [[modal logic|modal]] higher-order 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.<ref name="Fitting2002">{{cite book |last=Fitting |first=Melvin |authorlink=Melvin Fitting |date=2002 |title=Types, Tableaus, and Gödel's God |publisher=Springer Science & Business Media |isbn=978-1-4020-0604-3 |page=139 |quote=Godel's argument is modal and at least second-order, 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 second-order, but as third-order.}}</ref>

==See also==
* [[Zeroth-order logic]] (propositional logic)
* [[First-order logic]]
* [[Second-order logic]]
* [[Type theory]]
* [[Higher-order grammar]]
* [[Higher-order logic programming]]
* [[HOL (proof assistant)]]
* [[Many-sorted logic]]
* [[Typed lambda calculus]]
* [[Modal logic]]

==Notes==
{{Reflist}}

==References==
* [[Peter B. Andrews (mathematician)|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}}
* [[Joachim Lambek|Lambek, J.]] and Scott, P. J., 1986. ''Introduction to Higher Order [[Categorical logic|Categorical Logic]]'', Cambridge University Press, {{ISBN|0-521-35653-9}}
* {{cite book
  | last = Jacobs
  | first = Bart
  | date = 1999
  | title = Categorical Logic and Type Theory
  | publisher = North Holland, Elsevier
  | isbn =  0-444-50170-3
  | series = Studies in Logic and the Foundations of Mathematics 141
  | url = https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html }}
* {{cite book |last1=Benzmüller |first1=Christoph |last2=Miller |first2=Dale |editor1-last=Gabbay |editor1-first=Dov M. |editor2-last=Siekmann |editor2-first=Jörg H. |editor3-last=Woods |editor3-first=John |date=2014 |title=Handbook of the History of Logic, Volume 9: Computational Logic |chapter=Automation of Higher-Order Logic |publisher=Elsevier |isbn=978-0-08-093067-1}}

==External links==
* Andrews, Peter B, [http://plato.stanford.edu/entries/type-theory-church/ Church's Type Theory] in [[Stanford Encyclopedia of Philosophy]].
* Miller, Dale, 1991, "[http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/encyclopedia.pdf Logic: Higher-order]," ''Encyclopedia of Artificial Intelligence'', 2nd ed.
* Herbert B. Enderton, [http://plato.stanford.edu/entries/logic-higher-order/ Second-order and Higher-order Logic] in [[Stanford Encyclopedia of Philosophy]], published Dec 20, 2007; substantive revision Mar 4, 2009.

{{Mathematical logic}}

[[Category:Predicate logic]]
[[Category:Systems of formal logic]]