Higher-order logic
Encyclopedia
In mathematics
and logic
, a higher-order logic is a form of predicate logic
that is distinguished from first-order logic
by additional quantifiers and a 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.
is simple, not polymorphic
or dependent
.
There are two possible semantics for HOL. 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 powerset of the set of individuals. Thus, in standard semantics, once the set of individuals is specified, this is enough to specify all the quantifiers.
HOL with standard semantics is more expressive than first-order logic. For example, HOL admits categorical axiomatizations of the natural numbers, and of the real numbers, which are impossible with first-order logic. However, by a result of Gödel
, HOL with standard semantics does not admit an effective, sound and complete
proof calculus
.
The model-theoretic properties of HOL with standard semantics are also more complex than those of first-order logic. For example, the Löwenheim number
of second-order logic is already larger than the first measurable cardinal
, if such a cardinal exists. The Löwenheim number of first-order logic, in contrast, is ℵ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 powerset of the set of individuals. HOL with these semantics is equivalent to 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.
's Simple Theory of Types
, Thierry Coquand
's calculus of constructions
, which allows for both dependent and polymorphic types.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
and logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, a higher-order logic is a form of predicate logic
Predicate logic
In mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic or infinitary logic. This formal system is distinguished from other systems in that its formulae contain variables which can be quantified...
that is distinguished from first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
by additional quantifiers and a 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.
Higher-order simple predicate logic
The term "higher-order logic", abbreviated as HOL, is commonly used to mean higher order simple predicate logic. Here "simple" indicates that the underlying type theoryType theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
is simple, not polymorphic
Type polymorphism
In computer science, polymorphism is a programming language feature that allows values of different data types to be handled using a uniform interface. The concept of parametric polymorphism applies to both data types and functions...
or dependent
Dependent type
In computer science and logic, a dependent type is a type that depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like ATS, Agda and Epigram....
.
There are two possible semantics for HOL. 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 powerset of the set of individuals. Thus, in standard semantics, once the set of individuals is specified, this is enough to specify all the quantifiers.
HOL with standard semantics is more expressive than first-order logic. For example, HOL admits categorical axiomatizations of the natural numbers, and of the real numbers, which are impossible with first-order logic. However, by a result of Gödel
Godel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*Gödel...
, HOL with standard semantics does not admit an effective, sound and complete
Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
proof calculus
Proof calculus
In mathematical logic, a proof calculus corresponds to a family of formal systems that use a common style of formal inference for its inference rules...
.
The model-theoretic properties of HOL with standard semantics are also more complex than those of first-order logic. For example, the Löwenheim number
Löwenheim number
In mathematical logic the Löwenheim number of an abstract logic is the smallest cardinal number for which a weak downward Löwenheim–Skolem theorem holds...
of second-order logic is already larger than the first measurable cardinal
Measurable cardinal
- Measurable :Formally, a measurable cardinal is an uncountable cardinal number κ such that there exists a κ-additive, non-trivial, 0-1-valued measure on the power set of κ...
, if such a cardinal exists. The Löwenheim number of first-order logic, in contrast, is ℵ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 powerset of the set of individuals. HOL with these semantics is equivalent to 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.
Examples
Examples of higher order logics include HOL, ChurchAlonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...
's Simple Theory of Types
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a typed lambda calculus...
, Thierry Coquand
Thierry Coquand
Thierry Coquand is a professor in computer science at the University of Gothenburg, Sweden. He is known for his work in constructive mathematics, especially the calculus of constructions. He received his Ph.D. under the supervision of Gérard Huet.- External links :*...
's calculus of constructions
Calculus of constructions
The calculus of constructions is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.-General traits:The CoC is a...
, which allows for both dependent and polymorphic types.
Criticism
Quine has criticized higher-order logic (with standard semantics) as "set theory in sheep's clothing". Quine's criticism focuses on the lack of an effective, sound, complete proof theory; he argues that this makes HOL not a "logic". Shapiro has responded to this criticism, arguing that the additional semantic expressiveness can offset the lack of a proof theory, and arguing that a "logic" need only have a deductive system or a semantical system, but perhaps may not have both.See also
- Higher-order grammarHigher-order grammarHigher Order grammar is a grammar theory based on higher-order logic. It can be viewed simultaneously as generative-enumerative or model theoretic .-Key features:* There is a propositional logic of types, which denote sets of linguistic...
- Typed lambda calculusTyped lambda calculusA typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
- Intuitionistic Type TheoryIntuitionistic type theoryIntuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
- Many-sorted logicMany-sorted logicMany-sorted logic can reflect formally our intention, not to handle the universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming...
External links
- Miller, Dale, 1991, "Logic: Higher-order," Encyclopedia of Artificial Intelligence, 2nd ed.
- Herbert B. Enderton, Second-order and Higher-order Logic in Stanford Encyclopedia of PhilosophyStanford Encyclopedia of PhilosophyThe Stanford Encyclopedia of Philosophy is a freely-accessible online encyclopedia of philosophy maintained by Stanford University. Each entry is written and maintained by an expert in the field, including professors from over 65 academic institutions worldwide...
, published Dec 20, 2007; substantive revision Mar 4, 2009.