Higher order logic in mathematics and logic is a form of predicate logic that differs from first order logic in additional quantifiers , as well as in stronger semantics . Higher-order logic with their standard semantics is more expressive, but their model-theoretical properties are less “good” compared to first-order logic.
First-order logic quantifies variables only; second-order logic also allows quantification over sets; third-order logic quantifies and sets of sets, and so on. For example, a second order sentence
expresses the principle of mathematical induction . Higher order logic is a combination of first, second, third logic, etc. orders; in other words, higher-order logic admits statements over sets of arbitrary embedding depth.
Examples and properties
Higher-order logic includes branches of the simple theory of types [1] of Church and various forms of the intuitionistic theory of types. Gerard Yue showed that the unification problem is algorithmically unsolvable in an intuitionistic variety of third-order logic [2] [3] [4] , that is, there is no algorithm that determines whether an arbitrary equation has a solution over third-order terms (and even more so arbitrary order higher than third).
Given the concept of isomorphism, the Boolean operation is defined in second-order logic. Using this observation, Hintikka established in 1955 that second order logic can simulate higher order logic in the sense that for each formula of higher order logic one can find a corresponding equally satisfiable second order logic formula [5] .
In some contexts, it is assumed that the concept of higher order logic refers to classical logic of a higher order. However, higher order modal logic has also been studied. According to some logical scientists, ontological evidence Gödel is best studied (from a technical point of view) in this context [6] .
See also
- First order logic
- Second order logic
- Higher Grammar
- Intuitionistic Type Theory
- Multi-Sorted Logic
- Typed lambda calculus
- Modal logic
Notes
- ↑ Church, Alonzo , A formulation of the simple theory of types , The Journal of Symbolic Logic 5 (2): 56–68 (1940)
- Et Huet, Gérard P. The Third Order of Logic (English) // Information and Control : journal. - 1973. - Vol. 22 , no. 3 - P. 257-267 . - DOI : 10.1016 / s0019-9958 (73) 90301-x .
- ↑ Huet, Gérard (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2, ... ω (Ph.D.). Universite de Paris VII.
- ↑ Huet, Gérard. Higher Order Unification 30 years later // Proceedings, 15th International Conference TPHOL . - Springer, 2002. - Vol. 2410. - P. 3–12.
- ↑ Stanford Philosophical Encyclopedia article on higher order logic
- ↑ Fitting, Melvin. Types, Tableaus, and Gödel's God. - Springer Science & Business Media, 2002. - p. 139. - "Godel's argument has been given," [...] [AG96] showed a third-order, but as a third-order. ” - ISBN 978-1-4020-0604-3 .
Literature
- Andrews, Peter B. (2002). Annotation: To the 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, PJ, 1986. Introduction to Higher Order Categorical Logic , Cambridge University Press, ISBN 0-521-35653-9
- Jacobs, Bart. Categorical Logic and Type Theory . - North Holland, Elsevier, 1999. - ISBN 0-444-50170-3 .
- Benzmuller, Christoph. Automation of Higher-Order Logic // Handbook of History of Logic, Volume 9: Computational Logic / Christoph Benzmuller, Dale Miller. - Elsevier, 2014. - ISBN 978-0-08-093067-1 .
Links
- Andrews, Peter B, Church's Type Theory in the 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 the Stanford Encyclopedia of Philosophy , published December 20, 2007; substantially revised March 4, 2009.