Presburger arithmetic and recognizability of sets of natural numbers by automata: New proofs of Cobhamʹs and Semenovʹs theorems Original Research Article

Let View the MathML source be the set of nonnegative integers. We show the two following facts about Presburgerʹs arithmetic: 1. 1. LetView the MathML source. If Lis not definable in 〈View the MathML source, +〉 then there is anView the MathML source definable in View the MathML source, such that there is no bound on the distance between two consecutive elements ofL′. (Actually we give in Theorem 3.7 two explicit sets one of which can be chosen to be L′) and 2. 2. View the MathML source is definable in 〈View the MathML source, +〉 if and only if every subset ofView the MathML sourcewhich is definable inView the MathML sourceis definable in 〈View the MathML source, +〉. (Theorem 5.1) These two Theorems are of independent interest but we will get from them new proofs of Cobhamʹs and Semenovʹs Theorems (Cobhamʹs Theorem being the case n = 1 of Semenovʹs Theorem); Semenovʹs Theorem is: Let k and l be multiplicatively independent (i.e have no nondashtrivial common power). If View the MathML sourceis definable inView the MathML sourceand inView the MathML sourcethenLis recognizable (i.e definable in 〈View the MathML source, +〉). Here Vm is the function which sends a nonzero natural number to the greatest power of m dividing it.