The good intuitive reasons that the Axiom of Choice (AC) for arbitrary sets-- that a function f with f(i) in S(i) for each i in {i}, for any non-empty sets {i} and all S(i), exists-- doesn't follow from just ZF, seem to be good for finite {i} and S(i) (i.e., for FAC-- AC for {i} and all S(i) finite) as well as for one or both being infinite (I may be challenged on this). Whether the Godel-Cohen proof of the independence of AC from ZF works with FAC substituted for AC, I don't know. However, the best-known very peculiar consequence of ZFC, the Banach-Tarski paradox, requires AC for infinite S(i) (and maybe infinite {i}--I don't remember that detail of its demonstration which I saw long ago.) My question is, are there any at least nearly as peculiar paradoxes which are consequences of ZF + FAC, or at least ZF + (AC for all S(i) finite)?

Perhaps this edit will make my question more nearly suitable for MO. The "good intuitive reasons" (I actually know of only one) that AC doesn't follow from ZF is the following (which of course is not a proof of that fact): Any proof of that fact on the basis of ZF would have to be simply that since each S(i) is non-empty, for each i there is an e(i) in S(i), so let f(i) = e(i). Then f is the required choice function. The reason that this isn't a proof is that the existence of an e(i) in S(i) doesn't specify what that e(i) is, so f isn't specified by the foregoing, and even its existence isn't established. Since the supposed proof as well as its fatal objection don't refer to any properties of {i} and the S(i)'s other than their being non-empty, the objection to the offered proof applies to even that for AC restricted to finite {i} and S(i)'s. The rigorous proof that this supposed proof is defective is of course Godel-Cohen.

Peter LeFanu Lumsdaine--Your mentioned proof, by ordinary induction on the size of {i}, that AC for finite {i} (and presumable countably infinite {i}) is provable in ZF and even in weaker systems must therefore be different from the above, defective supposed proof. I have no idea what it could be. Would you supply at least as outline of it, a link, or a citation?

Effective implications between "finite" choice axioms[pp. 439-458 in Mathias/Rogers (editors),Cambridge Summer School in Mathematical Logic, Lecture Notes in Mathematics #337, Springer-Verlag, 1973; MR 50 #12725; Zbl 279.02047]. $\endgroup$ – Dave L Renfro May 19 '18 at 8:43