|
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 calculus of constructions.
See also Literature | ||||||||
|
| |||||||||
 |
|
| |