What is the formal definition of a rectangular coordinate system? Suppose we are working over the set $\mathbb{R}^2$. What is the formal definition of a rectangular coordinate system for $\mathbb{R}^2$? Informally, we take two perpendicular lines $X$ and $Y$ in $\mathbb{R}^2$, and, letting $O$ be their point of intersection, we choose points $A$ and $B$ on $X$ and $Y$, respectively, such that the distance $AO$ is equal to the distance $BO$. Now, we can define the rectangular coordinate system for $\mathbb{R}^2$ based on $X$ and $Y$ and the distance $d = AO = BO$ as the unit distance. Note, by the way, that the order of $X$ and $Y$ matters. Well, this is a somewhat informal definition. But, what is it formally? That is, what is the formal definition of the function $f: \mathbb{R}^2 \rightarrow \mathbb{R}^2$ that takes an ordered pair of real numbers and maps it to the ordered pair of real number that you get from using the perpendicular lines $X$ and $Y$ as the coordinate axes and $d$ as the unit distance? For example, using the line $\mathbb{R} \times \{0\}$ as $X$ and the line $\{0\} \times \mathbb{R}$ as $Y$ and choosing the distance $d$ to be $1$, the corresponding $f$ is simply the identity function on $\mathbb{R}^2$
Edit: Wait, now I realize that the location of the points $A$ and $B$ matter. So, forget $d$, and consider the quadruple $(X,Y,A,B)$. How does one define the coordinate system based on that quadruple?
 A: Defining a rectangular coordinate system as a function $f : \mathbb R^2 \to \mathbb R^2$ seems silly: it is defining a rectangular coordinate system only in terms of one you've already got.
A good definition should begin the way you started your "informal" one:

We take two perpendicular lines $x$ and $y$, and, letting $O$ be their point of intersection, we choose points $A$ and $B$ on $x$ and $y$, respectively, such that the distance $AO$ is equal to the distance $BO$.

(I have taken the liberty to make $x$ and $y$ lowercase to avoid confusing the lines for points.)
But now, we should actually define the coordinates of a point. For any point $P$ in the plane, let $F$ be the foot of the perpendicular from $P$ onto $x$, and let $G$ be the foot of the perpendicular from $P$ onto $y$. Then:

*

*The $x$-coordinate of $P$ is the signed ratio $\frac{OF}{OA}$: it is negative if $O$ is between $A$ and $F$, and positive otherwise.

*The $y$-coordinate of $P$ is the signed ratio $\frac{OG}{OB}$ (with the same convention for signs).

If we denote the Euclidean plane by $\mathbb E$ (we can't call it $\mathbb R^2$ if we don't have a coordinate system yet) then the function $f : \mathbb E \to \mathbb R^2$ given by $P \mapsto (\frac{OF}{OA}, \frac{OG}{OB})$ is our coordinate function.

This answer does assume that even though we don't have a coordinate system, we do have a distance - which the axioms of Euclidean geometry don't immediately give us. So a more fundamental task in defining a coordinate system is this: how do we assign a real number to every line segment such that congruent line segments get equal numbers, and such that segment arithmetic obeys the rules of real number arithmetic?
