One Plus One Equals Two (2006)

I'd say mathematics is discovered and definitions are invented. E.g. "ordered pair" is not part of set theory, it's an invented name we give to a convenient definition of a set schema.

Even base-N representations are an invention: S() and zero are all you need, but Roman Numerals were an improvement over base-1 representations and base-N is significantly more convenient to work with.

Be careful with making assumptions from modern, formalized set theory and the naive set theory.

The axiom schema of specification is added to avoid Russell's paradox.

A set in the naive meaning is just a well-defined collection of objects.

As ordered pairs are a binary relation, foundedness or order are operation dependant, and assuming an individual set is unordered is a useful assumption.

But IMHO it is problematic from a constructivist mathematics perspective. The ambiguity of a nieve set, especially when constricting the natural numbers, which are obvious totally ordered is a challenge to overcome.

I know the Principia was focused on successor sets, so mostly avoid it, but IMHO they would have hit it when trying to define an equally operation

If you remember membership and not elements define a set:

{a,b,c}=={a,b,c,b}=={c,b,b,a}

In a computing context, there were some protocols that may have been IBM specific that required duplicate members to be adjacent.

So while the first and the third sets would be equivalent, the second wouldn't be, so order mattered.

Most actual implementations just dropped the redundant elements, vs track membership, but I was just trying to provide an actual concrete example.

IIRC the axiom schema of specification is one of those that was folded into others in modern ZFC textbooks so it is easy to miss.

Mathematics is entirely founded on human invention.

When we wrote simple mathematics on the Pioneer and Voyager probes I think it was under the assumption that anyone or anything else finding them would have co-discovered enough mathematics to recognize it on the plaques. That's the sense in which I use the word "discovered" for much of mathematics. Our definitions will differ from aliens but the foundations will be translatable.

I'm not sure if I completely understand your point. Is it that the definitions of ordered pairs must be done carefully when talking about constructions in Principia because of its formulation in logical predicates, e.g. care was taken when constructing sets to avoid Russell's paradox explicitly given the axioms of logic rather than Russell's paradox being excluded in ZF by the axiom schema of specification?

Or is the difficulty in introducing a canonical order for the ordered pair, or introducing well/partial-ordering in sets themselves? I guess I see an ordered pair as more of an indexical definition than an ordering definition.

A sentient entity could well decide to simulate the universe without developing tools to approximate it.