# * Russell's Orders in Kripke's Theory of Truth and Computational Type Theory *

## by Robert L. Constable, Fairouz Kamareddine, Twan Laan

2012

Published in *Handbook of the History of Logic: Sets and Extensions in the Twentieth Century*. Vol. 6

available online

**Abstract**

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; Kamareddine and Laan, 2001] and in explaining the truth levels in Kripke’s Theory of Truth KTT [Kripke, 1975; Kamareddine and Laan, 2001].

**bibTex ref: KLC12**

cite link