If one wishes to introduce ordered pairs to ZFC as a new sort, rather than constructing them as sets (e.g., using the Kuratowski pairing function) within ZFC, it is possible to add a binary function symbol, e.g., "$g$", which given any pair of objects, returns an object of type "ordered pair."

One then includes the axiom that the output of $g$ satisfies the characteristic property of the ordered pair, i.e., that for all objects $a_1$, $a_2$, $b_1$, and $b_2$, $g(a_1,a_2) = g(b_1, b_2)$ if and only if $a_1 = a_2$ and $b_1 = b_2$.

However, is it also necessary to include as an axiom that ordered pairs exist? Terence Tao writes on page 62 of Analysis I, where he defines ordered pairs,

Strictly speaking, this definition is partly an axiom, because we have simply postulated that given any two objects $x$ and $y$, that an object of the form $(x, y)$ exists.

Similarly, Robert Wolf writes as the fourth of the "Set axioms" listed in Appendix 1, A General-Purpose Axiom System for Mathematics, on page 372 of Proof, Logic, and Conjecture / The Mathematician's Toolbox,

For every $x$ and $y$, the ordered pair $(x,y)$ exists.

But isn't that $g(a,b)$ exists for all objects $a$ and $b$ implicit in the fact that $g$ is defined as a binary function symbol? For example, in Peano arithmetic, with the unary successor function symbol $S$, I don't think it's necessary to explicitly axiomatize that $S(n)$ exists for all natural numbers $n$--isn't this implicit in the fact that $S$ is a unary function symbol?

  • $\begingroup$ The correct analogy in your $S(n)$ example is that I must know $n$ exists before I can consider $S(n)$. If you introduce the function $g(a,b)$ (which might more accurately be written as $g((a,b))$, then what is it defined on? What am I allowed to put into it? What is $(a,b)$? $\endgroup$ – kccu May 13 '17 at 14:05

No. If you have a function symbol, then it is implicit that any terms that you can produce with it exists and well-defined when you interpret the term.

Specifically, if $g$ is the symbol of your ordered pair operator, and $M$ is a structure to your language $\{\in,g\}$, then you require that $g$ is defined on $M^2$, so for every $x,y\in M$, $g(x,y)$ is some element of $M$, which in other words means that it exists.

  • $\begingroup$ The question seems to be more whether we need to postulate that $(x,y)$ exists (i.e., $M^2$ exists) before we can talk about $g$ or $g(x,y)$. $\endgroup$ – kccu May 13 '17 at 14:30
  • 2
    $\begingroup$ That is not part of the theory at all. That is part of the meta-theory. $\endgroup$ – Asaf Karagila May 13 '17 at 14:33

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.