Some time ago I read a somewhat informal paper that was basically an ode to equivalence classes. Equivalence classes, isomorphisms, homeomorphisms and similar abound. A lot of maths is going "this thing is shaped like this other thing".
Coming at it another way, maths is about the study of interesting patterns and structures. The interesting ones are the ones that keep cropping up. While you might define what a group is through a set of axioms, a group is really the name given to a set of patterns that kept occurring, and the generalisation of them.
This is all both anti-Bourbakist and in tune with the way maths really operates. Solvable groups pre-existed groups as Galois invented them for Galois theory, to say nothing of how people managed arithmetic for millennia before it was axiomatised.
Switching over to computer science for a moment, this is pretty much what's at the root of what's wrong with almost every monad tutorial. The stereotypical tutorial tries to explain what a monad is, in its generality, first. It would be so much more sensible to explain how you might want to build combinators to handle list comprehensions, state readers and writers, errors, I/O etc., and then point out how they all follow the same pattern, and that pattern is what a monad is, and how it can then be formalised.
Coming back to the realm of maths, the fact that these are repeating patterns that occur in different contexts mean that there's no single, true formalisation. You can build the natural numbers from set theory, or zero and a successor function, or lambda calculus terms, or whatever. They're all equivalent, and none is innately better.
Getting more metaphysical, if you see a system, you might ask what it's embedded in. If you can't tell from the inside, it's pretty much embedded in all the possibilities, and none. Putting it another way, engaging with a question that worries some people far more than it's worth thinking about (one generation via The Matrix, another via AGI over-analysis): The question "Are we all in a simulation?" is essentially meaningless, another Gödellian "undecidable inside the system" question.
I rather like maths giving me an excuse to not engage with such questions. I get to spend more time thinking about the lovely interesting patterns.
Posted 2023-11-23.