In Presburger Arithmetic there is no predicate that can express divisibility, else Presburger Arithmetic would be as expressive as Peano Arithmetic. Divisibility can be defined recursively, for example D(a,c) := exists b: M(a,b,c), M(a,b,c) := M(a-1,b,c-b), M(1,b,c) := (b=c). But some predicates which *can* be expressed in Presburger Arithmetic also have recursive definitions, for example P(x,y,z) := (x+y=z) versus P(x,y,z) := P(x-1,y+1,z), P(0,y,z) := (y=z).

How to tell if a predicate, defined recursively without use of multiplication, has an equivalent non-recursive definition which can be expressed in Presburger Arithmetic?