🚀 go-pugleaf

jamie@cs.sfu.ca (Jamie Andrews) writes:

>     Where can I expect to find easily a precise and elegant
>axiomatization of Presburger arithmetic?  (I know it's
>"arithmetic without multiplication" and I can think of some
>horrible axiomatizations; I wanted to find a nice one.)

In ZML 12 (1966), pp. 131 - 168, H. Apelt gives the following
axiom system for Presburger Arithmetic:

  a+b = b+a
  a+(b+c) = (a+b)+c
  \exists b  ( a+b = c  \or  c+b = a )
  c+a = c+b \to a=b
  a+b = 1 \to ( a=1 \or b=1 )
  a+b = 0 \to b=0
  \not 0=1

plus the schema

 \exists b ( b+...+b = a \or b+...+b+1 = a \or ... \or b+...+b+1+...+1 = a )
               p b's          p b's                     p b's  p-1 1's

for every prime number p.

>thanks
>--Jamie.

No matter

Jan Johannsen   jnjohann@immd1.informatik.uni-erlangen.de