A history of types

F. Kamareddine, T.D.L. Laan, R.P. Nederpelt

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureHoofdstukAcademic

1 Citaat (Scopus)


In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([Whitehead and Russell, 1910], 1910–1912) and Church's simply typed ¿-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's Grundgesetze der Arithmetik for which Russell applied his famous paradox1 and this led him to introduce the first theory of types, the Ramified Type Theory (rtt). We present RTT formally using the modern notation for type theory and we discuss how Ramsey, Hilbert and Ackermann removed the orders from RTT leading to the simple theory of types STT. We present STT and Church's own simply typed ¿-calculus (¿¿C2) and we finish by comparing RTT, STT and ¿¿C.
Originele taal-2Engels
TitelLogic: A History of its Central Concepts
RedacteurenD.M. Gabbay, F.J. Pelletier, J. Woods
ISBN van geprinte versie978-0-444-52937-4
StatusGepubliceerd - 2012

Publicatie series

NaamHandbook of the History of Logic

Vingerafdruk Duik in de onderzoeksthema's van 'A history of types'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Kamareddine, F., Laan, T. D. L., & Nederpelt, R. P. (2012). A history of types. In D. M. Gabbay, F. J. Pelletier, & J. Woods (editors), Logic: A History of its Central Concepts (blz. 451-511). (Handbook of the History of Logic; Vol. 11). Elsevier. https://doi.org/10.1016/B978-0-444-52937-4.50009-5