Decidability of the theory of the natural integers with the cantor pairing function 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 integers equipped with the Canter pairing function and an extra relation or function X on N. When X is equal either to multiplication, or coprimeness, or divisibility, or addition or natural ordering, it can be proved that the theory 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 Science B.V. All rights reserved.