A note on the reverse mathematics of the sorites

TL;DR

This paper examines the reverse mathematical strength of formalizations of the sorites paradox, revealing that one formalization is more constructive than the other based on proof-theoretic analysis.

Contribution

It provides a new comparison of two formalizations of the sorites paradox using reverse mathematics, showing their differing proof-theoretic strengths.

Findings

Formalization (1) is provable in RCA_0.

Formalization (2) is equivalent to ACA_0 over RCA_0.

Approach (1) is more constructive than approach (2).

Abstract

Sorites is an ancient piece of paradoxical reasoning pertaining to sets with the following properties: (Supervenience) elements of the set are mapped into some set of "attributes", (Tolerance) if an element has a given attribute then so are the elements in some vicinity of this element, and (Connectedness) such vicinities can be arranged into pairwise overlapping finite chains connecting two elements with different attributes. Obviously, if Superveneince is assumed, then (1) Tolerance implies lack of Connectedness, and (2) Connectedness implies lack of Tolerance. Using a very general but precise definition of "vicinity", Dzhafarov and Dzhafarov (2010) offered two formalizations of these mutual contrapositions. Mathematically, the formalizations are equally valid, but in this paper, we offer a different basis by which to compare them. Namely, we show that the formalizations have different proof-theoretic strengths when measured in the framework of reverse mathematics: the formalization of (1) is provable in $\mathsf{RCA}_0$, while the formalization of (2) is equivalent to $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$. Thus, in a certain precise sense, the approach of (1) is more constructive than that of (2).