## On Spatial Conjunction as Second-Order Logic

paper ps
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.

### Citation

Viktor Kuncak and Martin Rinard. On spatial conjunction as second-order logic. Technical Report 970, MIT CSAIL, October 2004.

### BibTex Entry

```@techreport{KuncakRinard04SpatialConjunctionSecondOrderLogic,
author = {Viktor Kuncak and Martin Rinard},
title = {On Spatial Conjunction as Second-Order Logic},
institution = {MIT CSAIL},
year = 2004,
number = {970},
month = {October},
url = {http://arxiv.org/abs/cs.LO/0410073},
abstract = {
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.
}
}
```