Closure properties of team properties

A team property T : TeamProperty α is a class of teams, Set (Finset α); a formula of a team logic defines the property of the teams supporting it. T is flat if its membership reduces pointwise: s ∈ T ↔ ∀ w ∈ s, {w} ∈ T. This file states the flatness property of [Ant21] (Definition 2.2.1) and proves its closure-property characterisation (Proposition 2.2.2): a flat team property is downward-closed, sup-closed, and contains ∅.

Over SemilatticeSup-with-OrderBot carriers (which Finset α is) the three closure properties coincide with the data of an Order.IsIdeal: sup-closure ⟺ directedness (via SupClosed.directedOn), and ∅ ∈ T ⟺ T.Nonempty (via IsLowerSet.bot_mem, both in mathlib). This file proves the bridge IsFlat T ↔ Order.IsIdeal T, exposing mathlib's order-ideal infrastructure to consumers of IsFlat.

Main definitions

• Team.TeamProperty α — a class of teams.
• Team.IsFlat T — Anttila's pointwise flatness predicate.

Main results

• Team.isFlat_iff — [Ant21] Proposition 2.2.2.
• Team.isFlat_iff_isIdeal — flat team properties are precisely the carriers of order-ideals of Finset α.
• Team.isLowerSet_iff_ordConnected_of_empty — given the empty-team property, downward closure coincides with convexity (Set.OrdConnected). Convexity ([Ant25]) is the closure invariant that survives in the NE-bearing setting where the empty-team property fails. We reuse mathlib's Set.OrdConnected rather than a bespoke predicate, mirroring the IsFlat ↔ Order.IsIdeal bridge.

References

• [Ant21] Anttila, The Logic of Free Choice: Axiomatizations of State-based Modal Logics
• [Ant25] Anttila, Not Nothing: Nonemptiness in Team Semantics
• [Vaa07] Väänänen, Dependence Logic: A New Approach to Independence Friendly Logic

TODO

• Generalise IsFlat to atomistic lattices ([SemilatticeSup L] [OrderBot L] [IsAtomistic L]) once a non-Finset consumer surfaces.

@[reducible, inline]

abbrev Team.TeamProperty (α : Type u_2) : Type u_2

A team property over points α is a class of teams.

Equations

• Team.TeamProperty α = Set (Finset α)

def Team.IsFlat {α : Type u_1} (T : TeamProperty α) : Prop

A team property T is flat iff membership reduces pointwise: s ∈ T ↔ every singleton from s is in T.

[Ant21] Definition 2.2.1. Equivalent characterisations: isFlat_iff (via closure properties), isFlat_iff_isIdeal (via Order.IsIdeal).

Equations

• Team.IsFlat T = ∀ (s : Finset α), s ∈ T ↔ ∀ w ∈ s, {w} ∈ T

theorem Team.isFlat_iff {α : Type u_1} [DecidableEq α] (T : TeamProperty α) : IsFlat T ↔ IsLowerSet T ∧ SupClosed T ∧ ∅ ∈ T

[Ant21] Proposition 2.2.2: a team property is flat iff it is downward-closed under inclusion, closed under binary union, and contains the empty team.

theorem Team.isFlat_of_isLowerSet_supClosed_empty {α : Type u_1} [DecidableEq α] {T : TeamProperty α} (hLower : IsLowerSet T) (hSup : SupClosed T) (hEmpty : ∅ ∈ T) : IsFlat T

theorem Team.IsFlat.isLowerSet {α : Type u_1} [DecidableEq α] {T : TeamProperty α} (h : IsFlat T) : IsLowerSet T

theorem Team.IsFlat.supClosed {α : Type u_1} [DecidableEq α] {T : TeamProperty α} (h : IsFlat T) : SupClosed T

theorem Team.IsFlat.empty_mem {α : Type u_1} [DecidableEq α] {T : TeamProperty α} (h : IsFlat T) : ∅ ∈ T

theorem Team.isFlat_iff_isIdeal {α : Type u_1} [DecidableEq α] (T : TeamProperty α) : IsFlat T ↔ Order.IsIdeal T

[Ant21] Proposition 2.2.2 restated via Order.IsIdeal: flat team properties are precisely the carriers of order-ideals of Finset α.

Over SemilatticeSup + OrderBot the three closure-property coordinates of IsFlat translate to the three ideal-axiom coordinates: SupClosed ↔ DirectedOn (·≤·) (in SemilatticeSup) and ∅ ∈ T ↔ T.Nonempty (in OrderBot, for lower sets).

Convexity

Convexity — Set.OrdConnected on (Finset α, ⊆), i.e. s ⊆ t ⊆ u with s, u ∈ T forces t ∈ T — is [Ant25]'s generalization of downward closure to the NE-bearing setting where the empty-team property may fail. Mathlib's Set.OrdConnected is exactly this predicate (Set.Icc s u ⊆ T), so we reuse it rather than introduce a bespoke IsConvex, mirroring the IsFlat ↔ Order.IsIdeal reuse above. The forward bridge IsLowerSet.ordConnected is already in mathlib.

theorem Team.isLowerSet_of_ordConnected_empty {α : Type u_1} {T : TeamProperty α} (hConv : Set.OrdConnected T) (hEmpty : ∅ ∈ T) : IsLowerSet T

A convex team property with the empty-team property is downward-closed — the reverse of mathlib's IsLowerSet.ordConnected. Together they give isLowerSet_iff_ordConnected_of_empty.

theorem Team.isLowerSet_iff_ordConnected_of_empty {α : Type u_1} {T : TeamProperty α} (hEmpty : ∅ ∈ T) : IsLowerSet T ↔ Set.OrdConnected T

Given the empty-team property, downward closure and convexity coincide ([Ant25]). For NE-bearing team properties — which break the empty-team property — convexity is the invariant that survives where downward closure does not.

theorem Team.IsFlat.ordConnected {α : Type u_1} [DecidableEq α] {T : TeamProperty α} (h : IsFlat T) : Set.OrdConnected T

Flat team properties are convex (IsFlat → IsLowerSet → OrdConnected).