A New Proof of a Theorem by Ginsburg and Spanier

Marcus Kracht

Department of Linguistics

UCLA 405 Hilgard Avenue

PO Box 951543

Los Angeles

CA 90095-1543

December 18, 2002

Abstract In [2], Ginsburg and Spanier showed that the semilinear subsets of n are exactly the sets that are definable in Presburger Arithmetic. The proof relied on two results shown in [1]: (1) that linear equations define semilinear sets, and (2) that the complement of a semilinear set is and the intersection of semilinear sets is again semilinear. Here we offer a much simpler proof of this fact. Basically, using quantifier elimination for Presburger Arithmetic we avoid having to show closure under negation. Instead, this will now follow from the results. Second, closure under intersection will be shown using standard techniques from linear algebra.

1  Preliminaries

Let n be the set of n–tuples of natural numbers. A tuple is denoted by an arrow, eg v, whose coordinates are vi, i<n. Put 0000. Define v+w by

( v + w ) ( i ) = v ( i ) + w ( i ) (1.1)

Denote the structure n,0¯,+ also by n. The unit vector which is 0 except at place number i. where it is 1, is denoted by ei. We define nv inductively as follows. 0v0¯, (n+1)vnv+v. We write v for the set {nv:n} and V+W{v+w:vV,wW}. A nonempty subset of n is called linear if it can be written as

v 0 + v 1 + v 2 + + v m (1.2)

for some m (which may be zero, in which case we get the singleton {v0}). Likewise, a subset of n(n) is called linear if it has the form

v 0 + v 1 + v 2 + + v m (1.3)

for subsets of n as well as

v 0 + v 1 + v 2 + + v m (1.4)

for subsets of n. The linear subset of n are nothing but the affine subspaces.

A subset of n(n,n) is called semilinear if it is the finite union of semilinear sets. We employ the following notation.

Definition 1.1. Let M and N be finite subsets of n. Then Σ(M:N) denotes the set of vectors of the form u+Σi<pkivi such that uM, ki and viN for all i<p.

Presburger Arithmetic is defined as follows. The basic symbols are 0, 1, +, < and m, m{0,1}. Then Presburger Arithmetic is the first order theory of the structure _01+<m:1<m, where ambiffab is divisible by m.

Negation can be eliminated.

¬ ( x y ) x < y y < x ¬ ( x < y ) x y y < x ¬ ( a m b ) 0 < i < m a m b + n _ (1.5)

where n_ is defined by 0_0, n+1_n_+1. We shall occasionally use xy for x<yxy. Moreover, multiplication by a given natural number also is definable: put 0t0¯, and (n+1)tnt+t. Every term in the variables xi, i<n, is equivalent to b+Σi<naixi, where b,ai, i<n. A subset S of n is definable if there is a formula ϕxox1xn1 such that

S = { k i : i < n n : _ ϕ k 0 k 1 k m 1 } (1.6)

The definable subsets of n are closed under union, intersection and complement and permutation of the coordinated. Moreover, if Sn+1 is definable, so is its projection

π n [ S ] { k i : i < n n : there is k n : k i : i < n + 1 S } (1.7)

The same holds for definable subsets of n, which are simply those definable subsets of n that are included in n. Clearly, if Sn is definable, so Sn.

2  Linear Equations

Lemma 2.1. Suppose that a+Σi<npixi=b+Σi<nqixi is a linear equation with rational numbers a, b, pi and qi(i<n). Then there is an equivalent equation g+Σi<nuixi=h+Σi<nvixi with positive integer coefficients such that g·h=0 and for every i<n:viui=0.

Proof First, multiply with the least common denominator to transform the equation into an equation with integer coefficients. Next, for every i<n, substract qixi from both sides pi>qi and pixi otherwise.

Call an equation reduced if it has the form

g + i < m k i x i = m i < n k i x i (2.1)

with positive integer coefficients g and ki, i<n. Likewise for an inequation. Evidently, modulo renaming of variables we can transform every rational equation into reduced form.

Lemma 2.2. The set of solutions of reduced equation is semilinear.

Proof Let μ be the least common multiple of the ki. Consider a vector of the form ci,j=(μ/ki)ei+(μ/kj)ej, where i<m and mj<n. Then if v is a solution, so is v+ci,j and conversely. Put C{ci,j:i<m,mj<n} and let

P { u : g i < m k i u ( i ) = m j < n k i u ( i ) , i < n : u ( i ) < μ / k i } (2.2)

Both P and C are finite. Moreover, the set of solutions is exactly Σ(P:C).

Lemma 2.3. The set of solutions of a reduced inequation is semilinear.

Proof Assume that the inequation has the form

g + i < m k i x i m i < n k i x i (2.3)

Define C and P as before. Let E{ei:mi<n}. Then the set of solutions is Σ(P:CE). If the inequation has the form

g + i < m k i x i m i < n k i x i (2.4)

the set of solutions is Σ(P:CF) where F{ei:i<m}.

Lemma 2.4. Let Mnbe an affine subspace. Then Mn is a semilinear subset of n.

Proof Let vi, i<n+1, be vectors such that

M = v 0 + v 1 + v 2 + + v m 1 (2.5)

We can assume that the vi are lineary independent. Clearly, since w=(λw) for any nonzero rational number λ, we can assume that vin, i<m. Now, let V{v0+0<i<mλivi:0λi<1}. Vnis finite. Moreover, if v0+0<i<mκivin then also v0+0<i<mκivin if κiκi. Hence,

M = w V w + v 1 + + v m (2.6)

There is a semilinear set.

Lemma 2.5. Let Mn be a semilinear subset of n. Then Mn is semilinear.

Proof It suffices to show this for linear subsets. Let vi, i<n+1, be vectors such that

M = v 0 + v 1 + + v m 1 (2.7)

Put wivi, 0<i<m. Then

M = v 0 + v 1 + v 2 + + v m 1 + w 1 + + w m 1 (2.8)

Thus, we may without loss of generality assume that

M = v 0 + v 1 + v 2 + + v m 1 (2.9)

Notice, however, that these vectors are not necessarily in n. For i starting at 1 until n we do the following.

Let xjivi(i). Assume that for 0<j<p, xji0, and that for pj<m, xji>0. (A renaming of the variables can achieve this.) We introduce new cyclic vectors cj,k for 0<j<p and pk<m. Let μ the least common multiple of the |xsi|, for all 0<s<m where xsi0:

c i , j ( μ / x j i ) v j + ( μ / x k i ) v k (2.10)

Notice that the s-coordinates of these vectors are positive for s<i, since this is a positive sum of positive numbers. The ith coordinate of these vectors is 0. Suppose that the ith coordinate of

w = v 0 + 0 < j < m λ j v j (2.11)

is 0, where γj for all 0<j<m. Suppose further that for some kp we have λkv0i+(μ/|xki|). Then there must be a j<p such that λj(μ/xji). Then put λrλr for rj,k,λjλj(μ/xji) and λkλk+(μ/xki). Then

w = c j , k + 0 < j < m λ j v j (2.12)

Moreover, λjλj for all j<p, and λk<λk. Thus, by adding these cyclic vectors we can see to it that the coefficients of vk for pk<m are bounded. Now define P to be the set of

w = v 0 + 0 < j < m λ j v j n (2.13)

where λj<v0j+m|μ/xji| for all 0<j<m. Then

M n = u P u + 0 < j < p λ j v j + 0 < j < p k < m κ j , k c j , k (2.14)

with all λj, κj,k0. Now we have achieved that all jth coordinates of vectors are positive.

The following is now immediate.

Lemma 2.6. Let Mn be an affine subspace. Then Mn is a semilinear subset of n.

Lemma 2.7. The intersection of two semilinear sets is again semilinear.

Proof It is enough to show the claim for linear sets. So, let C0={ui:i<m}, C1={vi:i<n} and S0Σ({v0}:C0) and S1Σ({v1};C1) be linear. We will show that S0S1 is semilinear. To see this, notice that wS0S1 iff there are natural numbers κi(i<m) and λj(j<n) such that

w = c + i < m κ i u i = e + i < n λ i v i (2.15)

So, we have to show that the set of these w is semilinear.

The equations are now taken as linear equations with κi, i<m and λj, i<n, as variables. Thus we have equations for m+n variables. We solve these equations first in m+1. They form an affine subspace of m+nmn. By the Lemma 2.6, the intersection of the set with m+n is semilinear, and so is its projection onto m (or to n for that matter). Let it be i<pLi, where for each i<p, Lim is linear. Thus there is a representation of Li as

L i = θ + η 0 + + η γ 1 (2.16)

Now put

W i { v 0 + i < m κ ( i ) u i : κ L i } (2.17)

From the construction we get that

S 0 S 1 = i < p W i (2.18)

Define vector qiΣi<mη(j), ui, i<γ and rc+Σj<mθ(j)ui. Then

W i = r + q 0 + + q γ 1 (2.19)

So, Wi is linear. This shows the claim.

Lemma 2.8. If Sn is semilienar, so is its projection πn[S].

2.1  The Theorem

We need one more prerequisite. Say that a first-order theory T has quantifier elimination if for every formula ϕ(x) there exists a quantifier free formula χ(x) such that Tϕ(x)χ(x). We follow the proof of [3].

Theorem 2.9. (Presburger) Presburger Arithmetic has quantifier elimination.

Proof It is enough to show that for every formula (x)ϕ(y,x) with ϕ(y,x) quantifier free there exists a quantifier free formula χ(y) such that

( y ) ( ( x ) ϕ ( y , x ) χ ( y ) ) (2.20)

Now, we may further eliminate negation (see the remarks above) and disjunctions inside ϕ(y,x) (since (x)(αβ)(x)α(x)β ). Finally, we may assume that all conjuncts contain x. For if α does not contain x fee, (x)(αβ) is equivalent to α(x)β. So, ϕ can be assumed to be a conjunction of atomic formulae of the following form:

( x ) ( i < p n i x t i i < q n i x < t i i < r n i x > t i i < s n i x m i t i ) (2.21)

Now, st is equivalent with nsnt, so after suitable multiplication we may see to it that all the ni, ni, ni are the same number ν.

( x ) ( i < p ν x τ i i < q ν x < τ i i < r ν x > τ i i < s ν x m i τ i ) (2.22)

We may rewrite the formula in the following way (replacing νx b< x and the condition that x is divisible by ν).

( x ) ( x ν 0 i < p x τ i i < q x < τ i i < r x > τ i i < s x m i τ i ) (2.23)

Assume that p>0. Then the first set of conjunctions is equivalent with the conjunction of i<j<pτiτj (which does not contain x) and xτ0. We may therefore eliminate all occurances of x by τ0 in the formula (2.23).

Thus, from now on we may assume that p=0. Also, notice that x<σx<τ is equivalent to (x<σστ)(x<ττ<σ). This means that we can assume q1, and likewise that r1. Next we show that we can actually have s1. To see this, notice the following.

Let u, v, w, x be integeres, w, x>1, and let p be the least common multiple of w and x. Then qed (p/w,p/x)=1, and so there exist integers m, n such that 1=m·p/w+n·p/x. It follows that the following are equivalent.

y u (modw) and yv (modx)

u v (modged(w,x)) and ym(p/w)u+n(p/x)v(modp).

Proof Using this equivalence we can reduce the congruence statements to a conjunction of congruences where only involves x.

This leaves us with 8 possibilities. If r=0 or s=0 the formula is actually trivially true. That is to say, (x)(x<τ), (x)(v<x), (x)(xmξ), (x)(x<τxmξ) and (x)(v<xxmξ) are equivalent to . Finally, it is verified that

( x ) ( x < τ v < x ) v + 1 < τ (2.24)
( x ) ( x < τ v < x x m ξ ) i < m ( τ + 1 + i < v τ + 1 + i m ξ ) (2.25)

Theorem 2.10. (Ginsburg & Spanier) A subset of n is semilinear iff it is definable in Presburger Arithmetic.

Proof  () Every semilinear set is definable in Presburger Arithmetic. To see this it is enough to show that linear sets are definable. For if M is a union of Ni, i<p, and each Ni is linear and hence definable by a formula ϕi(x), then M is definable by i<pϕi(x). Now let M=v+v0++vm1 be linear. Then put

ϕ ( x ) ( y 0 ) ( y 1 ) ( y m 1 ) ( i < m 0 y i i < n ( v ( i ) + j < m y i v ( i ) j x i ) ) (2.26)

ϕ ( x ) defines M. () Let ϕ(x) be a formula defining S. By Theorem 2.9, there exists a quantifier free formula χ(x) defining S. Moreover, as we have remarked above, χ can be assumed to be negation free. Thus, χ is a disjunction of conjunctions of atomic formulae. By Lemma 2.7, the set of semilinear subsets of n is closed under intersection of members, and it is also closed under union. Thus, all we need to show is that atomic formulae define semilinear sets. Now, observe that x0mx1 is equivalent to (x2)(x0x1+mx2), which is semilinear, as it is the projection of x0x1+mx2 onto the first two components.

Corollary 2.11. The complement of a semilinear set is again semilinear.

References

 [1] Seymour Ginsburg and Edwin H. Spanier.
Bounded ALGOL–Like Languages.
Transactions of the American Mathematical Society, 113:333 – 368, 1964.

 [2] Seymour Ginsburg and Edwin H. Spanier.
Semigroups, Presburger Formulas, and Languages.
Pacific Journal of Mathematics, 16:285 – 296, 1966.

 [3] J. Donald Monk. Mathematical Logic. Springer, Berlin, Heidelberg, 1976.