Simple type theory (STT) is a system of classical higher-order logic. It is often referred to by other names, including
and so on.
At its heart, STT consists of
The idea is that is the type of data (e.g. natural numbers), whereas is the type of propositions.
The constants themselves contain all the usual logical connectives as functions from propositions to propositions, e.g.
Many familiar constructions from logic can be given types in STT. For example, a term is really a predicate: it is a function which, given a data value, returns a proposition with a truth value.
Similarly, we can quantify over a predicate by applying a constant
that turns a predicate into a proposition. In first-order logic, we essentially only have such a constant for type . But in STT/HOL we have a constant for any type , which allows higher-order quantification.
Perhaps the most widely-used proof assistant based on STT/HOL is Isabelle/HOL, i.e. the Isabelle proof assistant coupled with the HOL core.
Other proof assistants include:
Stanford Encyclopedia of Philosophy: Church's type theory.
Wikipedia: Higher-order logic
A textbook treatment can be found in:
Andrews, Peter B. 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Vol. 27. Applied Logic Series. Dordrecht: Springer Netherlands. https://doi.org/10.1007/978-94-015-9934-4.
@book{andrews_2002,
address = {Dordrecht},
series = {Applied {Logic} {Series}},
title = {An {Introduction} to {Mathematical} {Logic} and {Type} {Theory}: {To} {Truth} {Through} {Proof}},
volume = {27},
isbn = {978-90-481-6079-2 978-94-015-9934-4},
shorttitle = {An {Introduction} to {Mathematical} {Logic} and {Type} {Theory}},
publisher = {Springer Netherlands},
author = {Andrews, Peter B.},
editor = {Gabbay, Dov M. and Barwise, Jon},
year = {2002},
doi = {10.1007/978-94-015-9934-4},
}
Church, Alonzo. 1940. ‘A Formulation of the Simple Theory of Types’. The Journal of Symbolic Logic 5 (02): 56–68. https://doi.org/10.2307/2266170.
@article{church_1940,
title = {A formulation of the simple theory of types},
volume = {5},
url = {www.jstor.org/stable/2266170},
doi = {10.2307/2266170},
number = {02},
journal = {The Journal of Symbolic Logic},
author = {Church, Alonzo},
year = {1940},
pages = {56--68}
}