Definability and expressive completeness for team-semantic logics

A team property over a point type α is a class of teams, Set (Finset α). A formula defines the team property consisting of all teams that support it, and a logic defines the class ⟦L⟧ of the properties its formulas define ([Ant25]). The organizing theorem for the team-semantic family is expressive completeness: ⟦L⟧ equals a class fixed by closure conditions (downward closure IsLowerSet, union closure SupClosed, convexity Set.OrdConnected, the empty-team property ∅ ∈ P, flatness Team.IsFlat), plus invariance under bounded bisimulation in the modal case.

The definable class is stated over an abstract support relation s : Form → Finset α → Prop, so every logic instantiates it with its own support M, and a fragment of a language is the subtype of its formulas. Soundness is definableClass s ⊆ C and completeness definableClass s = C; each logic proves the soundness half from its closure theorems through definableClass_subset, and the converse half, through normal forms, is per-logic work.

Main definitions

• Team.definableClass s: the properties definable under s, written ⟦L⟧ in [Ant25].

Main results

• Team.definableClass_subset: closure of every formula's support set is soundness.

References

• [Ant25] Anttila, Not Nothing: Nonemptiness in Team Semantics

def Team.definableClass {α : Type u_1} {Form : Type u_2} (s : Form → Finset α → Prop) : Set (TeamProperty α)

The class ⟦L⟧ of team properties definable under the support relation s: the support sets of the formulas.

Equations

• Team.definableClass s = Set.range fun (φ : Form) => {t : Finset α | s φ t}

@[simp]

theorem Team.mem_definableClass {α : Type u_1} {Form : Type u_2} {s : Form → Finset α → Prop} {P : TeamProperty α} : P ∈ definableClass s ↔ ∃ (φ : Form), {t : Finset α | s φ t} = P

theorem Team.definableClass_subset {α : Type u_1} {Form : Type u_2} {s : Form → Finset α → Prop} {C : TeamProperty α → Prop} (h : ∀ (φ : Form), C {t : Finset α | s φ t}) : definableClass s ⊆ {P : TeamProperty α | C P}

Soundness from closure. If every formula's support set has the closure property C, every definable property does.