Review of Symbolic Logic:1-43 (forthcoming)
Authors |
|
Abstract |
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 |
Options |
![]() ![]() ![]() ![]() |
Download options
References found in this work BETA
Plural Logic.Alex Oliver & Timothy John Smiley - 2013 - Oxford, England: Oxford University Press UK.
Conceptions of Set and the Foundations of Mathematics.Luca Incurvati - 2020 - Cambridge University Press.
View all 43 references / Add more references
Citations of this work BETA
Engineering Existence?Lukas Skiba - forthcoming - Inquiry: An Interdisciplinary Journal of Philosophy.
Unrestricted Quantification and Ranges of Significance.Thomas Schindler - forthcoming - Philosophical Studies:1-22.
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.
An Interpretation of Martin-Löf's Type Theory in a Type-Free Theory of Propositions.Jan Smith - 1984 - Journal of Symbolic Logic 49 (3):730-753.
Cumulative Versus Noncumulative Ramified Types.Anthony F. Peressini - 1997 - Notre Dame Journal of Formal Logic 38 (3):385-397.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
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.
Defining Features Versus Incidental Correlates of Type 1 and Type 2 Processing.Keith E. Stanovich & Maggie E. Toplak - 2012 - Mind and Society 11 (1):3-13.
Expressing ‘the Structure of’ in Homotopy Type Theory.David Corfield - 2017 - Synthese 197 (2):681-700.
Analytics
Added to PP index
2021-08-27
Total views
126 ( #92,758 of 2,507,011 )
Recent downloads (6 months)
51 ( #16,776 of 2,507,011 )
2021-08-27
Total views
126 ( #92,758 of 2,507,011 )
Recent downloads (6 months)
51 ( #16,776 of 2,507,011 )
How can I increase my downloads?
Downloads