> Mathematics includes the natural numbers and plane and solid geometry.
That, to me, feels similar to Euclid’s fifth postulate, in the sense that it isn’t something you’d want to include in a definition.
Maybe, the similarity doesn’t end there, and we have multiple mathematics, just as pure mathematicians don’t talk about algebra, but about an algebra, with some of them being more interesting than others, and it not always being easy to show that two algebras are different from each other.
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.
> 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.
That, to me, feels similar to Euclid’s fifth postulate, in the sense that it isn’t something you’d want to include in a definition.
Maybe, the similarity doesn’t end there, and we have multiple mathematics, just as pure mathematicians don’t talk about algebra, but about an algebra, with some of them being more interesting than others, and it not always being easy to show that two algebras are different from each other.
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.