Review of Symbolic Logic:1-43 (forthcoming)

Tim Button
University College London
Robert Trueman
University of York
Standard Type Theory, ${\textrm {STT}}$, tells us that $b^n$ is well-formed iff $n=m+1$. However, Linnebo and Rayo [23] have advocated the use of Cumulative Type Theory, $\textrm {CTT}$, which has more relaxed type-restrictions: according to $\textrm {CTT}$, $b^\beta $ is well-formed iff $\beta>\alpha $. In this paper, we set ourselves against $\textrm {CTT}$. We begin our case by arguing against Linnebo and Rayo’s claim that $\textrm {CTT}$ sheds new philosophical light on set theory. We then argue that, while $\textrm {CTT}$ ’s type-restrictions are unjustifiable, the type-restrictions imposed by ${\textrm {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 $\textrm {CTT}$. We end by examining an alternative approach to cumulative types due to Florio and Jones [10]; we argue that their theory is best seen as a misleadingly formulated version of ${\textrm {STT}}$.
Keywords type theory  standard type theory  cumulative type theory
Categories (categorize this paper)
DOI 10.1017/s1755020321000435
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

 PhilArchive page | Other versions
Through your library

References found in this work BETA

Philosophy and Model Theory.Sean Walsh & Tim Button - 2018 - Oxford, UK: Oxford University Press.
Objects of Thought.Arthur Norman Prior - 1971 - Oxford, England: Clarendon Press.
Plural Logic.Alex Oliver & Timothy John Smiley - 2013 - Oxford, England: Oxford University Press UK.
Quality and Concept.George Bealer - 1982 - Oxford, England: Oxford University Press.

View all 43 references / Add more references

Citations of this work BETA

Higher‐Order Metaphysics.Lukas Skiba - 2021 - Philosophy Compass 16 (10):1-11.
Engineering Existence?Lukas Skiba - forthcoming - Inquiry: An Interdisciplinary Journal of Philosophy.

Add more citations

Similar books and articles

Naïve Type Theory.Thorsten Altenkirch - 2019 - In Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts. Springer Verlag. pp. 101-136.
Cumulative Versus Noncumulative Ramified Types.Anthony F. Peressini - 1997 - Notre Dame Journal of Formal Logic 38 (3):385-397.
Type-Theoretical Grammar.Aarne Ranta - 1994 - Oxford, England: Oxford University Press on Demand.
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
Well-Ordering Proofs for Martin-Löf Type Theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
Treatise on Intuitionistic Type Theory.Johan Georg Granström - 2011 - Dordrecht, Netherland: Springer.
Logic in the 1930s: Type Theory and Model Theory.Georg Schiemer & Erich H. Reck - 2013 - Bulletin of Symbolic Logic 19 (4):433-472.


Added to PP index

Total views
128 ( #92,350 of 2,518,158 )

Recent downloads (6 months)
48 ( #17,439 of 2,518,158 )

How can I increase my downloads?


My notes