| Spatial conjunction is a powerful construct for reasoning about dynamically allocated
data structures, as well as concurrent, distributed and mobile computation. While
researchers have identified many uses of spatial conjunction, its precise expressive power
compared to traditional logical constructs was not previously known.
In this paper we establish the expressive power of spatial conjunction. We construct an
embedding from first-order logic with spatial conjunction into second-order logic, and more
surprisingly, an embedding from full second order logic into first-order logic with spatial
conjunction. These embeddings show that the satisfiability of formulas in first-order logic
with spatial conjunction is equivalent to the satisfiability of formulas in second-order logic.
These results explain the great expressive power of spatial conjunction and can be used
to show that adding unrestricted spatial conjunction to a decidable logic leads to an undecidable
logic. As one example, we show that adding unrestricted spatial conjunction to
two-variable logic leads to undecidability.
On the side of decidability, the embedding into second-order logic immediately implies the
decidability of first-order logic with a form of spatial conjunction over trees. The embedding
into spatial conjunction also has useful consequences: because a restricted form of spatial
conjunction in two-variable logic preserves decidability, we obtain that a correspondingly
restricted form of second-order quantification in two-variable logic is decidable. The resulting
language generalizes the first-order theory of boolean algebra over sets and is useful in
reasoning about the contents of data structures in object-oriented languages. |