A history of types

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

doi:10.1016/B978-0-444-52937-4.50009-5

A history of types

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

Research on miscellaneous topics in computing science, not included in one of the research schools

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic

1 Citation (Scopus)

Abstract

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.

Original language	English
Title of host publication	Logic: A History of its Central Concepts
Editors	D.M. Gabbay, F.J. Pelletier, J. Woods
Publisher	Elsevier
Pages	451-511
ISBN (Print)	978-0-444-52937-4
DOIs	https://doi.org/10.1016/B978-0-444-52937-4.50009-5
Publication status	Published - 2012

Publication series

Name	Handbook of the History of Logic
Volume	11

Access to Document

10.1016/B978-0-444-52937-4.50009-5

Fingerprint Dive into the research topics of 'A history of types'. Together they form a unique fingerprint.

Cite this

@inbook{b32781b67251424a8b76cb1b9779cbd2,

title = "A history of types",

abstract = "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.",

author = "F. Kamareddine and T.D.L. Laan and R.P. Nederpelt",

year = "2012",

doi = "10.1016/B978-0-444-52937-4.50009-5",

language = "English",

isbn = "978-0-444-52937-4",

series = "Handbook of the History of Logic",

publisher = "Elsevier",

pages = "451--511",

editor = "D.M. Gabbay and F.J. Pelletier and J. Woods",

booktitle = "Logic: A History of its Central Concepts",

address = "Netherlands",

}

TY - CHAP

T1 - A history of types

AU - Kamareddine, F.

AU - Laan, T.D.L.

AU - Nederpelt, R.P.

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

U2 - 10.1016/B978-0-444-52937-4.50009-5

DO - 10.1016/B978-0-444-52937-4.50009-5

M3 - Chapter

SN - 978-0-444-52937-4

T3 - Handbook of the History of Logic

SP - 451

EP - 511

BT - Logic: A History of its Central Concepts

A2 - Gabbay, D.M.

A2 - Pelletier, F.J.

A2 - Woods, J.

PB - Elsevier

ER -