Against Cumulative Type Theory

Review of Symbolic Logic 15 (4):907-49 (2022)
  Copy   BIBTEX

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

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.
Logic in the 1930s: type theory and model theory.Georg Schiemer & Erich H. Reck - 2013 - Bulletin of Symbolic Logic 19 (4):433-472.

Analytics

Added to PP
2021-08-27

Downloads
387 (#40,019)

6 months
109 (#18,008)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Tim Button
University College London
Robert Trueman
University of York

Citations of this work

Higher‐order metaphysics.Lukas Skiba - 2021 - Philosophy Compass 16 (10):1-11.
A fictionalist theory of universals.Tim Button & Robert Trueman - forthcoming - In Peter Fritz & Nicholas K. Jones (eds.), Higher-Order Metaphysics. Oxford University Press.
Ordinal Type Theory.Jan Plate - forthcoming - Inquiry: An Interdisciplinary Journal of Philosophy.
On Type Distinctions and Expressivity.Salvatore Florio - 2023 - Proceedings of the Aristotelian Society 123 (2):150-172.
Against relationalism about modality.Carlos Romero - 2023 - Philosophical Studies 180 (8):2245-2274.

View all 10 citations / Add more citations

References found in this work

Quality and concept.George Bealer - 1982 - New York: Oxford University Press.
Objects of thought.Arthur Norman Prior - 1971 - Oxford,: Clarendon Press. Edited by P. T. Geach & Anthony Kenny.
Philosophy and Model Theory.Tim Button & Sean P. Walsh - 2018 - Oxford, UK: Oxford University Press. Edited by Sean Walsh & Wilfrid Hodges.
Plural Logic.Alex Oliver & Timothy John Smiley - 2013 - Oxford, England: Oxford University Press UK. Edited by T. J. Smiley.

View all 43 references / Add more references