pairing function

we define the primitive recursive function if is any given number, there is a unique solution to the equation

namely, is the largest number such that , and is then the solution of the equation

this last equation has a (unique) solution because must be odd. (the twos have been "divided out.") eq-pairing-function-1 thus defines functions since eq-pairing-function-1 implies that we have hence we can write

so that are primitive recursive functions.

the definition of can be expressed by the statement the properties of the functions , and are summarized in the-pairing-func.