Definability in terms of the successor function and the coprimeness predicate in the set of arbitrary integers
Denis Richard · Journal of Symbolic Logic · 1989
Abstract Using coding devices based on a theorem due to Zsigmondy, Birkhoff and Vandiver, we first define in terms of successor S and coprimeness predicate ⊥ a full arithmetic over the set of powers of some fixed prime, then we define in the same terms a restriction of the exponentiation. Hence we prove the main result insuring that all arithmetical relations and functions over prime powers and their opposite are {S, ⊥}-definable over Z. Applications to definability over Z and N are stated as corollaries of the main theorem.