A natural interest of computational logic is to investigate decidable subsets of first-order logic. One such subset is the formalism of inclusion logic (FOI), introduced by Galliani as an evolution of dependence logic [1], which investigates functional dependencies that arise in database theory. FOI allows as an atomic predicate only tuple inclusion (a generalization of the subset predicate to multiple components); the semantics of FOI are defined not only over single assignments of variables to values, but also over sets of assignments called “teams.”

This paper investigates the properties of inclusion logic under lax team semantics, where a disjunction is also satisfied if overlapping subsets of teams satisfy each of its parts. In particular, it shows: (1) the full expressiveness of FOI is already achieved if formulas are restricted to a single universal quantifier; (2) already in finite models, a logic FOI_k that restricts inclusion to tuples of length k is strictly less expressive than a logic FOI_(k+1) (which gives rise to an infinite expressiveness hierarchy); and (3) in finite ordered models, the expressiveness of FOI is already achieved if formulas are restricted to five inclusion atoms. The proofs of these results, in particular for the main result (2), represent the core of the paper.

This paper nicely complements and extends Galliani’s results; for more background on FOI and its motivation, readers should study the corresponding references first. It also raises open questions for future research, such as generalizing property to ordered models or to unordered ones.