العربية
中国
Français
Deutsch
Ελληνική
हिन्दी
Italiano
日本語
Português
Русский
EspañolHIGHER-ORDER LOGIC
In mathematics, 'higher-order logic' is distinguished from first-order logic in a number of ways.
One of these is the type of variables appearing in quantifications; in first-order logic, roughly speaking, it is forbidden to quantify over predicates. See second-order logic for systems in which this is permitted.
Another way in which higher-order logic differs from first-order logic is in the constructions allowed in the underlying type theory. A 'higher-order predicate' is a predicate that takes one or more other predicates as arguments. In general, a higher-order predicate of order ''n'' takes one or more (''n'' − 1)th-order predicates as arguments, where ''n'' > 1. A similar remark holds for 'higher-order functions.'
Higher-order logics are more expressive, but their properties, in particular with respect to model theory, make them less well-behaved for many applications. By a result of Gödel, classical higher-order logic does not admit a (recursively axiomatized) sound and complete proof calculus; however, such a proof calculus does exist which is sound and complete with respect to Henkin models.
Examples of higher order logics include the Church's ''Simple Theory of Types'' and
calculus of constructions.
★ Higher-order grammar
★ Typed lambda calculus
★ Intuitionistic Type Theory
★ Many-sorted logic
★ Miller, Dale, 1991, "Logic: Higher-order," ''Encyclopedia of Artificial Intelligence'', 2nd ed.
★ Andrews, P.B., 2002. ''An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof'', 2nd ed. Kluwer Academic Publishers, available from Springer.
★ Church, Alonzo, 1940, "A Formulation of the Simple Theory of Types," ''Journal of Symbolic Logic 5'': 56-68.
★ Henkin, Leon, 1950, "Completeness in the Theory of Types," ''Journal of Symbolic Logic 15'': 81-91.
★ Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press.
★ Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., ''The Blackwell Guide to Philosophical Logic''. Blackwell.
★ Lambek, J. and Scott, P. J., 1986. ''Introduction to Higher Order Categorical Logic'', Cambridge University Press.
One of these is the type of variables appearing in quantifications; in first-order logic, roughly speaking, it is forbidden to quantify over predicates. See second-order logic for systems in which this is permitted.
Another way in which higher-order logic differs from first-order logic is in the constructions allowed in the underlying type theory. A 'higher-order predicate' is a predicate that takes one or more other predicates as arguments. In general, a higher-order predicate of order ''n'' takes one or more (''n'' − 1)th-order predicates as arguments, where ''n'' > 1. A similar remark holds for 'higher-order functions.'
Higher-order logics are more expressive, but their properties, in particular with respect to model theory, make them less well-behaved for many applications. By a result of Gödel, classical higher-order logic does not admit a (recursively axiomatized) sound and complete proof calculus; however, such a proof calculus does exist which is sound and complete with respect to Henkin models.
Examples of higher order logics include the Church's ''Simple Theory of Types'' and
calculus of constructions.
| Contents |
| See also |
| External links |
| References |
See also
★ Higher-order grammar
★ Typed lambda calculus
★ Intuitionistic Type Theory
★ Many-sorted logic
External links
★ Miller, Dale, 1991, "Logic: Higher-order," ''Encyclopedia of Artificial Intelligence'', 2nd ed.
References
★ Andrews, P.B., 2002. ''An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof'', 2nd ed. Kluwer Academic Publishers, available from Springer.
★ Church, Alonzo, 1940, "A Formulation of the Simple Theory of Types," ''Journal of Symbolic Logic 5'': 56-68.
★ Henkin, Leon, 1950, "Completeness in the Theory of Types," ''Journal of Symbolic Logic 15'': 81-91.
★ Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press.
★ Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., ''The Blackwell Guide to Philosophical Logic''. Blackwell.
★ Lambek, J. and Scott, P. J., 1986. ''Introduction to Higher Order Categorical Logic'', Cambridge University Press.
This article provided by Wikipedia. To edit the contents of this article, click here for original source.
psst.. try this: add to faves
