Nielsen-Schreier and the Axiom of Choice

Question

The Nielse-Schreier (NS) Theorem says that every subgroup of a free group is free. The proof uses the Axiom of Choice, and Läuchli showed in 1962 that the negation of NS is consistent with ZFA (ZF with atoms). By a result of Jech-Sochor, this result can be transferred to ZF. So some form of Choice is needed to prove NS.

In 1985, Paul Howard showed that the Axiom of Choice for sets of finite sets follows from NS.

Is the NS theorem known to be equivalent to the Axiom of Choice or some weak form of Choice?

Answer 1

As I wrote at the end of this answer, the paper by Paul Howard doesn't appear to be cited anywhere (see this Google Scholar search).

So I doubt there has been any progress since Howard's original paper, and that there is any particular "choicey" principle that the NS theorem is equivalent to.

It should also be remarked that "weak form of choice" is a very arbitrary thing, one can define it simply as a statement provable from $\sf ZFC$ but not from $\sf ZF$, but one can also define it as a statement which explicitly says "Given a family with property X, we can choose from it". In the case of the former, NS itself appears to be a weak form of choice; but in the latter case it is not clear if such principle even exists (for example "every set can be linearly ordered" is not equivalent, to the best of my knowledge, to such principle).