Decidability of the theory of the natural integers with the cantor pairingfunction and the successor

The binary Canter pairing function C from N x N into N is defined by C(x, y ) = (1/2)(x +y) (x + y + 1) + g:. We consider the theory of natural integer s equipped with the Canter pairing function and an extra relation or functi on X on N. When X is equal either to multiplication, or coprimeness, or div isibility, or addition or natural ordering, it can be proved that the theor y Th(N, C,X) is undecidable. Let S be the successor function. We provide an algorithm solving the decision problem for Th(N,C,S). (C) 2001 Elsevier Sc ience B.V. All rights reserved.