Exclusion Logic

Origin. Pietro Galliani, "Inclusion and exclusion dependencies in team semantics" (Annals of Pure and Applied Logic, 2012), which introduced the exclusion atom alongside the inclusion atom and settled its expressive power in the same paper.

Models. The dual constraint to inclusion: the values a team gives x̄ and the values it gives ȳ are disjoint. Like inclusion, it is a property of the team and not of any assignment in it. Unlike inclusion, it is downward closed — and that single property makes it expressively equivalent to dependence logic.

Formalism.

The exclusion atom: M, X ⊨ x̄ | ȳ iff ∀s, s′ ∈ X : s(x̄) ≠ s′(ȳ) No value of x̄ is a value of ȳ anywhere in the team.

Closure: Downward closed: X ⊨ φ and Y ⊆ X gives Y ⊨ φ. Same closure as dependence logic; opposite to inclusion logic.

Expressive power (Galliani 2012): Exclusion logic ≡ dependence logic, sentence for sentence. Both capture Σ¹₁, hence NP over finite structures. Each atom is definable from the other in the presence of first-order machinery.

Inclusion + exclusion: Together they give independence logic's strength. Inclusion–exclusion logic ≡ independence logic (Galliani 2012).

Contrast with inclusion: Two atoms, one paper, opposite closure properties, different logics. Downward closure tracks Σ¹₁; union closure tracks GFP⁺.

Symbols.

Symbol	Unicode	Name	Meaning
X	—	Team	Set of assignments
\|	—	Vertical line / Exclusion atom	x̄ \| ȳ: value sets disjoint
⊆	U+2286	Subset / Inclusion atom	The dual constraint; also subteam
Σ¹₁	—	Sigma-1-1	Existential second-order; the captured class
⊨	U+22A8	True / Satisfaction	Between a model-team pair and a formula
∀	U+2200	Universal quantifier	Ranges over members of the team
∈	U+2208	Element of	Assignment belonging to a team
≠	U+2260	Not equal to	Disjointness of value tuples
s	—	Assignment	A member of the team
GFP⁺	—	Positive greatest fixed point	Inclusion logic's class, for contrast

Metatheory. Galliani (2012) proved exclusion logic equivalent to dependence logic by giving translations both ways: the exclusion atom is definable in dependence logic and the dependence atom in exclusion logic. The equivalence places exclusion logic exactly where Kontinen and Väänänen (2009) placed dependence logic — a formula defines a class of teams iff that class is Σ¹₁-definable, downward closed, and contains the empty team — and hence at Σ¹₁ on sentences, which by Fagin's theorem is NP over finite structures. Downward closure, the empty team property and locality all hold. Validity is inherited from dependence logic and so is non-arithmetical, with no recursive axiomatization. The equivalence is the reason the atom matters: it shows that Σ¹₁ is reached by more than one route, and that the family's expressive classification is organized by closure properties rather than by the intuitive content of the atoms. Combined with inclusion, it reaches independence logic — so two atoms with simple database readings suffice for the whole hierarchy.

Applies to. Database dependency theory (exclusion dependencies). Comparative expressive power in team semantics. Reductions among team-semantic logics.

Limitations. Downward closure caps what the logic can say as much as it enables: no team property that is not downward closed is definable, so the inclusion atom is not expressible here, and since the empty team satisfies every formula, nonemptiness of a team cannot be stated. The Σ¹₁ ceiling excludes any co-NP-complete property over finite structures unless NP = co-NP, and well-foundedness, which is Π¹₁, outright. Validity has no recursive axiomatization. There is no compositional contradictory negation. Expressively the atom adds nothing to dependence logic — the negative result is what made it a footnote — and the disjointness reading is natural for databases and strained as an account of anything linguistic, which is where the dependence atom's motivation came from.