P. Cegielski et D. Richard, Decidability of the theory of the natural integers with the cantor pairingfunction and the successor, THEOR COMP, 257(1-2), 2001, pp. 51-77
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.