Russell’s orders in Kripke’s Theory of Truth and Computational Type Theory

Fairouz Dib Kamareddine, Twan Laan, Robert Constable

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)


In Russell’s Ramified Theory of Types rtt as presented in Principia Mathematica
by Whitehead and Russell [1910, 1927], two hierarchical concepts dominate: orders
and types. The class of propositions over types is divided into different orders
where a propositional function can only depend on objects of lower orders. The
use of orders renders the logic part of rtt predicative. Ramsey [1926] and Hilbert
and Ackermann [1928] considered the orders to be too restrictive and therefore
removed them. This led to the development of Church’s Simple Type Theory stt
[1940] which uses types without orders. Since, numerous type systems abandoned
the hierarchy of orders. For example, all the eight influential Pure Type Systems
(PTSs) of the Barendregt cube [1992] avoid orders. Despite this lack of explicit
use of orders in some modern type systems, orders still play an influential role
in understanding hierarchy in modern type systems. In this chapter, we reflect
on the use of orders in providing an adequate foundation for basic concepts in
computer science and computational mathematics as expressed in Computational
Type Theory ctt [Constable et al., 1986; Allen et al., 2006] and in explaining the
truth levels in Kripke’s Theory of Truth ktt [Kripke, 1975].
Original languageEnglish
Title of host publicationHandbook of the History of Logic: Sets and Extensions in the Twentieth Century
EditorsDov Gabbay, Akihiro Kanamori, John Woods
Place of PublicationSan Diego
Number of pages44
ISBN (Print)978-0-444-51621-3
Publication statusPublished - 2012


Dive into the research topics of 'Russell’s orders in Kripke’s Theory of Truth and Computational Type Theory'. Together they form a unique fingerprint.

Cite this