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)?