Set theory like first-order theory of ordered pairs The widely-accepted Kuratowski definition of an ordered pair is $(a,b):=\{\{a\},\{a,b\}\}$. This definition makes perfect sense in the context of first-order set theory. However, how would a first-order theory using ordered pairs as basic notion look like?
My first try used the alphabet $S_{pair}=\{l,r\}$, where $l$ and $r$ are unary function symbols.


*

*Axioms of atoms The left and right part of an atom $x$ are the same as $x$ itself. A pair is an atom if it is the same as its left or right part:
$$\forall x(l(x) \equiv x \Leftrightarrow r(x) \equiv x)$$
Let $Ax$ be an abbreviation for $(l(x) \equiv x \lor r(x) \equiv x)$, i.e. $Ax$ if and only if $x$ is an atom.

*Axiom of extensionality Two pairs $x$ and $y$ are equal (or $x$ or $y$ is an atom) if their left and right parts are the same:
$$\forall x \forall y ((l(x) \equiv l(y) \land r(x) \equiv r(y)) \Rightarrow (x \equiv y \lor Ax \lor Ay))$$

*Axiom of pairing For two pairs $x$ and $y$, there exists a pair $z$ (which is not an atom) with $x$ and $y$ as left and right part:
$$\forall x \forall y \exists z(\lnot Az \land l(z) \equiv x \land r(z) \equiv y)$$

*Axiom schema of induction For each formula $\phi(x,y_1,...,y_k)$ in the language of pairs, the first-order induction axiom holds, i.e. $\phi(x,\bar{y})$ with $\bar{y}=y_1,...,y_k$ is true for all pairs $x$, if it is true for all atoms $x$, and true if it is true for the left and right part of $x$:
$$\forall \bar{y}((\forall x (Ax \Rightarrow \phi(x,\bar{y})) \land$$ $$\forall x((\phi(l(x),\bar{y})\land \phi(r(x),\bar{y})) \Rightarrow \phi(x,\bar{y})))$$
$$\Rightarrow \forall x \phi(x,\bar{y}))$$


I could add another axiom to ensure that there exists exactly one atom (which would then be the empty pair), but this wouldn't change the resulting theory significantly. I wonder more whether the axiom schema of induction as given above will achieve what I intent. (Note While trying to prove this, I discovered that the axioms were "buggy", which I tried to fix by introducing the abbreviation $Ax$ and using it appropriately.)
Question Will the  first-order theory of pairs given above have the same "consistency strength" as PA, if we additionally ensure that there is only a given fixed finite number of atoms by an additional axiom? Will the resulting theory be equivalent to PA in a certain way?

An alternative idea for an axiomatic first-order theory of pair would be to take ordered pairs of sets as basic objects (s-pairs for short), and define pairs and sets in terms of these s-pairs. I could use the alphabet $S_{s-pair}=\{\in,\ni\}$ where $\in$ and $\ni$ would be binary relation symbols. I could define that an s-pair $p$ is a pair if its left and right part contain no more than one element ($\forall x \forall y(((x \in p \land y \in p) \lor (p \ni x \land p \ni y)) \Rightarrow x \equiv y)$). The most symmetric definition for a set seems to be to define that an s-pair $s$ is a set if its left and right part contain the same elements ($\forall x(x\in s \Leftrightarrow s \ni x)$).
However, now the question arises how to best "convert" the ZF axioms of set theory into similar axioms for s-pairs. Perhaps it would already be sufficient to only modify the axiom of extensionality, leave all the other axioms to refer only to $\in$, and only add one axiom allowing to regroup left and right parts, like 
$$\forall l \forall r \exists p(\forall x(x \in p \Leftrightarrow l \ni x)\land\forall y(p \ni y \Leftrightarrow y \in r))$$
Question The thing with the s-pairs described above seems closely related to surreal numbers and Conway games. Is there some place where such a first-order theory is described in sufficient detail? Does the above construction works more or less and gives a theory with the same "consistency strength" as ZF, or are there significant differences to ZF that I overlooked (i.e. which prevent such a theory from having similar properties as ZF)?
 A: The theory is not very expressive, it only allows ordered pairs, which is not too much to work with (compared to set theory which allows sets of an unlimited size).
To add well-foundedness, one can suggest using the following schema:

For every $n\in\omega$ we write the following axiom: $$\forall x_1\dots\forall x_n\Bigg(\bigwedge_{i=1}^{n-1}\Big(l(x_i)\equiv x_{i+1}\lor r(x_i)\equiv x_{i+1}\Big)\rightarrow\exists z\Big(\bigvee_{i=1}^n\big(z\equiv x_i\big)\land\bigwedge_{i=1}^n\big(l(z)\equiv x_i\lor r(z)\equiv x_i\rightarrow z\equiv x_i\big)\Big)\Bigg)$$

This schema says that whenever we have a decreasing sequence, there is an element which is an atom (this is comparable to the axiom of foundation which implies [and is probably equivalent to] "the transitive closure of every set contains the empty set").
One caveat is that I don't know how this schema is going to work in the context of non-standard integers, but let us assume for starters that the model is nice and fine and dandy. All the integers are standard etc.
