5
$\begingroup$

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

  • 0
    What are $x,y$ in the axiom of pairing?2012-11-21
  • 0
    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*?2012-11-21
  • 0
    @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.2012-11-21
  • 0
    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.2012-11-21
  • 0
    @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).2012-11-21
  • 0
    What are atoms? Are atoms just pairs whose elements are...? Yes, you will probably going to need an induction schema or replacement schema of some sort.2012-11-21
  • 0
    @PeterSmith Both theories are intended as single-sorted theories. The intention of the first theory was to model a pair as a "universal data structure" in a programming language. The intention of the second theory was to avoid meaningless theorems like http://us.metamath.org/mpegif/avril1.html caused by definitions like the ordered pairs which feel like "hacks". But all two-sorted theories (including pairs in set theory) I tried felt even more like "hacks" than ordinary ZF set theory. But the theory of s-pairs doesn't feel worse than ordinary ZF to me, and seems to do the trick.2012-11-21
  • 0
    It seems to me that unless you allow infinite branches, König's lemma means you can only get finite data structures out of this. But I suppose that's OK if you only want it to have the strength of PA... (The usual first-order way of asserting that some datatype can only be built from certain constructors is to add an induction schema. Of course, the existence of non-standard models precludes the possibility of a completely satisfactory axiomatisation...)2012-11-21
  • 0
    Your atoms axiom as it stands is wrong. It says that every element is an atom. You should say that there exists $x_1,\ldots, x_n$ which are mutually unequal, and each is an atom on its own.2012-11-21
  • 0
    @AsafKaragila The atom axiom just says that a pair is equal to its left part if and only if it is equal to its right part. But the logic behind this axiom starts with the question what should be the left and right part of an atom. If it were the empty set, we would run into trouble with the axiom of extensionality. Hence the most useful definition seems to be that the left and right part of an atom are identical to the atom itself. Now we just need an axiom that allows us to turn this property into a convenient definition of what it means for a pair to be an atom.2012-11-21
  • 0
    It seems plausible that you could get away with a unique atom: if we use the Gödel unpairing function on $\mathbb{N}$ then the only number which is represents an atom is $0$.2012-11-22
  • 0
    Ah, yes. I wasn't careful when I read the axiom!2012-11-22
  • 0
    @AsafKaragila If I just have a single atom, it will be the empty set and I don't care to name it. So the axioms $\forall x \forall y((l(x)\equiv x \land l(y)\equiv y) \Rightarrow x \equiv y)$ and $\exists x l(x)\equiv x$ could be used. However, if there are more than one atom, I probably just want to add them as constants to my alphabet. I guess the theory won't change in any significant way whether I have a single atom or a given fixed finite number of atoms.2012-11-22
  • 0
    You may want to add axioms for well-foundedness, and that there exists an atom (which would be compatible with the existence of many atoms).2012-11-22
  • 0
    I wonder if it would be better to write down a theory of ordered sets or ordered multi-sets (i.e. lists) instead of merely ordered pairs?2012-11-22
  • 0
    @AsafKaragila The axioms for well-foundedness is actually exactly the point were I get lost. The thing which I don't fully understand is that I can get well-foundedness for first-order set theory (and I guess also for first order s-pair theory), but apparently not for first-order pair theory. The obstacle seems to be that the theory would characterize a countable set otherwise, which is not possible for a first-order theory. So I have to fall back to something like the axiom schema of induction, and try to understand its consequences. (Note that I edited the question to use this axiom schema.)2012-11-22
  • 0
    Yes, well-foundedness seems like something difficult to achieve with such a limited expressibility. Note, however that you are aiming for PA, and PA cannot express internal well-foundedness as well (although it cannot disprove it either). I think that the key issue is the fact that you have two predicates instead of just one which expresses membership, and that you only allow collections of two elements at a time. You might want to add an axiom schema which asserts well-foundedness, in such case.2012-11-22
  • 0
    @Hurkyl If I would model ordered multi-sets similar to lisp lists, all I would have to change is replace the functions $l$ and $r$ (for left and right) by $h$ and $t$ (for head and tail), add a constant $e$ to the alphabet (for the empty list) and modify the definitions/axioms for atoms such that the head of an atom is identical to the atom itself and the tail of an atom is the empty list. I haven't thought about how to turn the theory of s-pairs into a theory of s-lists, but I guess your suggestion wasn't meant to apply to that part.2012-11-22
  • 0
    @Thomas: I was thinking more along the lines of arbitrary-length lists, rather than finite or countable-length lists.2012-11-24
  • 0
    @Hurkyl An arbitrary length list would be a function from an index set to the "universe". In fact, while searching for such a theory, I found out that von Neumann proposed such a [theory](http://books.google.de/books?id=v4tBTBlU05sC&pg=PA393&source=gbs_toc_r&cad=3#v=onepage&q&f=false) in 1925, and that it actually was the first "correct" axiomatization of set theory and "backported" to ZFC. Paul Bernays modified Von Neumann's theory so as to make sets and set membership primitive, and this became NBG. Gödel used this theory for his investigations of the continuum hypothesis.2012-11-25
  • 0
    The proposition "I could define that an s-pair p is a pair if its left and right part contain no more than one element" should better be "I could define that an s-pair p is a pair if its left and right part contain exactly one element", because otherwise it wouldn't correctly model the notion of a pair. However, I first want to better understand the two theories (for example the consequences of the induction scheme for the first, or what happens if I use a NBG axiomatization for the second) before editing the question again, after which I will delete this comment.2012-11-26

1 Answers 1