Higher-order logic
From Free net encyclopedia
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.
See also
External links
Literature
- Andrews, P.B., An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edition, Academic Press, New York, NY, 2002.
- Church, A., "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic, vol. 5, 1940, pp. 56-68.
- Henkin, L., "Completeness in the Theory of Types", Journal of Symbolic Logic, vol. 15, 1950, pp. 81-91.
- Lambek, J. and Scott, P.J., Introduction to Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK, 1986.
