Abstract
Fractional share models are used to reason about how multiple actors share ownership of resources. We study the decidability and complexity of reasoning over the tree share model of Dockins et al. using first-order logic and its fragments. We identify a connection between the basic Boolean operations on trees — union (t), intersection (u), and complement — and countable atomless Boolean algebras. This connection allows us to establish decidability results with precise complexity bounds for both the full first-order theory and its existential fragment over the tree share model with these operations. We further relate the multiplication operation (bowtie) on trees to the theory of word equations, deriving decidability for its existential theory and undecidability for its full first-order theory. Finally, we show that the full first-order theory over the model combining Boolean operations with restricted multiplication (./ with constants on the right-hand side) remains decidable via an embedding into tree-automatic structures.