# 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.

© 2026 Lingenic LLC