On the strength of the finite intersection principle
We study the logical content of several maximality principles related to the finite intersection principle (FIP) in set theory. Classically, these are all equivalent to the axiom of choice, but in the context of reverse mathematics their strengths vary: some are equivalent to ACA0 over RCA0, while others are strictly weaker and incomparable with WKL0. We show that there is a computable instance of FIP every solution of which has hyperimmune degree, and that every computable instance has a solution in every nonzero c.e. degree. In particular, FIP implies the omitting partial types principle (OPT) over RCA0. We also show that, modulo Σ 02 induction, FIP lies strictly below the atomic model theorem (AMT).
Dzhafarov, D.D., Mummert, C. On the strength of the finite intersection principle. Isr. J. Math. 196, 345–361 (2013). https://doi.org/10.1007/s11856-012-0150-9