Skip to main content
1 of 2
Asaf Karagila
  • 39.7k
  • 8
  • 135
  • 283

According to this .pdf file the definition is this:

Consider the canonical ordering on $\mathsf{Ord\times Ord}$: $$(\alpha,\beta)\prec(\gamma,\delta)\iff\begin{cases} \max\lbrace\alpha,\beta\rbrace\lt\max\lbrace\gamma,\delta\rbrace & \lor \\\ \max\lbrace\alpha,\beta\rbrace=\max\lbrace\gamma,\delta\rbrace\land\alpha\lt\gamma&\lor\\\ \max\lbrace\alpha,\beta\rbrace=\max\lbrace\gamma,\delta\rbrace\land\alpha=\gamma\land\beta\lt\gamma \end{cases}$$

The pairing function, if so, $G(\alpha,\beta)=\operatorname{otp}\lbrace(\gamma,\delta)\in\mathsf{Ord\times Ord}\mid(\gamma,\delta)\prec(\alpha,\beta)\rbrace$.

Asaf Karagila
  • 39.7k
  • 8
  • 135
  • 283