Kuratowski's definition of ordered pairs
Kuratowski's definition arose naturally out of Kuratowski's idea for representing any linear order of a set $S$ in terms of just sets, not ordered pairs. The idea was that a linear ordering of $S$ can be represented by the set of initial segments of $S$. Here "initial segment" means a nonempty subset of $S$ closed under predecessors in the ordering. When applied to the special case of two-element sets $S$, this gives the Kuratowski ordered pair.
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.
How one models ordered pairs is not particularly important; what matters is the existence of a pairing function $(-,-)$ along with functions $\text{first}(-)$ and $\text{second}(-)$ satisfying the requisite properties.
Which definition you use only matters for a brief period between the definition and the point where its properties have been proven, at which point you promptly forget the details of the definition -- so the only real point of deliberating definitions is to make this period as painless as possible for others.
I haven't thought through all of the possibilities, but I will offer an example that $\text{first}(-)$ is tricky to define for your definition 1. The 'obvious' choice seems to be $$ z = \text{first}(P) \equiv z \in P \wedge \exists a: z \in a \in P $$ which turns out to depend on the axiom of foundation to be well-defined! (consider a $y$ satisfying $y = \{ x, y \}$) I, personally, would have more confidence in being correct if I was trying to develop the properties of ordered pairs from definitions 2 or 4, rather than from 1 or 3.