Of course there are many pairing functions, and they all
have the crucial property that from the pair $(x,y)$, one
can reconstruct both $x$ and $y$. And although your
question has been answered, let me point out that all four
of the ordered pair definitions that you consider have the
property that the von Neumann rank of the pair $(x,y)$ is
strictly greater than the ranks of $x$ and $y$. Thus, for
your functions, if $x$ and $y$ are in $V_\alpha$, then the
pair $(x,y)$ can only be guaranteed to appear by
$V_{\alpha+2}$.

But actually, this rank-increasing feature is sometimes
annoying, and there occasionally arises in set-theoretic
argument the need or desire for a *flat* pairing function,
a pairing function that does not increase rank in this way.
Specifically, what is desired is a pairing function
$\langle x,y\rangle$ such that whenever $x,y\in V_\alpha$
for infinite $\alpha$, then also $\langle x,y\rangle\in
V_\alpha$, for the same rank $\alpha$. (Note that one
cannot achieve this for finite $\alpha\gt 1$, since there
are too many pairs to fit.) With such a flat pairing
function, every infinite $V_\alpha$ is closed under
pairing, and this is sometimes important or at least
convenient in inductive arguments, or in arguments about
$\alpha$-strong cardinals and in similar situations, where
one wants to consider only sets of a given rank, but one
also wants to use pairs.

It is a fun exercise to prove that flat pairing functions
exist, and I encourage you to try it on your own, before
reading what I write below. But the definitions are all
somewhat more involved than the comparatively simple
definitions you provide, since they achieve the flatness
property. As Hurkyl says, we ultimately care only about the
existence of the function with the desired properties,
rather than its exact nature.

Here is one way to construct a flat pairing function.
Define $\langle x,y\rangle=x^0\cup y^1$, where $x^0$ is
obtained by replacing every natural number $n$ in any
element of $x$ by $n+1$ and adding the object $0$, whereas
$y^1$ just replaces $n$ inside elements of $y$ with $n+1$.
Thus, we can tell from any element of $x^0\cup y^1$ whether
it came from $x$ or $y$, by looking to see if it contains
$0$ or not, and we can reconstruct the unmodified set by
removing $0$ and replacing all $n+1$ with $n$ again, and so
it is a pairing function. And one can check that $\langle
x,y\rangle$ has the same rank as the maximum rank of $x$
and $y$, if this max is infinite, and so this is a flat
pairing function, as desired.

essenceof "ordered pair", but just to bring this notion into the language of set theory (in the same spirit of von Neumann's definition of ordinal numbers, for instance). So it really doesn't matter which one we choose. $\endgroup$ – Pietro Majer Apr 24 '11 at 6:15