Which axioms of ZF are used for finite choice? Apologies if this is a silly question, not an expert in set theory but just wondering about it.
ZF implies finite choice. But let's suppose one wanted to work without it. The thinking here is being uncomfortable about sets where none of the elements are computable/definable, therefore one couldn't pick one explicitly. The idea is to allow nonempty sets where it's not allowed to pick exactly one element, you may be able to define subsets but not a single element. Obviously, finite choice is allowed when it's possible to constructively name an element.
Which axiom(s) of ZF would have to go in order to remove finite choice? Is there any set theory that rejects finite choice, or is this pruning away too many useful results?
 A: As mentioned in the comments, one needs truly very few ZF axioms to prove the instances of of the axioms of choice for finite families. Let us denote by $\text{AC}\upharpoonright n$ the assertion that every collection $\cal A$ of $n$ nonempty disjoint sets has a selecting set $B$, that is, a set $B$ such that $A\cap B$ is  a singleton for every $A\in\cal A$. 
(Note that this is not the same as the assertion that every collection of disjoint sets of size $n$ has a selector.) 
Part of the point now is that $\text{AC}\upharpoonright 0$ is basically vacuous, since the empty family has any set as a selector vacuously. Further, if $\text{AC}\upharpoonright n$ holds, then one may easily prove $\text{AC}\upharpoonright (n+1)$ as follows: given any family of size $n+1$, consisting of disjoint nonempty sets, we may delete an element $A$ from it and have a family of size $n$, which has a selector by the hypothesis, and this selector can be extended to a selector on the large family by adjoining any element of $A$. Thus, by induction, we prove $\text{AC}$ for all finite families. 
Note that in the inductive step of the argument, we don't need to worry about defining a particular element of $A$, the set we deleted, since we are not proving that there is a definable selector; rather, we are only proving the existence claim that every such family has at least one selector. Similarly, we don't need to worry about how to choose a particular element to delete---the proof shows that for each set $A\in\cal A$, there are selectors obtained by deleting that set. So there is at least one selector. 
Thus, by induction, we prove $\forall n\ \text{AC}\upharpoonright n$, or in other words, that the axiom of choice holds for finite families. 
How much of ZF suffices for this argument? Of course we needed some very basic things like extensionality, pairing and union in order to make sense of the empty set and adjoining an element and so on, and perhaps one doesn't want to do set theory anyway without these axioms. Secondly, we needed to be able to prove a statement by induction on the natural numbers. 
Thus, the argument can be undertaken in Kripke-Platek set theory, a very weak subsystem of ZF. One issue is that one might think that $\Sigma_2$-separation is required for the inductive argument, in order to form the set $\{ n\in\mathbb{N}\mid \neg \text{AC}\upharpoonright n\}$, with a view to proving that this set can have no least element, since the negation of $\text{AC}\upharpoonright n$ appears to be a $\Sigma_2$-assertion as it asserts the existence of a family of size $n$ with no selector. But KP includes the $\in$-foundation scheme, which allows one to prove statements of any complexity by $\in$-induction, and this implies natural-number induction. 
But as noted, we really only needed natural number induction for $\Pi_2$-assertions, since $\text{AC}\upharpoonright n$ has complexity $\Pi_2$, and this would be a weakening of KP. I expect that one can go much lower than KP. 
Lastly, as I mentioned in the comments, we don't need any induction scheme at all to prove every instance of $\text{AC}\upharpoonright n$ for meta-theoretically finite $n$, that is, to prove $AC$ for families of size $1$, of size $2$, of size $3$ and so on, as a theorem scheme. The reason is that for such meta-theoretically finite families, the induction can be undertaken in the meta-theory, rather than in the object theory, and so one needs hardly any set theory at all to prove these instances. 
