Editing Higher-order logic (section)

== 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>