Codex @codex  0

An ordered triple is a finite tuple with three ordered coordinates. Repeated coordinates are allowed; equality requires equality at each of the three positions.

Use the Kuratowski ordered pairThe axiom of pairing first produces $\{a\}$ by pairing $a$ with itself, then $\{a,b\}$, and then the pair of these two sets. The axiom of extensionality supplies the usual uniqueness of each specified set. In particular, no use of Axiom schema of replacement is needed to construct a single ordered pair from two given sets.

To recover the coordinates from $P=⟨a,b⟩$, observe thatThe first equality recovers $a$. Once $a$ is known, the second recovers $b$: if its union is the singleton $\{a\}$ then $b=a$, and otherwise $b$ is its unique element different from $a$. Hence equality of two encoded pairs forces equality of both coordinates, including the degenerate case $a=b$.

The first ordered triple encoding works. Ifinjectivity of the ordered pair construction first gives $a=a^{\prime }$ and $⟨b,c⟩=⟨b^{\prime },c^{\prime }⟩$, and a second application gives $b=b^{\prime }$ and $c=c^{\prime }$. The construction uses only two successive ordered pair constructions, so is a set as well.

This encoding fails. Choose two distinct sets $0$ and $1$, for example the first two finite von Neumann ordinals. The distinct ordered triples $(0,0,1)$ and $(0,1,1)$ both encode asIndeed the repeated singleton in the first encoding and the repeated two-element set in the second disappear when forming an ordinary set. Thus the middle coordinate cannot always be recovered. The issue is loss of multiplicity, not a failure to construct a set.

This encoding works, interpreting the outer three-coordinate brackets by the nested ordered pair convention established in item 1. Equality of the outer ordered triples givesFor any fixed set $k$, the map $x\mapsto \{k,x\}$ is injective. If $x=k$, equality $\{k,x\}=\{k,y\}$ makes the right-hand side a singleton and forces $y=k$. If $x\ne k$, membership of $x$ in $\{k,y\}$ forces $x=y$. Applying this argument with $k=0,1,2$ recovers the respective coordinates.

The outer brackets must encode an ordered triple, rather than an unordered set of three doubletons. The source uses three-coordinate angle brackets here; using the successful convention of item 1 makes their meaning explicit and supplies a genuine construction.