Higher-order logic

Higher-order logic

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 Church's "Simple Theory of Types" and
calculus of constructions.

See also

*Higher-order grammar
*Typed lambda calculus
*Intuitionistic Type Theory
*Many-sorted logic

External links

* Miller, Dale, 1991, " [http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/AIencyclopedia/ Logic: Higher-order,] " "Encyclopedia of Artificial Intelligence", 2nd ed.

References

* Andrews, P.B., 2002. "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof", 2nd ed. Kluwer Academic Publishers, available from Springer.
* Church, Alonzo, 1940, "A Formulation of the Simple Theory of Types," "Journal of Symbolic Logic 5": 56-68.
* Henkin, Leon, 1950, "Completeness in the Theory of Types," "Journal of Symbolic Logic 15": 81-91.
*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.


Wikimedia Foundation. 2010.

Игры ⚽ Нужен реферат?

Look at other dictionaries:

  • higher-order logic — One in which the variables of the quantifiers are permitted to range over properties and functions as well as individuals (see also first order language ) …   Philosophy dictionary

  • Higher order grammar — (HOG) is a grammar theory based on higher order logic. It can be viewed simultaneously as generative enumerative (like Categorial Grammar and Principles Parameters) or model theoretic (like Head Driven Phrase Structure Grammar or Lexical… …   Wikipedia

  • 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 (a less… …   Wikipedia

  • 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.[1] Second order logic is in turn extended by higher order logic and type theory. First order logic uses only… …   Wikipedia

  • Higher-order abstract syntax — In computer science, higher order abstract syntax (abbreviated HOAS) is a technique for the representation of abstract syntax trees for languages with variable binders.Relation to first order abstract syntaxAn abstract syntax tree is abstract… …   Wikipedia

  • Higher-order function — In mathematics and computer science, higher order functions or functionals are functions which do at least one of the following: *take one or more functions as an input *output a function.In mathematics these are also known as operators or… …   Wikipedia

  • Theorem Proving in Higher-Order Logics — (TPHOLs) is an annual international academic conference on the topic of automated reasoning in higher order logics. The first TPHOLs was held in Cambridge, UK in 1987, but in the early years was an informal gathering of researchers interested in… …   Wikipedia

  • Logic programming — is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy s [1958] advice taker proposal, logic is used as a purely declarative… …   Wikipedia

  • Logic in computer science — describes topics where logic is applied to computer science and artificial intelligence. These include:*Investigations into logic that are guided by applications in computer science. For example: Combinatory logic and Abstract interpretation;… …   Wikipedia

  • Logic (disambiguation) — Logic is the study of the principles and criteria of valid inference and demonstration.Logic may also refer to:In logic and mathematics*A branch of logic: **Inductive logic, also called induction or inductive reasoning **Informal logic, the study …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”