A characterisation of the relations definable in presburger arithmetic

Abstract

Four sub-recursive classes of functions, , , and are defined, and compared to the classes G 0, G 1 and G 2, originally defined by Grzegorczyk, based on bounded minimalisation, and characterised by Harrow in [5]. is essentially G 0 with predecessor substituted for successor; is G 1 with (truncated) difference substituted for addition. We prove that the induced relational classes are preserved ( and ). We also obtain (the quantifier free fragment of Presburger Arithmetic), and , and , where is G 2 with integer division and remainder substituted for multiplication, and where is known to be equal to the predicates definable by a bounded formula in Peano Arithmetic. © 2008 Springer-Verlag Berlin Heidelberg.