An expansion of Presburger's arithmetics by a unary function
such that the first-order theory of the expansion
is decidable, the expansion has an independent formula and
(M,I)-Isolation Property does not hold
3.
A.Blumensath and E.Graedel.
Automatic structures.
In Proc. 15th IEEE Symp. on Logic
in Computer Science ,
pages 51−62.
IEEE Computer Society Press, 2000.
4.
M.Benedikt, L.Libkin, T.Schwentick,
and L.Segoufin.
A model-theoretic approach to regular
string relations.
In Proc. 16th IEEE Symp. on Logic
in Computer Science,
pages 431−442.
IEEE Computer Society Press, 2001.
It was proved in [3] that the first-order theory
of
< N, <, +, |p>
where
p>1 is a natural number and
x|p y ⇔
(∃u)(∃k)
(x=pu & y=kx)
is decidable. It is trivial and was observed in [4]
that
< N, <, +, |p>
has an independent
formula. I prove that in many cases,
(M,I)-Isolation Property does
not hold for the first-order theory of
< N, <, +, |p>.
Previous page
Next page