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 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.
Let be the set of –tuples of natural numbers. A tuple is denoted by an arrow, eg , whose coordinates are , . Put . Define by
(1.1) |
Denote the structure also by . The unit vector which is except at place number . where it is , is denoted by . We define inductively as follows. , . We write for the set and . A nonempty subset of is called linear if it can be written as
(1.2) |
for some (which may be zero, in which case we get the singleton ). Likewise, a subset of is called linear if it has the form
(1.3) |
for subsets of as well as
(1.4) |
for subsets of . The linear subset of are nothing but the affine subspaces.
A subset of is called semilinear if it is the finite union of semilinear sets. We employ the following notation.
Definition 1.1. Let and be finite subsets of . Then denotes the set of vectors of the form such that , and for all .
Presburger Arithmetic is defined as follows. The basic symbols are , , , and , . Then Presburger Arithmetic is the first order theory of the structure , where is divisible by .
Negation can be eliminated.
(1.5) |
where is defined by , . We shall occasionally use for . Moreover, multiplication by a given natural number also is definable: put , and . Every term in the variables , , is equivalent to , where , . A subset of is definable if there is a formula such that
(1.6) |
The definable subsets of are closed under union, intersection and complement and permutation of the coordinated. Moreover, if is definable, so is its projection
(1.7) |
The same holds for definable subsets of , which are simply those definable subsets of that are included in . Clearly, if is definable, so .
Lemma 2.1. Suppose that is a linear equation with rational numbers , , and . Then there is an equivalent equation with positive integer coefficients such that and for every .
Proof First, multiply with the least common denominator to transform the equation into an equation with integer coefficients. Next, for every , substract from both sides and otherwise.
□
Call an equation reduced if it has the form
(2.1) |
with positive integer coefficients and , . 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 . Consider a vector of the form , where and . Then if is a solution, so is and conversely. Put and let
(2.2) |
Both and are finite. Moreover, the set of solutions is exactly .
□
Lemma 2.3. The set of solutions of a reduced inequation is semilinear.
Proof Assume that the inequation has the form
(2.3) |
Define and as before. Let . Then the set of solutions is . If the inequation has the form
(2.4) |
the set of solutions is where .
□
Lemma 2.4. Let be an affine subspace. Then is a semilinear subset of .
Proof Let , , be vectors such that
(2.5) |
We can assume that the are lineary independent. Clearly, since for any nonzero rational number , we can assume that , . Now, let . is finite. Moreover, if then also if . Hence,
(2.6) |
There is a semilinear set.
□
Lemma 2.5. Let be a semilinear subset of . Then is semilinear.
Proof It suffices to show this for linear subsets. Let , , be vectors such that
(2.7) |
Put , . Then
(2.8) |
Thus, we may without loss of generality assume that
(2.9) |
Notice, however, that these vectors are not necessarily in . For starting at until we do the following.
Let . Assume that for , , and that for , . (A renaming of the variables can achieve this.) We introduce new cyclic vectors for and . Let the least common multiple of the , for all where :
(2.10) |
Notice that the -coordinates of these vectors are positive for , since this is a positive sum of positive numbers. The th coordinate of these vectors is . Suppose that the th coordinate of
(2.11) |
is , where for all . Suppose further that for some we have . Then there must be a such that . Then put for and . Then
(2.12) |
Moreover, for all , and . Thus, by adding these cyclic vectors we can see to it that the coefficients of for are bounded. Now define to be the set of
(2.13) |
where for all . Then
(2.14) |
with all , . Now we have achieved that all th coordinates of vectors are positive.
□
The following is now immediate.
Lemma 2.6. Let be an affine subspace. Then is a semilinear subset of .
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 , and and be linear. We will show that is semilinear. To see this, notice that there are natural numbers and such that
(2.15) |
So, we have to show that the set of these is semilinear.
The equations are now taken as linear equations with , and , , as variables. Thus we have equations for variables. We solve these equations first in . They form an affine subspace of . By the Lemma 2.6, the intersection of the set with is semilinear, and so is its projection onto (or to for that matter). Let it be , where for each , is linear. Thus there is a representation of as
(2.16) |
Now put
(2.17) |
From the construction we get that
(2.18) |
Define vector , , and . Then
(2.19) |
So, is linear. This shows the claim.
□
Lemma 2.8. If is semilienar, so is its projection .
We need one more prerequisite. Say that a first-order theory has quantifier elimination if for every formula there exists a quantifier free formula such that . 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 with quantifier free there exists a quantifier free formula such that
(2.20) |
Now, we may further eliminate negation (see the remarks above) and disjunctions inside (since ). Finally, we may assume that all conjuncts contain . For if does not contain fee, is equivalent to . So, can be assumed to be a conjunction of atomic formulae of the following form:
(2.21) |
Now, is equivalent with , so after suitable multiplication we may see to it that all the , , are the same number .
(2.22) |
We may rewrite the formula in the following way (replacing b< and the condition that is divisible by ).
(2.23) |
Assume that . Then the first set of conjunctions is equivalent with the conjunction of (which does not contain ) and . We may therefore eliminate all occurances of by in the formula (2.23).
Thus, from now on we may assume that . Also, notice that is equivalent to . This means that we can assume , and likewise that . Next we show that we can actually have . To see this, notice the following.
Let , , , be integeres, , , and let be the least common multiple of and . Then qed , and so there exist integers , such that . It follows that the following are equivalent.
and
and .
□
Proof Using this equivalence we can reduce the congruence statements to a conjunction of congruences where only involves
This leaves us with 8 possibilities. If or the formula is actually trivially true. That is to say, , , , and are equivalent to . Finally, it is verified that
(2.24) |
(2.25) |
□
Theorem 2.10. (Ginsburg & Spanier) A subset of 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 is a union of , , and each is linear and hence definable by a formula , then is definable by . Now let be linear. Then put
(2.26) |
defines . Let be a formula defining . By Theorem 2.9, there exists a quantifier free formula defining . 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 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 is equivalent to , which is semilinear, as it is the projection of onto the first two components.
□
Corollary 2.11. The complement of a semilinear set is again semilinear.
[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.