Against Cumulative Type Theory

TL;DR

This paper critically examines Cumulative Type Theory (CTT), arguing against its philosophical and semantic motivations, and defends Standard Type Theory (STT) with a Fregean semantics as more justified.

Contribution

The paper provides a detailed critique of CTT, defends STT using Fregean semantics, and clarifies the relationship between CTT and STT, including an analysis of Florio & Jones's approach.

Findings

CTT's relaxed type restrictions are unjustifiable.

Fregean semantics justify STT's type restrictions.

Florio & Jones's approach is a form of STT.

Abstract

Standard Type Theory, STT, tells us that $b^n(a^m)$ is well-formed iff $n=m+1$. However, Linnebo and Rayo (2012) have advocated for the use of Cumulative Type Theory, CTT, which has more relaxed type-restrictions: according to CTT, $b^\beta(a^\alpha)$ is well-formed iff $\beta > \alpha$. In this paper, we set ourselves against CTT. We begin our case by arguing against Linnebo & 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 & Rayo's Semantic Argument for CTT. We end by examining an alternative approach to cumulative types due to Florio & Jones (2021); we argue that their theory is best seen as a misleadingly formulated version of STT.