The current state of the metatheory of Banach tarski is that it follows from the ZF + Ultrafilter, but not ZF + dependent choice, and has very little to do with the excluded middle.