Next: Reducing Domino Problems to
Up: Consistency of  is
Previous: Domino Systems
Similar to proving undecidability by reduction of unbounded domino problems,
where defining infinite grids is the key problem, defining a torus of
exponential size is the key to obtaining a
completeness proof by
reduction of bounded domino problems.
To be able to apply Corollary 3.3 to
consistency for
,
we must characterise the torus
with a
of polynomial size. To characterise
this torus, we use 2n concepts
and
,
where X_{i} (resp., Y_{i}) codes the ith bit of the binary representation of
the Xcoordinate (resp., Ycoordinate) of an element a.
For an interpretation
and an element
,
we define
by
We use a wellknown characterisation of binary addition
(e.g. [BGG97]) to relate the positions of the elements in the
torus:
Lemma 3.4
Let x,
x'
be natural numbers with binary representations
Then
where the empty conjunction and disjunction are interpreted as true
and false, respectively.
Figure 3:
A TCBOX defining a torus of exponential size

The
T_{n} is defined in Figure 3. The concept
C_{(0,0)} is satisfied by all elements a of the domain for which
holds.
C_{(2n1,2n1)} is a similar concept, whose instances asatisfy
.
The concept
is similar to
where the role
has
been substituted for
and variables X_{i} and Y_{i} have been swapped.
The concept
(resp.
)
enforces that, along the role
(resp.
), the value of
(resp.
)
increases by one while
the value of
(resp.
)
is unchanged. They are analogous to the
formula in Lemma 3.4.
The following lemma is a consequence of the definition of
and
Lemma 3.4.
Lemma 3.5
Let
be an interpretation,
defined as in Figure 3, and
.
The
T_{n} defines a torus of exponential size in the following
sense:
Lemma 3.6
Let T_{n} be the
as defined in Figure 3. Let
be a model of T_{n}. Then
where
U(2
^{n},2
^{n})
is the torus
and S_{1},
S_{2} are
the horizontal and vertical successor relations on this torus.
Proof.
We show that the function pos is an isomorphism from
to
U(2^{n},2^{n}). Injectivity of
is shown by induction on the
``Manhattan distance'' d(a) of the
value of an element a to the
value of the upper right corner.
For an element
we define d(a) by
Note that
implies
d(a) = d(b). Since
,
there is at most one element
such that d(a)=0. Hence, there is exactly one element a such
that
.
Now assume there are elements
such that
and
d(a) = d(b) > 0. Then either
or
.
W.l.o.g., we assume
.
From
,
it follows that
.
Let a_{1},b_{1} be elements such that
and
.
Since
d(a_{1}) = d(b_{1}) < d(a) and
,
the induction
hypothesis yields a_{1} = b_{1}. From
Lemma 3.5 it follows that
This also implies a=b because
and
.
Hence
is injective.
To prove that
is also surjective we use a similar technique.
This time, we use an induction on the distance from the lower left corner.
For each element
,
we define:
d'(x,y) = x+y .
We show by induction that, for each
,
there is an
element
such that
.
If
d'(x,y) = 0, then
x=y=0. Since
,
there is an element
such that
.
Now consider
with
d'(x,y) >0. Without loss of generality we assume x > 0 (if x = 0 then y > 0 must hold). Hence
and
d'(x1,y) <
d'(x,y). From the induction hypothesis, it follows that there is an element
such that
.
Then there must be an
element a_{1} such that
and
Lemma 3.5 implies that
.
Hence
is also surjective.
Finally,
is indeed a homomorphism as an immediate consequence of
Lemma 3.5.
It is interesting to note that we need inverse roles only to guarantee that
pos is injective. The same can be achieved by adding the cardinality
restriction
to T_{n}, from which the
injectivity of pos follows from its surjectivity and simple cardinality
considerations. Of course the size of this cardinality restriction would
only be polynomial in n if we assume binary coding of numbers. Also note
that we have made explicit use of the special expressive power of
cardinality restrictions by stating that, in any model of T_{n}, the
extension of
C_{(2n1,2n1)} must have at most one element. This
cannot be expressed with a
TBox consisting of terminological axioms.
Next: Reducing Domino Problems to
Up: Consistency of  is
Previous: Domino Systems
Stephan Tobies
May 02 2000