Decision procedure in Presburger arithmetic

360 Views Asked by At

Suppose I want to decide whether the statement

$$\exists x.(x+x+x+1+1+1=1+1+1+1+1)$$

is part of the set of consequences of Presburger arithmetic. In more readable language, this is saying that

$$\exists x.(3x+3=5)$$

or

$$3 \equiv_3 5$$

Using some metatheory, it is easy to compute the remainder of $5-3$ after division by $3$ and discover that it is $2 \neq 0$ so that the original statement is false.

But if I wanted to prove this statement within Presburger arithmetic, would I be allowed to use the division algorithm?

Presburger arithmetic only defines the addition symbol $+$, and multiplication by constants is obtained by repeated addition. How does one express the division algorithm within Presburger arithmetic and prove that it terminates?

Perhaps there exists a sequence of steps that will show the falsehood of the statement within the system, but as far as Presburger arithmetic is concerned, this sequence of steps can only be arrived at by an ad-hoc manner, or using insight from the meta-theory.

Or am I misunderstanding something about what it means to say that Presburger arithmetic is complete? I am familiar with number theory but not so much with the formal logic.

1

There are 1 best solutions below

5
On BEST ANSWER

First, please note that in general, completeness is not the same as decidability. For example, first-order logic is complete, but not decidable.

Now, as it so happens, Presburger arithmetic is both complete and decidable.

For your particular statement, you'd show it to be false doing something like this:

Assuming the statement is true, we get that for some $a$:

$$a+a+a+1+1+1=1+1+1+1+1$$

Using Presburger axiom 2 that says:

$$\forall x \forall y (x+ 1 = y+1 \rightarrow x = y)$$

we thus obtain:

$$a+a+a=1+1$$

Now, using Presburger's inductive axiom 5:

$$(P(0) \land \forall x (P(x) \rightarrow P(x+1))) \rightarrow \forall y P(y)$$

you can show that:

$$\forall x \ (x = 0 \lor \exists y \ x = y + 1)$$

and thus we can infer:

$$a = 0 \lor \exists y \ a = y + 1$$

If $a=0$, we thus get:

$$0+0+0=1+1$$

Using axiom 3:

$$\forall x \ x + 0 = x$$

we obtain:

$$0 = 1 + 1$$

but that contradicts axiom 1:

$$\forall x \ \neg (0 = x +1)$$

On the other hand, if $\exists y \ a = y + 1$, then we get for some $b$:

$$a = b+1$$

and thus:

$$b+1+b+1+b+1=1+1$$

Now, using axioms 3,4, and 5 we can prove that:

$$\forall x \forall y \ x + y = y + x$$

and

$$\forall x \forall y \forall z \ x + (y + z) = (x + y) + z$$

both of which we can use to obtain:

$$b+b+b+1+ 1+1=1+1$$

Applying axioms 2 and 3:

$$b+b+b+1=0$$

and so that contradicts axiom 1 as well.

So, the assumption that your statement is true leads to a contradiction, and so it is in fact false.