Higher level logic

from Wikipedia, the free encyclopedia

Under Logic higher level ( English Higher-Order Logic , HOL ), also stage logic , understood as an extension of first-order logic . It is based on the typified lambda calculus and goes back to Alonzo Church's Theory of Simple Types .

Developed around 1940 as an attempt to formalize logic in the Principia Mathematica by Whitehead and Russell , it has been extensively studied by Leon Henkin and Peter Andrews . In the early 1970s, non-classical versions of higher-level logic were developed that form the basis of modern type theory ( Per Martin-Löf , Jean-Yves Girard ) and proof theory (Jean-Yves Girard, Gérard Huet , Robert Harper , Furio Honsell ) . Since higher-level logic is both powerful and relatively easy to implement on a computer , some theorem provers for it have recently been developed that are of interest to both mathematics and computer science .

See also

literature

  • Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof . Academic Press, 1986.
  • J. Lambek, PJ Scott: Introduction To Higher Order Categorical Logic , Cambridge University Press, Cambridge, UK, 1986. Online ( Memento from July 5, 2007 in the Internet Archive )

Web links