nLab pairing structure



Pairing structure

Given a set VV with an extensional relation \prec on VV, a pairing structure is a binary function P:V×VVP:V \times V \to V such that

  • for all aVa \in V and bVb \in V, aP(a,b)a \prec P(a, b) and bP(a,b)b \prec P(a, b)

Unordered pairing structure

An unordered pairing structure on VV is pairing structure {,}:V×VV\{-,-\}:V \times V \to V where additionally

  • for all sets zz, z{x,y}z \in \{x, y\} implies that z=xz = x or z=yz = y.

Uniqueness of {x,y}\{x, y\} follows from \prec being an extensional relation.

Ordered pairing structure

An ordered pairing structure on VV is a pairing structure (,):V×VV(-,-):V \times V \to V which satisfies product extensionality:

  • for all aVa \in V, aVa' \in V, bVb \in V, bVb' \in V, P(a,b)=P(a,b)P(a, b) = P(a', b') if and only if a=aa = a' and b=bb = b'

Foundational concerns

In any material set theory, instead of postulating the mere existence of a set PP in which aPa \in P and bPb \in P one could add a primitive binary operation P(a,b)P(a, b) which takes material sets aa and bb and returns a material set P(a,b)P(a, b) such that for all aa and bb, aP(a,b)a \in P(a, b) and bP(a,b)b \in P(a, b)

See also


Last revised on December 15, 2022 at 22:50:33. See the history of this page for a list of all contributions to it.