Inclusion Logic

Origin. Pietro Galliani, "Inclusion and exclusion dependencies in team semantics" (Annals of Pure and Applied Logic, 2012). First-order logic extended with the inclusion atom, borrowed from the inclusion dependencies of database theory. Its expressive power was settled by Galliani and Hella (2013).

Models. A team gives each variable a set of values. The inclusion atom says one such set is contained in another: whatever x̄ takes, ȳ takes somewhere in the same team. The atom is a statement about the team as a whole and says nothing about any single assignment in it — which is why the logic is not a fragment of first-order logic despite having no second-order syntax.

Formalism.

Teams: X ⊆ {s : s an assignment on dom} Satisfaction is M, X ⊨ φ, never M, s ⊨ φ.

The inclusion atom: M, X ⊨ x̄ ⊆ ȳ iff ∀s ∈ X ∃s′ ∈ X : s(x̄) = s′(ȳ) Every value x̄ takes somewhere, ȳ takes somewhere.

Closure properties — the distinguishing facts: Union closure: if X_i ⊨ φ for every i, then ⋃_i X_i ⊨ φ. NOT downward closed: X ⊨ φ and Y ⊆ X does not give Y ⊨ φ. Dependence logic is the mirror image: downward closed, not union closed.

Empty team: ∅ ⊨ φ for every φ (the empty team property, shared across the family).

Expressive power (Galliani–Hella 2013): Sentences of inclusion logic capture GFP⁺ — positive greatest-fixed-point logic. Over ordered finite structures, that is PTIME. Compare dependence logic: Σ¹₁, hence NP. The family does not have one expressive power; the closure property decides it.

No compositional negation: Contradictory negation is not definable; the logic is closed under a dual negation only on the flat fragment.

Symbols.

Metatheory. Galliani and Hella (2013) proved that sentences of inclusion logic capture exactly positive greatest-fixed-point logic, hence, by the Immerman–Vardi theorem, PTIME over finite ordered structures; the data complexity of model checking is polynomial, against NP-completeness for dependence logic. Union closure without downward closure is what makes this possible, and it is the payoff of the whole construction: a team-semantic logic that is not Σ¹₁. The result requires an order on the finite structures, as descriptive-complexity capture results generally do, and it requires the lax reading of the existential quantifier — under strict semantics the union-closure argument fails. The empty team property and locality both hold (Galliani, 2012). Combined with the exclusion atom, inclusion logic reaches independence logic, so it is not weak but differently placed. The atom is exactly the inclusion dependency of relational databases, where Casanova, Fagin and Papadimitriou (1984) showed the implication problem for inclusion dependencies alone to be PSPACE-complete, and where the axiom system for it came from.

Applies to. Database dependency theory. Descriptive complexity below NP. The comparative study of team-semantic atoms. Any setting where a constraint holds of a set of records rather than of each record.

Limitations. Union closure is a ceiling as well as a tool: the dependence atom is not union closed and so is not definable in inclusion logic, and no NP-complete property is expressible over finite structures unless PTIME = NP. The empty team satisfies every formula, so nonemptiness of a team cannot be stated. There is no compositional contradictory negation, which loses the usual proof-theoretic machinery. The PTIME capture is over ordered structures only; without order the question is the standard open one for the whole capture programme, and it depends on the lax semantics — the strict reading gives a different and not union-closed logic. The atom's database provenance can mislead: inclusion dependencies there are a static constraint, while here the team is the semantic object and changes under the connectives.

© 2026 Lingenic LLC