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.

On a side note, and since you mentioned Roman Numerals in your other comment, I would say that the representation of I, II and III being different from IV is related to how the human brain processes quantities up to 4 [0].

So it is a simple example showing that the way humans process language influences the representation/definition of mathematical ideas.

[0] https://www.nature.com/articles/s41562-023-01709-3

As the Principia is pretty ugly and tortured at least for me let me offer:

Naive set theory. Halmos, Paul R. http://people.whitman.edu/~guichard/260/halmos__naive_set_th...

Note the first entry of "Ordered Pairs"

> What does it mean to arrange the elements of a set A in some order?

Also note how the earlier section on "Unordered Pairs" is more about building the axiom of pairing etc...to get to ordered pairs which gets to the Cartesian product, which outputs ordered pairs.

It doesn't matter if you go through Zermelo's theorem+Zorn, that states that every set can be well-ordered, or though Cartesian product's and/or AC. (Note: This is in FoL well-ordering and AC are the same, but not in SoL and HoL)

It is not that sets are expressly unordered, as a set of points in a line segment would very much have an order, but that you didn't actively arrange the elements in order to take advantage of properties that are useful to you.

Maybe I just hit mental blocks but IMHO it is important that when you make the assumption that "there exists a set." it is very important to realize that it is "unordered" because you haven't imposed one, but is not an innate property of an element of the set.

Hopefully that helps in addressing this from your original post.

> "ordered pair" is not part of set theory

While many creators of both naive and formal set theories may choose to not define (a,b) = {{a},{a,b}} explicitly, the output of the Cartesian product is the ordered pairs, so it doesn't matter, you don't have a useful set theory without them.