I am bothered by the fact that most mathematicians aren’t bothered by that! Am I missing something? Would love to understand why like, system F isn’t the foundation of math (i should care about)
Outside of logic and set theory, most mathematicians aren't really working in any particular foundation: they're working directly with the relevant structures. An ordered pair `(x,y)` can be modeled as the set `{{x},{x,y}}`, but that doesn't mean it is that set. What it is, to the extent the question is even coherent, is a thing that has the data ordered pairs are supposed to have: a first element, and a second element.
This may be true for Category Theory as well (Product of two objects):
https://en.wikipedia.org/wiki/Product_(category_theory)
But Category Theory captures the essence of Products/Pairs, so I am more inclined to accept it.
Well, yeah, but {x, y} is also a pair. How is (x, y) different? It's ordered, you say? All right, an ordering is a relation that's antisymmetric and so on, but in this case let's say we have a function that maps x to 0 and y to 1… But what is a function? Okay, a function is a type of relation, so let's define a relation first: a set of ordered pairs… oops.
The real problem with defining (x, y) = {{x}, {x, y}} is that elements of a set must also be elements of some universal set 𝓤, {x, y} ⊂ 𝓤, but as we know, there is infamously not such a thing as a "set of all things". Sets have to be typed. But in a pair, x and y can be of entirely different kinds of entities.
But an ordered set is fundamentally different than an unordered set as well!