Types in logic and mathematics before 1940

Fairouz Kamareddine, Twan Laan, Rob Nederpelt

Research output: Contribution to journalArticle

Abstract

In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 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 paradox 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 languageEnglish
Pages (from-to)185-245
Number of pages61
JournalBulletin of Symbolic Logic
Volume8
Issue number2
Publication statusPublished - 2002

Fingerprint

Mathematics
Logic
Calculi
Gottlob Frege
David Hilbert
Prehistory
Logical Paradoxes
Notation
Principia
Paradox

Cite this

Kamareddine, Fairouz ; Laan, Twan ; Nederpelt, Rob. / Types in logic and mathematics before 1940. In: Bulletin of Symbolic Logic. 2002 ; Vol. 8, No. 2. pp. 185-245.
@article{18c1dc3bf36d4ee6af5de03f279afb99,
title = "Types in logic and mathematics before 1940",
abstract = "In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 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 paradox 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 = "Fairouz Kamareddine and Twan Laan and Rob Nederpelt",
year = "2002",
language = "English",
volume = "8",
pages = "185--245",
journal = "Bulletin of Symbolic Logic",
issn = "1079-8986",
publisher = "Association for Symbolic Logic",
number = "2",

}

Kamareddine, F, Laan, T & Nederpelt, R 2002, 'Types in logic and mathematics before 1940', Bulletin of Symbolic Logic, vol. 8, no. 2, pp. 185-245.

Types in logic and mathematics before 1940. / Kamareddine, Fairouz; Laan, Twan; Nederpelt, Rob.

In: Bulletin of Symbolic Logic, Vol. 8, No. 2, 2002, p. 185-245.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Types in logic and mathematics before 1940

AU - Kamareddine, Fairouz

AU - Laan, Twan

AU - Nederpelt, Rob

PY - 2002

Y1 - 2002

N2 - In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 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 paradox 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 ([71], 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 paradox 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.

UR - http://www.scopus.com/inward/record.url?scp=0036017444&partnerID=8YFLogxK

M3 - Article

VL - 8

SP - 185

EP - 245

JO - Bulletin of Symbolic Logic

JF - Bulletin of Symbolic Logic

SN - 1079-8986

IS - 2

ER -