> For example, we have mathematics without the law of the excluded middle and with it, ones without the axiom of choice and with it, etc.

This is a bit off-topic. Elsewhere in comments [1] people talk about Terence Tao and his recent work in Lean. Lean is based on intuitionistic logic, a base which doesn't include axiom of choice and the excluded middle.

Since Tao and other classical mathematicians need excluded middle for proofs by contradiction.

The Classical library in Lean starts by declaring axiom of choice [2] and after some lemmas introduces excluded middle as a theorem, called "em" for brevity [3]. I like how Lean makes this particular choice for classical mathematics very obvious.

[1] https://news.ycombinator.com/item?id=38102096#38104412

[2] https://github.com/leanprover-community/lean/blob/cce7990ea8...

[3] https://github.com/leanprover-community/lean/blob/cce7990ea8...