Algebraic Relativization and Arrow Logic
Maarten Marx
Abstract:
We investigate several weakened versions of first--order logic, and of
the logic of binary relations, as provided by representable relation
algebras. The most important reason to weaken these two well-known and
often-used logics is their complexity: the theory of both systems is
undecidable. These logics are not only used in areas where this
complexity is needed, as in mathematics, but also in other disciplines
(computer science, linguistics) which deal with simpler (i.e.,
decidable) questions. For this reason it is desirable to develop new
versions of these logics, which are close to the original with respect
to expressive power and semantics, but behave better computationally.
We change first--order logic such that, given a model $M=$ the set
of assignments for $M$ is just a subset of ${^\omega D}$. We show
decidability of such a weakened first--order logic, using filtration. We
also investigate Craig interpolation and Beth definability of these logics.
J.~van Benthem baptized the weakened version of the logic of binary
relations ``arrow--logic''. This is a modal logic, interpreted on a
set of arrows, with modalities for composition and inverse of arrows,
and a (constant) modality denoting that the source and target of an
arrow are the same. In this work, we identify arrows with the pair
$<${\em source, target}$>$. We investigate the
complete spectrum of arrow--logics in which the domain of the models
is a binary relation, satisfying a combination of the conditions
$\{$ reflexivity, symmetry, transitivity, Cartesian product $\}$.
We systematically treat decidability, finite axiomatizability, Craig
interpolation and Beth definability. Our results can be summarized in
one sentence: an arrow--logic has one or more of these positive
properties if and only if the domains of the models are not
necessarily transitive relations.