Simple type theory, or Higher-order Logic (HOL)

Simple type theory (STT) is a system of classical higher-order logic. It is often referred to by other names, including

• Church's type theory
• Church's theory of types
• Higher-order logic (HOL)

and so on.

At its heart, STT consists of

• the simply-typed \lambda-calculus with function types, and
• at least two basic types, usually named \iota and \omicron, equipped with
• some constants.

The idea is that \iota is the type of data (e.g. natural numbers), whereas \omicron is the type of propositions.

The constants themselves contain all the usual logical connectives as functions from propositions to propositions, e.g.

  \land : \omicron \to \omicron \to \omicron \qquad\qquad
  \lnot  : \omicron \to \omicron

Predicates and quantifiers

Many familiar constructions from logic can be given types in STT. For example, a term M : \iota \to \omicron 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

  \forall_{\iota} : (\iota \to \omicron) \to \omicron

that turns a predicate into a proposition. In first-order logic, we essentially only have such a constant for type \iota. But in STT/HOL we have a constant \forall_\sigma for any type \sigma, which allows higher-order quantification.

Implementations

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:

• HOL Light

References

• Stanford Encyclopedia of Philosophy: Church's type theory.

• Wikipedia: Higher-order logic

• A textbook treatment can be found in:

@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},
}

• STT/HOL originated in

@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}
}