HOME

TheInfoList



OR:

In
mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
and
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from prem ...
, a higher-order logic is a form of
predicate logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
that is distinguished from
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
by additional quantifiers and, sometimes, stronger
semantics Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and comput ...
. 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. 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 In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a founda ...
is the ''theory of simple types'', also called the ''simple theory of types'' (see
Type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a founda ...
). Leon Chwistek and Frank P. Ramsey proposed this as a simplification of the complicated and clumsy ''ramified theory of types'' specified in the ''
Principia Mathematica The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. ...
'' by
Alfred North Whitehead Alfred North Whitehead (15 February 1861 – 30 December 1947) was an English mathematician and philosopher. He is best known as the defining figure of the philosophical school known as process philosophy, which today has found applica ...
and
Bertrand Russell Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British mathematician, philosopher, logician, and public intellectual. He had a considerable influence on mathematics, logic, set theory, linguistics, a ...
. ''Simple types'' is nowadays sometimes also meant to exclude polymorphic and dependent types.


Quantification scope

First-order logic quantifies only variables that range over individuals; ''
second-order logic In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...
'', in addition, also quantifies over sets; ''third-order logic'' also quantifies over sets of sets, and so on. ''Higher-order logic'' is the union of first-, second-, third-, ..., ''n''th-order logic; ''i.e.,'' higher-order logic admits quantification over sets that are nested arbitrarily deeply.


Semantics

There are two possible semantics for higher-order logic. 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 In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is post ...
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 number In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called '' cardinal ...
s, and of the
real number In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every ...
s, which are impossible with first-order logic. However, by a result of
Kurt Gödel Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imm ...
, HOL with standard semantics does not admit an effective, sound, and
complete Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...
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 In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...
is already larger than the first
measurable cardinal In mathematics, a measurable cardinal is a certain kind of large cardinal number. In order to define the concept, one introduces a two-valued measure on a cardinal , or more generally on any set. For a cardinal , it can be described as a subdivisi ...
, 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 In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is post ...
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.


Properties

Higher order logics include the offshoots of
Church Church may refer to: Religion * Church (building), a building for Christian religious activities * Church (congregation), a local congregation of a Christian denomination * Church service, a formalized period of Christian communal worship * Chri ...
's simple theory of types
Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scien ...

''A formulation of the simple theory of types''
The Journal of Symbolic Logic 5(2):56–68 (1940)
and the various forms of
intuitionistic type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...
. Gérard Huet has shown that unifiability is undecidable in a type-theoretic flavor of third-order logic, that is, there can be no algorithm to decide whether an arbitrary equation between third-order (let alone arbitrary higher-order) terms has a solution. Up to a certain notion of isomorphism, the powerset operation is definable in second-order logic. Using this observation,
Jaakko Hintikka Kaarlo Jaakko Juhani Hintikka (12 January 1929 – 12 August 2015) was a Finnish philosopher and logician. Life and career Hintikka was born in Helsingin maalaiskunta (now Vantaa). In 1953, he received his doctorate from the University of Hel ...
established in 1955 that second-order logic can simulate higher-order logics in the sense that for every formula of a higher order-logic, one can find an equisatisfiable formula for it in second-order logic.entry on HOL
/ref> The term "higher-order logic" is assumed in some context to refer to '' classical'' higher-order logic. However, modal higher-order logic has been studied as well. According to several logicians, Gödel's ontological proof is best studied (from a technical perspective) in such a context.


See also

*
Zeroth-order logic Zeroth-order logic is first-order logic without variables or quantifiers. Some authors use the phrase "zeroth-order logic" as a synonym for the propositional calculus,. but an alternative definition extends propositional logic by adding constant ...
(propositional logic) *
First-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
*
Second-order logic In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...
*
Type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a founda ...
*
Higher-order grammar Higher order grammar (HOG) is a grammar theory based on higher-order logic.Hana, JiriCzech Clitics in Higher Order Grammar Diss. The Ohio State University, 2007. It can be viewed simultaneously as generative-enumerative (like categorial grammar and ...
* Higher-order logic programming * HOL (proof assistant) *
Many-sorted logic Many-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. Both functional and assertive "parts of speech" ...
*
Typed lambda calculus A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) 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 ...
*
Modal logic Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend ot ...


Notes


References

* Andrews, Peter B. (2002). ''An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof'', 2nd ed, Kluwer Academic Publishers, * 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, * *


External links

* Andrews, Peter B
Church's Type Theory
in
Stanford Encyclopedia of Philosophy The ''Stanford Encyclopedia of Philosophy'' (''SEP'') combines an online encyclopedia of philosophy with peer-reviewed publication of original papers in philosophy, freely accessible to Internet users. It is maintained by Stanford University. E ...
. * 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 Philosophy The ''Stanford Encyclopedia of Philosophy'' (''SEP'') combines an online encyclopedia of philosophy with peer-reviewed publication of original papers in philosophy, freely accessible to Internet users. It is maintained by Stanford University. E ...
, published Dec 20, 2007; substantive revision Mar 4, 2009. {{Mathematical logic Predicate logic Systems of formal logic