Against Cumulative Type Theory

Rob Trueman; Tim Button

doi:10.1017/S1755020321000435

Against Cumulative Type Theory

Rob Trueman, Tim Button

Philosophy

Research output: Contribution to journal › Article › peer-review

Abstract

Standard Type Theory, STT , tells us that b^n(a^m) is well-formed iff n=m+1 . However, Linnebo and Rayo have advocated the use of Cumulative Type Theory, CTT , which has more relaxed type-restrictions: according to CTT , b^β(a^α) is well-formed iff β>α . In this paper, we set ourselves against CTT . We begin our case by arguing against Linnebo and Rayo’s claim that CTT sheds new philosophical light on set theory. We then argue that, while CTT ’s type-restrictions are unjustifiable, the type-restrictions imposed by STT are justified by a Fregean semantics. What is more, this Fregean semantics provides us with a principled way to resist Linnebo and Rayo’s Semantic Argument for CTT . We end by examining an alternative approach to cumulative types due to Florio and Jones; we argue that their theory is best seen as a misleadingly formulated version of STT .

Original language	English
Number of pages	43
Journal	The Review of Symbolic Logic
Early online date	2 Sept 2021
DOIs	https://doi.org/10.1017/S1755020321000435
Publication status	E-pub ahead of print - 2 Sept 2021

Bibliographical note

Access to Document

10.1017/S1755020321000435Licence: CC BY

against-cumulative-type-theory
© The Author(s), 2021. Published by Cambridge University Press on behalf of Association for Symbolic Logic
Final published version, 608 KBLicence: CC BY

Cite this

@article{301ae326de894e6d90c7a49e0a379fda,

title = "Against Cumulative Type Theory",

abstract = "Standard Type Theory, STT , tells us that b^n(a^m) is well-formed iff n=m+1 . However, Linnebo and Rayo have advocated the use of Cumulative Type Theory, CTT , which has more relaxed type-restrictions: according to CTT , b^β(a^α) is well-formed iff β>α . In this paper, we set ourselves against CTT . We begin our case by arguing against Linnebo and Rayo{\textquoteright}s claim that CTT sheds new philosophical light on set theory. We then argue that, while CTT {\textquoteright}s type-restrictions are unjustifiable, the type-restrictions imposed by STT are justified by a Fregean semantics. What is more, this Fregean semantics provides us with a principled way to resist Linnebo and Rayo{\textquoteright}s Semantic Argument for CTT . We end by examining an alternative approach to cumulative types due to Florio and Jones; we argue that their theory is best seen as a misleadingly formulated version of STT .",

author = "Rob Trueman and Tim Button",

note = "{\textcopyright} The Author(s), 2021. Published by Cambridge University Press on behalf of Association for Symbolic Logic",

year = "2021",

month = sep,

day = "2",

doi = "10.1017/S1755020321000435",

language = "English",

journal = "The Review of Symbolic Logic",

issn = "1755-0203",

publisher = "Cambridge University Press",

}

TY - JOUR

T1 - Against Cumulative Type Theory

AU - Trueman, Rob

AU - Button, Tim

PY - 2021/9/2

Y1 - 2021/9/2

N2 - Standard Type Theory, STT , tells us that b^n(a^m) is well-formed iff n=m+1 . However, Linnebo and Rayo have advocated the use of Cumulative Type Theory, CTT , which has more relaxed type-restrictions: according to CTT , b^β(a^α) is well-formed iff β>α . In this paper, we set ourselves against CTT . We begin our case by arguing against Linnebo and Rayo’s claim that CTT sheds new philosophical light on set theory. We then argue that, while CTT ’s type-restrictions are unjustifiable, the type-restrictions imposed by STT are justified by a Fregean semantics. What is more, this Fregean semantics provides us with a principled way to resist Linnebo and Rayo’s Semantic Argument for CTT . We end by examining an alternative approach to cumulative types due to Florio and Jones; we argue that their theory is best seen as a misleadingly formulated version of STT .

AB - Standard Type Theory, STT , tells us that b^n(a^m) is well-formed iff n=m+1 . However, Linnebo and Rayo have advocated the use of Cumulative Type Theory, CTT , which has more relaxed type-restrictions: according to CTT , b^β(a^α) is well-formed iff β>α . In this paper, we set ourselves against CTT . We begin our case by arguing against Linnebo and Rayo’s claim that CTT sheds new philosophical light on set theory. We then argue that, while CTT ’s type-restrictions are unjustifiable, the type-restrictions imposed by STT are justified by a Fregean semantics. What is more, this Fregean semantics provides us with a principled way to resist Linnebo and Rayo’s Semantic Argument for CTT . We end by examining an alternative approach to cumulative types due to Florio and Jones; we argue that their theory is best seen as a misleadingly formulated version of STT .

U2 - 10.1017/S1755020321000435

DO - 10.1017/S1755020321000435

M3 - Article

SN - 1755-0203

JO - The Review of Symbolic Logic

JF - The Review of Symbolic Logic

ER -