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

  • $\begingroup$ What are $x,y$ in the axiom of pairing? $\endgroup$
    – Asaf Karagila
    Nov 21 '12 at 12:26
  • $\begingroup$ Is the first plan to have a two-sorted theory, with sets as one sort and ordered pairs (relations) as another sort -- with distant echoes of Principia? $\endgroup$ Nov 21 '12 at 15:06
  • $\begingroup$ @AsafKaragila These theories are intended to be single sorted, so $x$, $y$ in the axiom of pairing are pairs themselves (because every object of this theory is called a pair). I see that the textual description "If $x$ and $y$ are pairs..." is misleading, and will correct it. $\endgroup$ Nov 21 '12 at 16:11
  • $\begingroup$ So does that mean it should be $\forall x\forall y$? I'm not clear about what are the objects you try to model, and what sort of theory you are trying to write for them. $\endgroup$
    – Asaf Karagila
    Nov 21 '12 at 16:12
  • $\begingroup$ @AsafKaragila You are right, the axioms of ZF always use $\forall$ qualifiers for all free variables in the axioms, so I should have done the same. If it were possible, the theory should model "pairs" as they could be use as a "universal data structures" in a programming language. So there should be a finite number of atoms (I know how to achieve this), and each pair should be recursively defined as a pair of previously defined pairs or atoms (I believe that a first-order theory can't achieve this completely, and has to settle for something similar to PA). $\endgroup$ Nov 21 '12 at 17:06

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.

  • $\begingroup$ I think the proposed axiom schema basically says that there are no recursive containment loops. My reasoning for this conclusion is that I try $z=x_n$ for $\exists z$. Then the only time the axiom says anything non-trivial is if there is a recursive containment loop. (Hence it should be possible to simplify the axiom schema, omit the $\exists z$ part and directly use $z=x_n$.) I hope that it is possible to prove this "sentence schema" from the axiom schema of induction, i.e. that it is not required to have this "sentence schema" as an additional axiom schema. $\endgroup$ Nov 22 '12 at 8:28
  • $\begingroup$ @Thomas: You may be right on the first part. It seems to stand for reason to require that $x_n$ is "atomic" in the chain (namely it is equal to any of its predecessors if and only if it is an atom); and the idea is indeed to ensure there is no recursive loop -- much like the axiom of foundation. As for the second part, I will be quite surprised if that would happen. $\endgroup$
    – Asaf Karagila
    Nov 22 '12 at 8:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.