Article (Scientific journals)
Church's Type Theory
Benzmüller, Christoph; Andrews, Peter
2019In Stanford Encyclopedia of Philosophy, p. 1--62
Peer reviewed


Full Text
Publisher postprint (1.48 MB)
Request a copy

All documents in ORBilu are protected by a user license.

Send to


Keywords :
Type Theory; Higher-Order Logic; Automated Reasoning
Abstract :
[en] Church’s type theory, aka simple type theory, is a formal logical language which includes classical first-order and propositional logic, but is more expressive in a practical sense. It is used, with some modifications and enhancements, in most modern applications of type theory. It is particularly well suited to the formalization of mathematics and other disciplines and to specifying and verifying hardware and software. It also plays an important role in the study of the formal semantics of natural language. When utilizing it as a meta-logic to semantically embed expressive (quantified) non-classical logics further topical applications are enabled in artificial intelligence and philosophy. A great wealth of technical knowledge can be expressed very naturally in it. With possible enhancements, Church’s type theory constitutes an excellent formal language for representing the knowledge in automated information systems, sophisticated automated reasoning systems, systems for verifying the correctness of mathematical proofs, and a range of projects involving logic and artificial intelligence. Some examples and further references are given in Sections 1.2.2 and 5 below. Type theories are also called higher-order logics, since they allow quantification not only over individual variables (as in first-order logic), but also over function, predicate, and even higher order variables. Type theories characteristically assign types to entities, distinguishing, for example, between numbers, sets of numbers, functions from numbers to sets of numbers, and sets of such functions. As illustrated in Section 1.2.2 below, these distinctions allow one to discuss the conceptually rich world of sets and functions without encountering the paradoxes of naive set theory. Church’s type theory is a formulation of type theory that was introduced by Alonzo Church in Church 1940. In certain respects, it is simpler and more general than the type theory introduced by Bertrand Russell in Russell 1908 and Whitehead & Russell 1927a. Since properties and relations can be regarded as functions from entities to truth values, the concept of a function is taken as primitive in Church’s type theory, and the λ-notation which Church introduced in Church 1932 and Church 1941 is incorporated into the formal language. Moreover, quantifiers and description operators are introduced in a way so that additional binding mechanisms can be avoided, λ-notation is reused instead. λ-notation is thus the only binding mechanism employed in Church’s type theory.
Disciplines :
Philosophy & ethics
Computer science
Author, co-author :
Benzmüller, Christoph ;  University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Andrews, Peter;  Carnegie Mellon University > Mathematics
External co-authors :
Language :
Title :
Church's Type Theory
Publication date :
21 May 2019
Journal title :
Stanford Encyclopedia of Philosophy
Publisher :
Stanford University, United States
Pages :
1--62 (in pdf version)
Peer reviewed :
Peer reviewed
Focus Area :
Computational Sciences
Available on ORBilu :
since 27 September 2019


Number of views
199 (0 by Unilu)
Number of downloads
0 (0 by Unilu)


Similar publications

Contact ORBilu