Against Cumulative Type Theory

Rob Trueman, Tim Button

Research output: Contribution to journalArticlepeer-review


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 languageEnglish
Number of pages43
JournalThe Review of Symbolic Logic
Early online date2 Sept 2021
Publication statusE-pub ahead of print - 2 Sept 2021

Bibliographical note

© The Author(s), 2021. Published by Cambridge University Press on behalf of Association for Symbolic Logic

Cite this