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 theory 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.
Read more about this topic: Higher-order Logic
Famous quotes containing the words simple, predicate and/or logic:
“The prostitute is the scapegoat for everyone’s sins, and few people care whether she is justly treated or not. Good people have spent thousands of pounds in efforts to reform her, poets have written about her, essayists and orators have made her the subject of some of their most striking rhetoric; perhaps no class of people has been so much abused, and alternatively sentimentalized over as prostitutes have been but one thing they have never yet had, and that is simple legal justice.”
—Alison Neilans. “Justice for the Prostitute—Lady Astor’s Bill,” Equal Rights (September 19, 1925)
“The only thing that one really knows about human nature is that it changes. Change is the one quality we can predicate of it. The systems that fail are those that rely on the permanency of human nature, and not on its growth and development. The error of Louis XIV was that he thought human nature would always be the same. The result of his error was the French Revolution. It was an admirable result.”
—Oscar Wilde (1854–1900)
““... We need the interruption of the night
To ease attention off when overtight,
To break our logic in too long a flight,
And ask us if our premises are right.””
—Robert Frost (1874–1963)