## 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] and in explaining the

truth levels in Kripke’s Theory of Truth ktt [Kripke, 1975].

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 language | English |
---|---|

Title of host publication | Handbook of the History of Logic: Sets and Extensions in the Twentieth Century |

Editors | Dov Gabbay, Akihiro Kanamori, John Woods |

Place of Publication | San Diego |

Publisher | Elsevier |

Pages | 801-845 |

Number of pages | 44 |

Volume | 6 |

ISBN (Print) | 978-0-444-51621-3 |

Publication status | Published - 2012 |