A Characterisation of the Relations Definable in Presburger Arithmetic

Four sub-recursive classes of functions,

${\mathcal{B}}$

,

${\mathcal{D}}$

,

${\mathcal{BD}}$

and

${\mathcal{BDD}}$

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].

${\mathcal{B}}$

is essentially

G

0

with

predecessor

substituted for

successor

;

${\mathcal{BD}}$

is

G

1

with

(truncated) difference

substituted for

addition

. We prove that the induced relational classes are preserved (

$G^0_\star={\mathcal{B}}_\star$

and

$G^1_\star={\mathcal{BD}}_\star$

). We also obtain

${\mathcal{D}}_\star={{{\mathfrak{PrA}}^{\text{\tiny qf}}}_\star}$

(the quantifier free fragment of Presburger Arithmetic), and

${\mathcal{BD}}_\star={\mathfrak{PrA}}_\star$

, and

${\mathcal{BDD}}_\star=G^2_\star$

, where

${\mathcal{BDD}}$

is

G

2

with

integer division

and

remainder

substituted for

multiplication

, and where

$G^2_\star$

is known to be equal to the predicates definable by a bounded formula in

Peano Arithmetic

.