I got this idea while reading a textbook. Previously I read that ordered pairs can be formalized in axiomatic set theory — for example, $(a, b) := \{\{a\}, \{a, b\}\}$ is viable solution. It has the property we would like to have, i.e. $ (a, b) = (c, d) $ iff $a = c$ and $b = d$.
However, this only deals with pairs. If the Cartesian product of two sets $X$ and $Y$ is defined as follows: $$ X\times Y := \{(x, y)\in\mathcal P(\mathcal P(X\cup Y))| x\in X \land y \in Y\}$$ Then, what does it mean by writing $\mathbb R^3$? If this refers to $\mathbb R \times \mathbb R \times \mathbb R $, which of these does it exactly express: $(\mathbb R \times \mathbb R) \times \mathbb R $ or $\mathbb R \times (\mathbb R \times \mathbb R)$? To make things worse, sometimes we write $(V^*)^p \times V^q$ to donate a $(p+q)$-tuple, such that the first $p$ elements are from the $V^*$, and the rest of them are from $V$. The formalization of ordered pairs and Cartesian products discussed above doesn’t seem to able to solve the problems directly.
Thus, I wonder whether the idea of ‘flattened’ ordered pairs may be useful: to make the ordered pairs satisfy yet another axiom: $\forall a, b, c(a,(b,c)) = ((a, b), c)$. Hence, the distinction between $(a,(b,c))$ and $(a,(b,c))$ is eliminated, and we can write uniformly: $(a,b,c)$.
To summarize: the theory of ‘flattened’ ordered pairs includes a primitive binary function $\mathscr P$ and two axioms: $$ \forall a \forall b \forall c \forall d ( \mathscr P ab \equiv \mathscr P cd \leftrightarrow a \equiv c \land b \equiv d)$$ $$ \forall a \forall b \forall c( \mathscr P \mathscr P abc \equiv \mathscr P a \mathscr P bc )$$
Does it has any model in the axiomatic set theory?
I tried $\langle a, b\rangle := \{\{a\}, \{a, b\}\}$ and $(a_1, \ldots, a_n):=\{\langle 1, a_1 \rangle, \ldots , \langle n, a_n\rangle\}$ which gives the $n$-tuple directly. I also thought about definition involving equivalent class. However, I still don’t know how to define the function $\mathscr P$, unless the if the parameter is a tuple is previously known. (Is this possible?)
Finally, my questions are:
Is there a more elegant way to solve the problem of defining multiple cartesian products?
Can we build the ‘flattened’ ordered pairs from the set theory?
A simple thing you can do is pick a fixed parenthesization: for example, you can choose to parenthesize starting on the right, so that e.g. $\mathbb{R}^4$ is $\mathbb{R} \times (\mathbb{R} \times (\mathbb{R} \times \mathbb{R}))$, or you can choose to parenthesize starting on the left, which is flipped. The problem is that with this definition the Cartesian product fails to be associative on the nose, so that for example $\mathbb{R}^2 \times \mathbb{R}^2 \neq \mathbb{R}^4$, and you might consider this unsatisfying.
What is true, however, is that the Cartesian product is monoidal. This means that even though it's not associative on the nose we can define a family of bijections
$$a_{X, Y, Z} : X \times (Y \times Z) \cong (X \times Y) \times Z$$
called associators which satisfy a somewhat complicated set of axioms, the point of which is to guarantee that any two ways of using associators to identify two parenthesizations of a Cartesian product agree.
Most binary operations on mathematical objects that you're familiar with fail to be associative on the nose (depending on how you construct them) but are still monoidal in this way, for example tensor products of vector spaces.