zbMATH — the first resource for mathematics

Reverse mathematics, trichotomy and dichotomy. (English) Zbl 1296.03008
This paper explores connections between reverse mathematics and constructive analysis. In [J. L. Hirst and C. Mummert, Notre Dame J. Formal Logic 52, No. 2, 149–162 (2011; Zbl 1225.03083)], it is shown that if a certain formula is provable in a constructive setting then \(\mathsf{RCA}_0\) proves a related formula for sequences. In this paper the non-constructive dichotomy (\(a\leq 0 \,\lor\, a\geq 0\) for \(a\in\mathbb{R}\)) and the trichotomy principle (\(a < 0 \,\lor\, a=0\,\lor\, a>0\) for \(a\in\mathbb{R}\)) are considered. It is shown that over \(\mathsf{RCA}_0\), \(\mathsf{WKL}\) is equivalent to a sequence of dichotomies, i.e., to the statement that for a sequence \(\langle a_i \rangle \subseteq \mathbb{R}\) there is a set \(I\subseteq \mathbb{N}\) with \(a_i \leq 0\) iff \(i\in I\). A similar statement is obtained for trichotomies and \(\mathsf{ACA}\). Moreover, (constructive) weakenings of these principles are explored.

03B30 Foundations of classical theories (including reverse mathematics)
03F35 Second- and higher-order arithmetic and fragments
03F55 Intuitionistic mathematics
03F60 Constructive and recursive analysis
Full Text: DOI