It's interesting to look at how people have handled the axiom of choice in Metamath, since the axiom of choice has long had some controversy. Metamath lets you

It's interesting to look at how people have handled the axiom of choice in Metamath, since the axiom of choice has long had some controversy. Metamath lets you state your axioms, then show that proofs build from their axioms. Each such collection of axioms & proofs is called a "database". There are Metamath databases that build on intuitionistic logic <http://us.metamath.org/ileuni/mmil.html http://us.metamath.org/ileuni/mmil.html> and New Foundations <http://us.metamath.org/nfeuni/mmnf.html http://us.metamath.org/nfeuni/mmnf.html> among others. The largest Metamath database by far uses ZFC (Zermelo-Fraenkel Set Theory with the Axiom of Choice). That's the Metamath Proof Exporer (MPE) database: <http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html>. But even in that database, it's avoided where possible. Its conventions say, "We prefer proofs that depend on fewer and/or weaker axioms, even if the proofs are longer. In particular, we prefer proofs that do not use the axiom of choice where such proofs can be found. The axiom of choice is widely accepted, and ZFC is the most commonly-accepted fundamental set of axioms for mathematics. However, there have been and still are some lingering controversies about the Axiom of Choice. Therefore, where a proof does not require the axiom of choice, we prefer that proof instead. E.g., our proof of the Schroeder-Bernstein Theorem (sbth) does not use the axiom of choice. In some cases, the weaker axiom of countable choice (ax-cc) or axiom of dependent choice (ax-dc) can be used instead." <http://us.metamath.org/mpeuni/conventions.html http://us.metamath.org/mpeuni/conventions.html>