Higher-order logic

Source: Wikipedia, the free encyclopedia.

In

quantifiers and, sometimes, 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.

The term "higher-order logic" is commonly used to mean higher-order simple predicate logic. Here "simple" indicates that the underlying

polymorphic and dependent types.[1]

Quantification scope

"Ordered logic" redirects here. For the unrelated term in linear logic, see 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-, ..., nth-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

ℵ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

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

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 third-order logic,[5][6][7][8]
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 equisatisfiable formula for it in second-order logic.[9]

The term "higher-order logic" is assumed in some context to refer to classical higher-order logic. However, 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.[10]

See also

Notes

  1. ^ Jacobs, 1999, chapter 5
  2. ^ Shapiro 1991, p. 87.
  3. ^ 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.
  4. The Journal of Symbolic Logic
    5(2):56–68 (1940)
  5. doi:10.1016/s0019-9958(73)90301-x
    .
  6. ^ Huet, Gérard (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.) (in French). Universite de Paris VII.
  7. ^ Warren D. Goldfarb (1981). "The Undecidability of the Second-Order Unification Problem" (PDF). Theoretical Computer Science. 13: 225–230.
  8. ^ Huet, Gérard (2002). "Higher Order Unification 30 years later" (PDF). In Carreño, V.; Muñoz, C.; Tahar, S. (eds.). Proceedings, 15th International Conference TPHOL. LNCS. Vol. 2410. Springer. pp. 3–12.
  9. ^ entry on HOL
  10. ISBN 978-1-4020-0604-3
    . 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.

References

External links
Retrieved from "https://en.wikipedia.org/w/index.php?title=Higher-order_logic&oldid=1188430002"