Sorites is an ancient piece of paradoxical reasoning pertaining to sets with the following properties: elements of the set are mapped into some set of “attributes”; if an element has a given attribute then so are the elements in some vicinity of this element; and such vicinities can be arranged into pairwise overlapping finite chains connecting two elements with different attributes. Obviously, if Superveneince is assumed, then Tolerance implies lack of Connectedness, and Connectedness implies lack of Tolerance. Using a very (...) general but precise definition of “vicinity”, Dzhafarov & Dzhafarov 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 is provable in$RC{A_0}$, while the formalization of is equivalent to$AC{A_0}$over$RC{A_0}$. Thus, in a certain precise sense, the approach of is more constructive than that of. (shrink)