[im3w1l]

I think the nature of mathematics is an interesting question without one clean answer. To present a radically different view of mathematics:

It's a game of string transformations, where the goal is to produce specific strings given a set of rules.

The (syntactically valid) strings would correspond to statements, a producible string a theorem, and the production the proof.

[chowells]

This is a description of one portion of math... one that's very easy to get tunnel vision towards when undertaking a very formal undergraduate mathematical education. And that's especially true if it was alongside a computer science education, which is precisely the branch of math concerned with formal systems being used in calculation.

I've done both of those things. I know what you get taught. But I've kept my math education going for the 25 years since then. I've talked to practicing mathematicians about what they do. I've learned a lot about the scope of math.

As an aside: most people really dislike it when I say that they should be much more precise about different numerical systems. The integers are not a subset of the rationals. They are entirely different constructions, but there is an isomorphism between integers and a subset of the rationals that preserves the integers' ring structure within that subset of the rationals and a few other aesthetic concerns. You can see why no one wants to communicate like this, even if they acknowledge it's technically correct. So I know all about pushing symbols around.

But I also know that pushing symbols around isn't the whole story. Pushing symbols around is only useful as a final check. Do you want to validate that 1+2=3? Pushing symbols around can help. But how do you decide that the ideas behind 1, 2, 3, +, and = are worth having precise and compact representations?

Math doesn't just use formal systems to generate proofs. It's not enough for symbols to be arranged neatly according to some rules. Math is also the process of creating the sets of symbols and their rules and communicating to other people why this set of rules and symbols is interesting. What ideas get preserved when you are working with this system? What is it an abstraction over?

[im3w1l]

> The integers are not a subset of the rationals. They are entirely different constructions, but there is an isomorphism between integers and a subset of the rationals that preserves the integers' ring structure within that subset of the rationals and a few other aesthetic concerns.

This actually strikes me as a very formal perspective.

Considering it from an informal perspective, it's a bit more fuzzy isn't it. As you say there are many isomorphic things, and when we say The Integers it's not actually clear which one of them we mean. Maybe we mean one of them today and another tomorrow. Often times it doesn't matter, and so we don't clarify the question.

Like you could imagine defining the BootstrapNaturals then the BootstrapIntegers then the BootstrapRationals then use them to define the Reals. And then say that the Naturals, Integers and Rationals are defined as subsets of the Reals. This would be one way to put the common view of the Naturals as being a subset of the Reals on a solid formal foundation. It's rarely done ig because it's seen as obviously unproblematic to be a bit handwavy.

Another criticism of the common construction of numbers we could pose, inspired by object oriented programming, is that they fail at "information hiding". In programming an object should ideally not expose its internals. But in mathematics we may define 0 as say the empty set, making set operations on numbers syntactically valid which is kinda strange.

But yeah I think everyone has a sort of implicit understanding that 0 isn't actually the empty set. That it's merely a sort of hmm... thought experiment? That considering it 0 is a limited time offer, for the duration of the definition phase?

Maybe we come back to the isomorphism after all. "The natural numbers are something isomorphic to this set stuff I will now do"