Reverse mathematics and properties of finite character (Q435197)

This article analyzes the logical strength of variants of Tukey's lemma in the framework of reverse mathematics. A formula \(\varphi\) with one free set variable has the finite character property if \(\varphi (\emptyset )\) holds and for every set \(A\), \(\varphi (A)\) holds if and only if \(\varphi (F)\) holds for every finite \(F \subseteq A\). For a class of formulas \(\Gamma\), the principle \(\Gamma\)-FCP asserts that, given any formula of finite character in \(\Gamma\) (with parameters), every set \(A\) has a maximal subset \(B\) such that \(\varphi (B)\) holds. The authors show that RCA\(_0\) proves \(\Sigma^0_1\)-FCP, and that for \(n\geq 1\), RCA\(_0\) proves that ACA\(_0\) is equivalent to \(\Pi^0_n\)-FCP and \(\Pi^1_n\)-CA\(_0\) is equivalent to \(\Pi^1_n\)-FCP. The finite character principle can be strengthened by requiring that the maximal set is closed under a finitary closure operator, yielding the \(\Gamma\)-CE scheme, or under a nondeterministic finitary closure operator, yielding \(\Gamma\)-NCE. The authors show that QF-CE and \(\Sigma^0_1\)-CE are each equivalent to ACA\(_0\), while QF-NCE and \(\Sigma^0_1\)-NCE are each equivalent to \(\Pi^1_1\)-CA\(_0\). For \(n \geq 1\), RCA\(_0\) proves that \(\Pi^1_n\)-CA\(_0\) is equivalent to \(\Pi^1_n\)-NCE. The results in this paper provide an interesting contrast to the authors' work on finite intersection principles [``On the strength of the finite intersection principle'', Isr. J. Math. (2012; \url{doi:10.1007/s11856-012-1050-9}), \url{arXiv:1109.3374}].