Reclassifying the antithesis of Specker's theorem (Q1938392)

In this paper, instances of the anti-Specker property are classified in the fashion of constructive reverse mathematics. The anti-Specker property is a semi-constructive compactness principle. A subspace \(X\) of a metric space \(Y\) has the anti-Specker (\(\mathsf{AS}^Y_X\)) property, if any sequence in \(Y\) that is eventually bounded away from any point in \(X\), is eventually bounded away from the entire set \(X\). The main result of this paper is that \(\mathsf{AS}^{\mathbb{R}^2}_{[0,1]}\), \(\mathsf{AS}^Y_X\) for any compact subspace \(X\) of \(Y\), and the fan theorem for \(\Pi^0_1\)-bars are equivalent. This result should be compared with [\textit{D. Bridges} and \textit{H. Diener}, Math. Log. Q. 56, No.~4, 434--441 (2010; Zbl 1206.03053)] where it was shown that \(\mathsf{AS}^{\mathbb{R}}_{[0,1]}\) is equivalent to the fan theorem for so-called \(c\)-bars.