You do not need to worry about the axiom of choice because: (1) Provably so in a very weak (and hence trustworthy) metatheory, assuming the axiom of choice doe

You do not need to worry about the axiom of choice because: (1) Provably so in a very weak (and hence trustworthy) metatheory, assuming the axiom of choice does not result in any new inconsistencies. More precisely: The systems ZFC (Zermelo–Fraenkel set theory with the axiom of choice) and ZF (ZFC but without choice) are equiconsistent; if ZF is consistent, then so is ZFC. (2) There is a mechanical procedure for transforming ZFC-proofs of number-theoretic statements into ZF-proofs. That is, appeals to the axiom of choice can always be mechanically eliminated from proofs of number-theoretic statements, even if those proofs rely on results in other areas which crucially depend on the axiom of choice. You should worry about the axiom of choice because: (3) Assuming the axiom of choice imposes an undue restriction on the scope of your results: Any theorem proven without the axiom of choice and without the law of excluded middle (which is implied by the axiom of choice) automatically also applies to continuous families. For instance, the theorem "every real symmetric matrix has an eigenvalue" has a proof avoiding AC and LEM. Hence it also holds that for every continuous family of symmetric matrices, locally on the parameter space, there is a continuous eigenvalue-picking function. PS: One could also wonder whether one should worry about the law of excluded middle. One should not because: (1') The systems ZF and IZF (ZF but without LEM) are equiconsistent. (2') There is a mechanical procedure for transforming ZF-proofs of number-theoretic statements of the special kind "for every numer x, there exists a number y such that some equation holds" into IZF-proofs. On the other hand, one should worry because of (3). PPS: The axiom which one should truly worry about is the inconspicuous powerset axiom. In contrast with ZFC, ZF and IZF, which are all equiconsistent, removing the powerset axiom results in a drastically weaker system. The proof-theoretic strength of Kripke–Platek set theory (ZF without powerset) is a reasonably large ordinal, whereas we are lacking the technology to even fathom the ordinal calibrating the strength of IZF/ZF/ZFC.