nLab pairing structure

Redirected from "ordered pairing structure".

Contents

Definition

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

References

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