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.