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.

Symbol	Unicode	Name	Meaning
X	—	Team	Set of assignments
⊆	U+2286	Inclusion atom	x̄ ⊆ ȳ: values of x̄ among values of ȳ
s	—	Assignment	A member of the team
⊨	U+22A8	Satisfaction	Between a team and a formula
GFP⁺	—	Greatest fixed point	The captured logic

Metatheory. Union closure without downward closure is what separates inclusion logic from the rest of the family, and the PTIME characterization is the payoff: a team-semantic logic that is not Σ¹₁. The result requires an order on the finite structures, as descriptive-complexity capture results generally do. The inclusion atom is exactly the inclusion dependency of relational databases, which is 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. No compositional contradictory negation, which costs 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. 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.