What kind of algebra is the class of ordered pairs equipped with the binary operation which forms them?

Question

There are many definitions of ordered pair in set theory, but all such definitions have the characteristic property of ordered pair:

$ \ \ \ \ \ \ (x, y) = (x', y') \leftrightarrow \ (x = x' \ and \ y = y')\ \ \ \ $(*)

The comma in the expression "$(x, y)$" can be treated as a binary operation over sets resulting in an ordered pair. My question is about this operation. The term "$(x, y)$" can be an operation symbol of the language of a set theory T, and my question is easier to be answered for this case, than for the case when this operation is defined by a concrete definition (Kuratowski's, Wiener's, etc.). Thus, what kind of algebra is "$(U, \ (x, y))$", where U denotes the universe of discourse of a set theory T, and "$(x, y)$" is an operation symbol in the language of T?

To make the question correct, I would have to use such terms as "class-algebra", say that $U$ is a Grothendieck universe, or otherwise take care of foundations. But the question is about algebraic properties of this algebra and to keep focus on this, I would keep the aspect of "size" ("set" versus "class") fuzzy for now.

The property (*) is neither an identity, nor a quasi-identity - do algebraists handle such properties of a binary operation?

Here is one reason why this question is interesting. Set theory can be presented algebraically, but then it would be nice that the formulas of such an algebraic set theory are treated on same basis as their interpretations ("within the same universe of discourse"). A formula can be treated as result of multiple applications of the operation $(x, y)$ and, therefore, it would be nice to get an idea of the algebraic properties of this operation - whence my question.

I guess, the AST (Algebraic Set Theory) presented in the language ofcategory theory treats syntax on the same basis as semantics. But can my question be answered in the language of universal algebra?

Answer 1

The property (*) is actually equivalent to a set of quasi-identities: $$(x,y)=(x',y')\rightarrow x=x'$$ $$(x,y)=(x',y')\rightarrow y=y'$$ The converse implication you had ($\leftarrow$) is logically valid and hence does not need to be mentioned.

Answer 2

Since your algebra mixes together the objects $x$ and $y$ with their pair $(x,y)$ in the same algebra, it has the effect of erasing "ordered-pair" as a separate type in this context, and so there is no reason to expect that condition $(*)$ is all the structure one will expect to find. For example, in your algebra you can form iterated terms like $(x,(y,z))$ and inquire whether $x=(x,y)$ is possible, while in a more highly typed context, such an equation wouldn't even be sensible necessarily. For this reason, there are numerous pairing functions that exhibit all kinds of other extra algebraic structure in the algebra you are considering.

For example, many of the usual ordered-pair definitions in set theory have the property that $(x,y)$ has higher rank than $x$ and $y$, and in particular, $x\neq (x,y)\neq y$.

Similarly, for most of the pairing functions, $\emptyset\neq (x,y)$, and so these pairing function are never a bijection of $U\times U$ with $U$.

But there are other pairing functions that do constitute a bijection between $U\times U$ and $U$, and in this sense it would be correct to write $U\times U=U$. This would include some of the usual flat pairing functions one sees in set theory, where actually every set $x$ is $(y,z)$ for some $y$ and $z$, and so the pairing function is a bijection of $U\times U$ with $U$. Indeed, with the flat pairing functions I have in mind, $V_\theta\times V_\theta=V_\theta$ for any infinite ordinal $\theta$, and this includes all the Grothendieck universes you were considering.

One can easily design artificial pairing functions that have other extra properties, such as having fixed-point objects $x$ for which $x=(x,x)$ and hence $x=(x,(x,x))=(((x,x),x),x)$ and so on, or having no such fixed-points $x$. One could also make pairing functions that had various instances of finite cycles $x=(x,y)$, $y=(y,z)$ and $z=(z,x)$ and so on. One can easily arrange crazy stuff, since of course the only requirement that $(*)$ imposes is that $(\cdot,\cdot)$ is injective.

If $(x,y)$ is a pairing function and $\pi:U\to U$ is any injective function, then $(x,y)_\pi:=\pi((x,y))$ is another pariing function. And indeed, all pairing functions arise this way from any given surjective pairing function.

Answer 3

I am not sure but I believe up to isomorphism this kind of structure is indistinguishable from arbitrary embedding $A\times A\hookrightarrow A$.

Sort of related are the s. c. Jónsson-Tarski algebras --- when one requires that the above is actually a bijection. The latter are equational in the well known way, and play important rôles in various fields, being source of many interesting counterexamples.

Answer 4

Universal algebra prefers to use a language in which the class of algebras under investigation is equationally defined (in other words: is a variety). This is why groups are often not written as structures $(G,*)$ but rather as structures $(G,*, 1, {}^{-1})$. (Or, rarely, as structures $(G,/)$, where $x/y:= x*y^{-1}$.)

I think the situation is similar here. If you do not require the pairing function to be onto, then the (in my opinion) natural way to represent your structures as algebras is to equip them with unary functions $l$ and $r$, and require $l(x*y)=x$, $r(x*y)=y$. (I use $*$ rather than the comma as the pairing operation.)

This makes your family of "sets with a pairing function" into an equationally defined class.

Every algebra $(A,*)$ with a pairing function in your sense can be expanded to an algebra $(A,*,l,r)$ in my sense. This implies that the first order theory of "my" algebras (the consequences of the two laws I gave) is a conservative extension of the theory of "your" algebras. (However, I think that this theory is quite trivial.)

An even more natural way would be to declare $l$ and $r$ to be partial functions, but it seems to me that partial functions are not popular in universal algebra.

Of course, if you do require the pairing function to be onto, you have to add the axiom $l(z)*r(z) = z$, and get a Jónsson-Tarski algebra, as remarked in previous answers.