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?

9more comments