14
$\begingroup$

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) \equiv \exists b \: M(a,b,c)$, $M(a,b,c) \equiv M(a-1,b,c-b)$, $M(1,b,c) \equiv (b=c)$. But some predicates which can be expressed in Presburger Arithmetic also have recursive definitions, for example $P(x,y,z) \equiv (x+y=z)$ versus $P(x,y,z) \equiv P(x-1,y+1,z)$, $P(0,y,z) \equiv (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?

$\endgroup$
2
  • $\begingroup$ The answers by Joel and Michaël are very informative and helpful to me. I noticed that P can be defined tail-recursively without addition, using only the successor function: P(x,y,z) := (x=0 and y=z) or exists w: S(w)=x and P(w,S(y),z), but it seems impossible to define M this way. Is there any principle (or rule of thumb) by which I can know that the recursive definition of P is well-founded but that of M is not? $\endgroup$ Sep 5, 2010 at 23:20
  • 4
    $\begingroup$ The issue is not that the definition of M is not well founded. The way you would actually define a "recursively defined function" in Peano Arithmetic is by quantifying over finite sequences that trace the computation of the function step by step. This is necessary because the language of arithmetic does not include a fixed-point combinator or recursor combinators to facilitate recursive definitions of functions. Presburger arithmetic is too weak to quantify over finite sequences, which is why recursively defined functions such as multiplication-from-addition cannot be defined there. $\endgroup$ Sep 6, 2010 at 12:19

3 Answers 3

24
$\begingroup$

Presburger arithmetic admits elimination of quantifiers, if one expands the language to include truncated minus and the unary relations for divisibility-by-2, divisibility-by-3 and so on, which are definable in Presburger arithmetic. (One can equivalently expand the language to include congruence $\equiv_k$ modulo $k$ for each natural number $k$.) That is to say, every assertion in the language of Presburger arithmetic is equivalent to a quantifier-free assertion in the expanded language.

It follows that the definable subsets of $\mathbb{N}$ in the language of Presburger arithmetic are exactly the eventually periodic sets. These are comparatively trivial sets, of course, and it means that the set of prime numbers and other interesting sets of natural numbers are simply not expressible in the language of Presburger arithmetic. A similar analysis holds in higher dimensions, and for this reason, we usually think of Presburger arithmetic as a weak theory.

The quantifier elimination argument leads directly to the conclusion that Presburger arithmetic is a decidable theory: given any sentence, one finds the quantifier-free equivalent formulation, and such sentences are easily recognized as true or false.

There is an interesting account in these slides for a talk by Cesare Tinelli.

$\endgroup$
1
  • $\begingroup$ I think quantifier elimination must be the only way to do what I want. $\endgroup$ Sep 8, 2010 at 4:53
23
$\begingroup$

Presburger Arithmetic (over the naturals) describes exactly the semi-linear sets. A set ($\subseteq \mathbb{N}^k$) is linear if it can be expressed as $$L(\vec c, P=\{\vec{p_1}, \ldots, \vec{p_n}\}) = \{ \vec c + \sum_{i=1}^pc_i\vec{p_i} \;|\; c_i \in \mathbb{N}\}.$$

A set is semi-linear if it can be expressed as a finite union of linear sets. One can deduce a few techniques from this characterization (due to Ginsburg & Spanier).

$\endgroup$
9
$\begingroup$

In addition to the answers above, it is worth mentioning that the existential fragment of Presburger arithmetic can actually be extended by a full divisibility predicate while retaining decidability [1]. Satisfiability in the resulting fragment is in NEXP, the lower bound being NP [2].

Also, it is possible to define a family of formulas $\Phi_n(x,m)$ such that for every natural number $m$ representable using $n$-bits, $\Phi_n(x,m)$ holds if and only if $x \equiv 0 \bmod m$ [3].

[1] L. Lipshitz, “The Diophantine problem for addition and divisibility,” Transactions of the American Mathematical Society, vol. 235, pp. 271– 283, 1976.

[2] Lechner, A.; Ouaknine, J.; Worrell, J., "On the Complexity of Linear Arithmetic with Divisibility," in Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 667-676, 2015.

[3] Haase, C., "Subclasses of Presburger arithmetic and the weak EXP hierarchy," in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (CSL-LICS '14). ACM, New York, NY, USA, Article 47, 2014.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.