I find many references to Gödel's pairing function on ordinals but I have not found a definition. What is it?



What is Gödel's pairing function on ordinals?
Define an order on pairs of ordinals $(\alpha,\beta)$ by ordering first by maximum, then by first coordinate, then by second coordinate. That is, one pair preceeds another if the maximum is smaller, or they have the same maximum and the first coordinate is smaller, or they have the same maximum and first coordinate, but the second coordinate is smaller. This is clearly a linear order, and it is a well-order, since none of these three quantities can descend infinitely. Furthermore, every proper initial segment of the order is a set, consisting of pairs with the same or smaller maximum (and indeed, the reason for using the order-by-maximum part of the definition is precisely to ensure that the order is set-like; the lexical order itself is not set-like on Ord). 


Thus, every pair $(\alpha,\beta)$ is the $\xi$ th element in this order for some unique $\xi$, we may view $\xi$ as the code of $(\alpha,\beta)$. Every pair has a unique code and every ordinal is a code.


This pairing function is highly robust and absolute, since the definition of the order is absolute to any model of even very weak set theories that contain those ordinals. Another attractive feature is that whenever $\kappa$ is an infinite cardinal (or even merely a sufficiently indecomposable ordinal), then $\kappa$ is closed under pairing, in the sense that any pair of ordinals below $\kappa$ is coded by an ordinal below $\kappa$. This is how we know $\kappa^2=\kappa$ for well-ordered cardinals. In particular, this method of coding also works on natural numbers. 


But I'm unsure if this coding is due to Gödel or was known earlier (perhaps even Cantor?); so it may not be the answer you seek.


