Let us say that a family $R$ of sets has the Finite Subcovering Property --- FSP --- if any subfamily of $R$ which covers the union $\cup B: B \in R$ has itself a finite subfamily which also covers. For example, take for $R$ the family of open balls in a compact metric space $M$. Clearly the family of finite intersections of open balls also has the FSP.


We say the Finite Intersection Principle --- FIP --- is the statement: If $R$ has the FSP then the family of all finite intersections of members of $R$ also has the FSP.


It is easily proved that FIP is a theorem in ZFC. The question is: Does ZF + FIP imply the Axiom of Choice?


I looked in Herrlich, "Axiom of Choice", and I did not see this, but I may have missed it. This must certainly be known: the question was raised by J. L. Kelley in Fund. Math. 37 (1950), p. 76.


Note that in the absence of the Axiom of Choice, we need to specify what "finite" should mean. For our purposes here, let's say a set is finite if it may be ordered so that every non-void subset has both a first element and a last element in the ordering. See Herrlich Section 4.1 for equivalent formulations.



A combinatorial property implied by the Axiom of Choice
This is not really an answer but too long for a comment:


Let me point out that there might be a relation to the Alexander Subbase Theorem here:  

A topological space is compact iff the topology has a subbase with the FSP. 


What FIP gives you is this:


If $R$ has the FSP and is a subbase for the topology of a space $X=\bigcup R$, then $X$ has a basis (namely all finite intersections of elements of $R$) with the FSP. 


Unfortunately it seems that getting compactness from the existence of a basis with the FSP also requires some form of choice. So FIP could be strictly weaker than the Alexander Subbase Theorem. But an upper bound on how much choice is needed for the subbase theorem would also be an upper bound for FIP.


Unfortunately I don't have access to any Axiom of Choice book right now. But it seems likely that there is some information about the amount of choice needed for the subbasis theorem.




---


Edit: By godelian's comment below, this actually answers the question: FIP follows from Alexander's Subbase Theorem which follows from the Boolean prime ideal theorem which is known to be strictly weaker than the full Axiom of Choice. So no, FIP does not imply AC.


