I find many references to Gödel's pairing function on ordinals but I have not found a definition. What is it?
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 wellorder, 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 orderbymaximum part of the definition is precisely to ensure that the order is setlike; the lexical order itself is not setlike 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 wellordered 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.

$\begingroup$ Thanks. The absoluteness is just the kind of thing I wanted to check from the definition. $\endgroup$ – Colin McLarty Nov 11 '12 at 16:15

$\begingroup$ I think that this coding is how Zermelo proved that $\aleph_\alpha\times\aleph_\alpha=\aleph_\alpha$. I'm not sure whether or not it was his discovery or someone else's and it can probably be checked in his 1904 paper. $\endgroup$ – Asaf Karagila Nov 11 '12 at 16:26

$\begingroup$ Maybe the ordinal pairing functions are called Gödel coding not because Gödel invented this particular ordinal pairing function, but rather just because it is analogous to Gödel coding of sequences? $\endgroup$ – Joel David Hamkins Nov 11 '12 at 16:32

$\begingroup$ Okay, according to Jech Set Theory historical notes the ordering is due to Hessenberg (from his book  which I couldn't find  "Grundbegriffe der Mengenlehre", 1906). $\endgroup$ – Asaf Karagila Nov 11 '12 at 16:56

$\begingroup$ I have not checked the original sources, but I guess that Godel's pairing function is the inverse of this function described by Joel Hamkins. This inverse have a direct description in Shoenfield's Mathematical Logic, page 251. This (inverse) function is used by Shoenfield in the definition of the constructible model. One place to look is Godel's book on constructible sets and the consistency of GCH. $\endgroup$ – Rodrigo Freire Nov 11 '12 at 22:07
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$.

$\begingroup$ In case it isn't clear: this is exactly the same order and coding as in my answer. $\endgroup$ – Joel David Hamkins Nov 11 '12 at 17:57

$\begingroup$ Yes, I only saw Joel's answer after posting my own. It is not hard to see that we describe the same order. $\endgroup$ – Asaf Karagila Nov 11 '12 at 18:16
Asaf and Joel have answered the question. Let me add a remark that expands the fact that it helps us prove that $\kappa\times$ and $\kappa$ have the same size. All the claims here can be verified rather easily. Multiplication and exponentiation are in the ordinal sense.
It is customary to write $\Gamma(\alpha,\beta)$ for the order type of the predecessors of $(\alpha,\beta)$ under the order than Asaf denotes $\prec$. For example, $\Gamma(\omega,\omega\cdot2)=\omega^2+\omega$.
An ordinal $\alpha$ is (additively) indecomposable iff $\alpha\gt 0$ and whenever $\beta,\gamma\lt\alpha$, then $\beta+\gamma\lt \alpha$. One can easily check that the indecomposable $\alpha$ are precisely those of the form $\omega^\beta$. Say that $\alpha$ is multiplicatively indecomposable iff $\alpha>0$ and $\beta\gamma\lt \alpha$ whenever $\beta,\gamma\lt\alpha$. Then $\alpha$ is multiplicatively indecomposable iff it is $1$ or has the form $\omega^{\omega^\beta}$.
Ok, we can now state the remark; unfortunately I would not know who to credit for this observation, I think of it as folklore: An ordinal $\alpha$ is multiplicatively indecomposable iff it is closed under Gödel pairing, that is, $\Gamma(\beta,\gamma)\lt\alpha$ whenever $\beta,\gamma\lt\alpha$. In particular, $\Gamma(\kappa,\kappa)=\kappa$ for any infinite cardinal $\kappa$, which of course implies that $\kappa\times\kappa$ and $\kappa$ have the same size. Also, if $\kappa$ is uncountable, then there are $\kappa$ ordinals $\alpha$ below $\kappa$ such that $\Gamma(\alpha,\alpha)=\alpha$. Of course, all of this works well in $\mathsf{ZF}$ and all the definitions involved are absolute.
I prefer a different approach when verifying that $\kappa\times\kappa$ and $\kappa$ have the same size, one that (again) is absolute and goes through in $\mathsf{ZF}$, but only requires the use of additively indecomposable ordinals: One first checks that there is a (recursive) bijection $h:\omega\times\omega\to\omega$ with $h(0,0)=0$. Then, given ordinals $\alpha,\beta$, use their Cantor's normal form to write them as $$ \alpha= \omega^{\alpha_1}n_1 + \omega^{\alpha_2}n_2 + \dots + \omega^{\alpha_k}n_k $$ and $$ \beta= \omega^{\alpha_1}n'_1 + \omega^{\alpha_2}n'_2 + \dots + \omega^{\alpha_k}n'_k $$ where $\alpha_1 \gt \alpha_2 \gt \dots \gt \alpha_k$ are ordinals, and $n_1,\dots,n_k, n'_1,\dots,n'_k$ are natural numbers. (Note that these representations are not unique, but at least one of $n_i$ and $n_i'$ is nonzero iff $\alpha_i$ appears as an exponent in the canonical form of $\alpha$ or $\beta$).
Now set $$ H(\alpha,\beta)=\omega^{\alpha_1}h(n_1,n'_1)+\omega^{\alpha_2}h(n_2,n'_2)+\dots+ \omega^{\alpha_k}h(n_k,n'_k). $$ Then $H$ is a bijection between $\alpha\times\alpha$ and $\alpha$ whenever $\alpha$ is indecomposable. And an easy inductive argument, appealing to the explicit proof of SchröderBernstein, allows us to use $H$ to argue that there is, provably in $\mathsf{ZF}$, a class function that assigns to each infinite ordinal $\alpha$ a bijection between $\alpha\times\alpha$ and $\alpha$.
(Of course, the existence of this class function can also be argued from $\Gamma$, using that there are $\kappa$ ordinals $\alpha$ below $\kappa$ with $\Gamma(\alpha,\alpha)=\alpha$, but this second approach is somewhat easier.)
I found this argument a while ago, but then saw that Levy gives essentially the same approach in his textbook on set theory. Again, I am not sure who to credit for this construction, it seems to go back to Gerhard Hessenberg's 1906 book, "Grundbegriffe der Mengenlehre".

$\begingroup$ In the comments to Joel's answer I wrote that Jech attributes this proof to Hessenberg. $\endgroup$ – Asaf Karagila Nov 11 '12 at 17:02

$\begingroup$ It is basically the same idea as the Hessenberg (commutative) addition operation on ordinals. For that, you sort the two Cantor normal forms to have the same terms, as here, and just add coordinatewise. The twist for coding is not to just add the similar terms, but also to apply a natural number pairing function also. $\endgroup$ – Joel David Hamkins Nov 11 '12 at 18:09

$\begingroup$ Hmm... the attribution seems right. I have not seen Hessenberg's book, but Oliver Deiser's "Einführung in die Mengenlehre" describes Hessenberg's argument in page 301, and it is reasonably close to the one above. $\endgroup$ – Andrés E. Caicedo Nov 11 '12 at 18:09

1$\begingroup$ Thanks Asaf and Joel! I didn't expect this argument to go back this far. $\endgroup$ – Andrés E. Caicedo Nov 11 '12 at 18:10