On the strength of the finite intersection principle (Q375889)

Consider the following (intersection) properties of families of sets \(A\). The \(D_k\) intersection property is the property that the intersection of each \(k\) distinct sets of \(A\) is empty. The \(\overline{D}_k\) intersection property is the property that the intersection of each \(k\) sets of \(A\) is non-empty. The \(F\) intersection property is the property that each finite intersection of sets of \(A\) is non-empty. It is a classical result that for each of the above intersection properties \(P\) the statement that each family \(A\) of sets contains a maximal subfamily \(A'\subseteq A\) satisfying \(P\), is equivalent to the axiom of choice over ZF. In this paper, these statements are analyzed in the fashion of reverse mathematics. To formulate them in the language of reverse mathematics the authors restrict their attention to countable families of sets. Writing \(P\mathsf{IP}\) for this statement with property \(P\), the following is obtained. \(D_k\mathsf{IP}\) is equivalent to \(\mathsf{ACA}_0\), \(F\mathsf{IP} \rightarrow \overline{D}_{k+1}\mathsf{IP} \rightarrow \overline{D}_k\mathsf{IP}\), and the \(\Pi^0_1\)-generic principle implies \(F\mathsf{IP}\) and \(\mathsf{WKL}_0\nvdash \overline{D}_2\mathsf{IP}\). Moreover, connections to the atomic model theorem and the omitting types theorem from [\textit{D. R. Hirschfeldt} et al., Trans. Am. Math. Soc. 361, No. 11, 5805--5837 (2009; Zbl 1184.03005)] are given.