Definability and expressive completeness for team-semantic logics

[Ant25]

A team property over a point type α is a class of teams, Set (Finset α) — the same object Team/Closure.lean calls a "team-set". A formula φ defines the team property consisting of all teams that support it. The organizing theorem for the team-semantic family ([Ant25]) is expressive completeness: the class of properties a logic can define equals a class fixed by closure conditions (downward closure, union closure, convexity, the empty-team property) — plus invariance under bounded bisimulation in the modal case.

This file is the substrate for that program. It defines definability and the definable class over an abstract support relation s : Form → Finset α → Prop, so every logic — bilateral or unilateral, modal or propositional — instantiates it with its own support M. It does not import any logic: each logic's expressive-completeness theorem lives with the logic and consumes definableClass_subset here.

The reusable bridge is definableClass_subset: a per-logic closure theorem (supClosed_support, isLowerSet_support, …, proved in each logic's file) becomes the soundness half of expressive completeness (definable class ⊆ closure class) by one application. The hard converse half — every property in the class is definable, via normal forms — is the per-logic work the roadmap tracks.

Main definitions

• TeamProperty α — a class of teams, Set (Finset α).
• definedBy s φ — the team property defined by φ under support s.
• Definable s P, definableClass s — the definable properties (written ⟦L⟧ in [Ant25] for a logic L with support relation s).
• ExpressivelyCompleteFor s C, SoundFor s C — the completeness and soundness relations against a class C of team properties.
• definableClassWhere s Q — the fragment-relative definable class (properties defined by a formula satisfying Q); definableClass is the Q := fun _ => True case. Logics with no unconditional cell (e.g. QBSML, whose closure properties hold only NE-free) state soundness against this.
• downwardClosedProperties, unionClosedProperties, convexProperties, emptyTeamProperties, flatProperties — the closure "cells" the completeness theorems characterise logics against.

Main results

• definableClass_subset — the reusable soundness bridge.

Roadmap

This file is phase 1 of the team-semantics family roadmap; see Core/Logic/Modal/README.md. The closure predicates it packages come from Team/Closure.lean (themselves mathlib Order/ predicates).

Team properties and definability

@[reducible, inline]

abbrev Core.Logic.Team.TeamProperty (α : Type u_3) : Type u_3

A team property over points α is a class of teams. A formula defines the property consisting of all teams in which it is true. Identical to the "team-set" T : Set (Finset α) of Team/Closure.lean; the alias marks the role in the expressive-completeness program.

Equations

• Core.Logic.Team.TeamProperty α = Set (Finset α)

def Core.Logic.Team.definedBy {α : Type u_1} {Form : Type u_2} (s : Form → Finset α → Prop) (φ : Form) : TeamProperty α

The team property defined by φ under support relation s: the class of all teams supporting φ.

Equations

• Core.Logic.Team.definedBy s φ = {t : Finset α | s φ t}

def Core.Logic.Team.Definable {α : Type u_1} {Form : Type u_2} (s : Form → Finset α → Prop) (P : TeamProperty α) : Prop

P is definable under s if some formula defines it.

Equations

• Core.Logic.Team.Definable s P = ∃ (φ : Form), P = Core.Logic.Team.definedBy s φ

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

The class of team properties definable under s — written ⟦L⟧ in [Ant25] for a logic L with support relation s. Expressive completeness is the statement definableClass s = C.

Equations

• Core.Logic.Team.definableClass s = {P : Core.Logic.Team.TeamProperty α | Core.Logic.Team.Definable s P}

@[simp]

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

def Core.Logic.Team.ExpressivelyCompleteFor {α : Type u_1} {Form : Type u_2} (s : Form → Finset α → Prop) (C : Set (TeamProperty α)) : Prop

A logic, given by its support relation s, is expressively complete for a class C of team properties iff the definable properties are exactly C.

Equations

• Core.Logic.Team.ExpressivelyCompleteFor s C = (Core.Logic.Team.definableClass s = C)

def Core.Logic.Team.SoundFor {α : Type u_1} {Form : Type u_2} (s : Form → Finset α → Prop) (C : Set (TeamProperty α)) : Prop

s is sound for C: every definable property lies in C. The easy half of expressive completeness, supplied by the per-logic closure theorems via definableClass_subset.

Equations

• Core.Logic.Team.SoundFor s C = (Core.Logic.Team.definableClass s ⊆ C)

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

The soundness bridge. If every formula's support set has closure property C, then every definable property does. Apply with a per-logic closure theorem — e.g. definableClass_subset (fun φ => supClosed_support M φ) yields the soundness half of BSML's expressive completeness.

theorem Core.Logic.Team.ExpressivelyCompleteFor.soundFor {α : Type u_1} {Form : Type u_2} {s : Form → Finset α → Prop} {C : Set (TeamProperty α)} (h : ExpressivelyCompleteFor s C) : SoundFor s C

Expressive completeness implies soundness.

Fragment-relative definability

Some logics have no unconditional closure cell — only a fragment of the language does. The leading case is QBSML ([AvO23]), whose support is flat only for NE-free formulas (Proposition 4.1 / Fact 2). For such logics the soundness statement is definableClassWhere s Q ⊆ C, where Q carves out the fragment.

def Core.Logic.Team.definableClassWhere {α : Type u_1} {Form : Type u_2} (s : Form → Finset α → Prop) (Q : Form → Prop) : Set (TeamProperty α)

The team properties definable under s by a formula satisfying Q. definableClass s = definableClassWhere s (fun _ => True); the fragment predicate Q restricts to a sublanguage (e.g. the NE-free fragment).

Equations

• Core.Logic.Team.definableClassWhere s Q = {P : Core.Logic.Team.TeamProperty α | ∃ (φ : Form), Q φ ∧ P = Core.Logic.Team.definedBy s φ}

theorem Core.Logic.Team.definableClassWhere_subset {α : Type u_1} {Form : Type u_2} {s : Form → Finset α → Prop} {Q : Form → Prop} {C : TeamProperty α → Prop} (h : ∀ (φ : Form), Q φ → C (definedBy s φ)) : definableClassWhere s Q ⊆ {P : TeamProperty α | C P}

Fragment-relative soundness bridge. If every Q-formula's support set has closure property C, every Q-definable property does. The fragment analogue of definableClass_subset.

Closure cells

The classes of team properties the expressive-completeness theorems characterise logics against. The "cell" a logic occupies (see the cell map in Core/Logic/Modal/README.md) is an intersection of these: BSML is convexProperties ∩ unionClosedProperties, ML(⊆) and BSML⊘ are unionClosedProperties ∩ emptyTeamProperties, dependence and inquisitive logic are downwardClosedProperties ∩ emptyTeamProperties.

def Core.Logic.Team.downwardClosedProperties {α : Type u_1} : Set (TeamProperty α)

The class of downward-closed (persistent) team properties.

Equations

• Core.Logic.Team.downwardClosedProperties = {P : Core.Logic.Team.TeamProperty α | IsLowerSet P}

def Core.Logic.Team.convexProperties {α : Type u_1} : Set (TeamProperty α)

The class of convex team properties (Set.OrdConnected under ⊆).

Equations

• Core.Logic.Team.convexProperties = {P : Core.Logic.Team.TeamProperty α | Set.OrdConnected P}

def Core.Logic.Team.emptyTeamProperties {α : Type u_1} : Set (TeamProperty α)

The class of team properties with the empty-team property.

Equations

• Core.Logic.Team.emptyTeamProperties = {P : Core.Logic.Team.TeamProperty α | ∅ ∈ P}

def Core.Logic.Team.unionClosedProperties {α : Type u_1} [DecidableEq α] : Set (TeamProperty α)

The class of union-closed team properties.

Equations

• Core.Logic.Team.unionClosedProperties = {P : Core.Logic.Team.TeamProperty α | SupClosed P}

def Core.Logic.Team.flatProperties {α : Type u_1} : Set (TeamProperty α)

The flat team properties: downward-closed ∩ union-closed ∩ empty-team (Anttila Proposition 2.2.2, via Team/Closure.lean's isFlat_iff).

Equations

• Core.Logic.Team.flatProperties = {P : Core.Logic.Team.TeamProperty α | Core.Logic.Team.IsFlat P}