Splittings and disjunctions in reverse mathematics

Foundations of classical theories (including reverse mathematics) (03B30) Higher-type and set recursion theory (03D65) Second- and higher-order arithmetic and fragments (03F35)

Abstract: Reverse Mathematics (RM hereafter) is a program in the foundations of mathematics founded by Friedman and developed extensively by Simpson and others. The aim of RM is to find the minimal axioms needed to prove a theorem of ordinary, i.e. non-set-theoretic, mathematics. As suggested by the title, this paper deals with two (relatively rare) RM-phenomena, namely splittings and disjunctions. As to splittings, there are some examples in RM of theorems

A, B, C

such that

A l e f t r i g h t a r r o w (B w e d g e C)

, i.e.

A

can be split into two independent (fairly natural) parts

B

and

C

. As to disjunctions, there are (very few) examples in RM of theorems

D, E, F

such that

D l e f t r i g h t a r r o w (E v e e F)

, i.e.

D

can be written as the disjunction of two independent (fairly natural) parts

E

and

F

. By contrast, we show in this paper that there is a plethora of (natural) splittings and disjunctions in Kohlenbach's higher-order RM. Finally, we discuss the role of these results in the grand scheme of things.

Review text

The author examines equivalences in higher order reverse mathematics for conjunctions and disjunctions of formulas. Such results have long been of interest in traditional reverse mathematics. For example, \textit{P. A. Cholak} et al. [J. Symb. Log. 66, No. 1, 1--55 (2001; Zbl 0977.03033)] proved the equivalence of Ramsey's theorem for pairs with the conjunction of the stable Ramsey theorem and the principle \textsf{COH}. \textit{H. Friedman} et al. [Ann. Pure Appl. Logic 62, No. 1, 51--64 (1993; Zbl 0781.03048)] proved the equivalence of the disjunction of \(\mathsf{WKL}_0\) and \(\Sigma^0_2\) induction with the assertion that finite iterations of continuous functions are continuous. Both types of results can lead to novel proof strategies. The first group of results here list splittings (conjunctions) equivalent to a modulus of uniform continuity \textsf{MUC} principle corresponding to the existence of the intuitionistic fan functional. The base system for these results is \(\mathsf{RCA}^\omega_0 +\mathsf{QF}\text{-}\mathsf{AC}^{2,0}\). Additional splittings of the functional principles \(\exists^2\) and \(\exists^3\) are related to \(\neg\mathsf{MUC}\). A second group of results proven over \(\mathsf{RCA}^\omega_0\) includes many disjunctions equivalent to \(\mathsf{WKL}_0 \lor\mathsf{I}\Sigma^0_2\). Additional disjunctions equivalent to \(\mathsf{WWKL}\) follow. After a section describing the foundational motivations of the work, a table gives a partial overview of the results. Note that, for example, Theorem 3.8 provides a scheme for generating additional results too numerous for inclusion in the table.

Recommendations

Cites work

Cited in

(10)

This page was built for publication: Splittings and disjunctions in reverse mathematics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2176407)