Team operations

A team-semantic connective takes the team properties defined by its arguments to the team property defined by the compound. The connectives are defined here once, as operations on TeamProperty α, so that each team logic's evaluation is a fold over them and each closure fact about a connective is proved once. They are the pointwise lift flat of a property of points, the tensor (split) disjunction tensor, the non-emptiness atom ne, and the modalities: Aloni's flat poss and nec over successor sets, Väänänen's single-witness possWitness and image necImage of modal dependence logic, and the lax possLax of modal inclusion logic.

The operations are mathlib's where mathlib has them. Tensor disjunction is the pointwise sup P ⊻ Q (Set.sups) of the lattice Finset α, so its closure lemmas are the lattice-general ones of Core/Data/Set/Sups.lean; conjunction is intersection; the image modality is the preimage of a property along the bundled SupBotHom biUnionHom R, so its closure lemmas are IsLowerSet.preimage and SupClosed.preimage. Following Anttila, flat properties and the flat modalities are flat outright, and flat commutes with conjunction, tensor disjunction and the flat modalities, so a formula built from flat atoms by these connectives defines a flat property, pointwise its classical truth.

Main definitions

• Team.flat, Team.tensor, Team.ne, Team.poss, Team.nec: the BSML connectives.
• Team.biUnionHom, Team.possWitness, Team.necImage, Team.possLax: the modal clauses of modal dependence and inclusion logic.

Main results

• Team.isFlat_flat, IsLowerSet.tensor, SupClosed.tensor, Team.empty_mem_tensor, Set.OrdConnected.tensor: closure per connective.
• Team.flat_inter, Team.tensor_flat, Team.poss_flat, Team.nec_flat, Team.possWitness_flat, Team.possLax_flat, Team.necImage_flat: flat is a homomorphism.
• Team.poss_union, Team.nec_union: the flat modalities send unions to tensor disjunctions.

Implementation notes

The pointwise connectives need no decidable equality on points and come first; the split and image connectives, which form unions of teams, follow under [DecidableEq α]. The bilateral anti-support of ne is the singleton property {∅}. Membership in each operation unfolds definitionally (mem_flat, mem_tensor, …), so a logic's evaluation clauses written through these operations are the same propositions as the paper's; a split of a team appears as a witness t₁ ∪ t₂ = t.

The points of a team are left abstract: worlds for BSML, world–assignment indices for QBSML, assignments for first-order dependence logic. "Team" is Väänänen's term; Aloni's state-based modal logics call the same object a "state".

References

• [Alo22] Aloni, Logic and Conversation: The Case of Free Choice
• [AAY24] Aloni, Anttila and Yang, State-based Modal Logics for Free Choice
• [Ant21] Anttila, The Logic of Free Choice: Axiomatizations of State-based Modal Logics
• [Ant25] Anttila, Not Nothing: Nonemptiness in Team Semantics
• [AHY25] Anttila, Häggblom and Yang, Axiomatizing modal inclusion logic and its variants
• [Vaa07] Väänänen, Dependence Logic: A New Approach to Independence Friendly Logic
• [Vaa08] Väänänen, Modal Dependence Logic

Pointwise connectives

def Team.flat {α : Type u_1} (p : α → Prop) : TeamProperty α

The pointwise lift flat p of a property of points holds of the teams all of whose points satisfy p. Atoms, and every flat connective, define such properties.

Equations

• Team.flat p = {t : Finset α | ∀ x ∈ t, p x}

def Team.ne {α : Type u_1} : TeamProperty α

The non-emptiness atom NE holds of the non-empty teams.

Equations

• Team.ne = {t : Finset α | t.Nonempty}

def Team.poss {α : Type u_1} (R : α → Finset α) (P : TeamProperty α) : TeamProperty α

The flat possibility modality over successor sets R holds of a team when every point of it has a non-empty set of successors in P.

Equations

• Team.poss R P = Team.flat fun (x : α) => ∃ s ⊆ R x, s.Nonempty ∧ s ∈ P

def Team.nec {α : Type u_1} (R : α → Finset α) (P : TeamProperty α) : TeamProperty α

The flat necessity modality holds of a team when the successor set of each of its points is in P.

Equations

• Team.nec R P = Team.flat fun (x : α) => R x ∈ P

def Team.possWitness {α : Type u_1} (R : α → Finset α) (P : TeamProperty α) : TeamProperty α

The single-witness possibility modality of modal dependence logic ([Vaa08] clause (T8), p. 245) holds of a team when one team Y in P supplies a successor to every point.

Equations

• Team.possWitness R P = {t : Finset α | ∃ (Y : Finset α), (∀ x ∈ t, ∃ y ∈ Y, y ∈ R x) ∧ Y ∈ P}

@[simp]

theorem Team.mem_flat {α : Type u_1} {p : α → Prop} {t : Finset α} : t ∈ flat p ↔ ∀ x ∈ t, p x

@[simp]

theorem Team.mem_ne {α : Type u_1} {t : Finset α} : t ∈ ne ↔ t.Nonempty

@[simp]

theorem Team.mem_poss {α : Type u_1} {P : TeamProperty α} {R : α → Finset α} {t : Finset α} : t ∈ poss R P ↔ ∀ x ∈ t, ∃ s ⊆ R x, s.Nonempty ∧ s ∈ P

@[simp]

theorem Team.mem_nec {α : Type u_1} {P : TeamProperty α} {R : α → Finset α} {t : Finset α} : t ∈ nec R P ↔ ∀ x ∈ t, R x ∈ P

@[simp]

theorem Team.mem_possWitness {α : Type u_1} {P : TeamProperty α} {R : α → Finset α} {t : Finset α} : t ∈ possWitness R P ↔ ∃ (Y : Finset α), (∀ x ∈ t, ∃ y ∈ Y, y ∈ R x) ∧ Y ∈ P

@[instance_reducible]

instance Team.flat.instDecidableMem {α : Type u_1} {p : α → Prop} [DecidablePred p] (t : Finset α) : Decidable (t ∈ flat p)

Equations

• Team.flat.instDecidableMem t = Finset.decidableDforallFinset

@[instance_reducible]

instance Team.ne.instDecidableMem {α : Type u_1} (t : Finset α) : Decidable (t ∈ ne)

Equations

• Team.ne.instDecidableMem t = { decide := decide (∃ a ∈ t, true = true), reflects_decide := ⋯ }

@[instance_reducible]

instance Team.nec.instDecidableMem {α : Type u_1} (R : α → Finset α) (P : TeamProperty α) [DecidablePred fun (x : Finset α) => x ∈ P] (t : Finset α) : Decidable (t ∈ nec R P)

Equations

• Team.nec.instDecidableMem R P t = { decide := decide (∀ a ∈ t.val.attach, (fun (x : α) (a : x ∈ t) => R x ∈ P) ↑a ⋯), reflects_decide := ⋯ }

theorem Team.isFlat_flat {α : Type u_1} (p : α → Prop) : IsFlat (flat p)

theorem Team.ordConnected_ne {α : Type u_1} : Set.OrdConnected ne

theorem Team.isLowerSet_singleton_empty {α : Type u_1} : IsLowerSet {∅}

theorem Team.ordConnected_singleton_empty {α : Type u_1} : Set.OrdConnected {∅}

theorem Team.isLowerSet_possWitness {α : Type u_1} (R : α → Finset α) (P : TeamProperty α) : IsLowerSet (possWitness R P)

theorem Team.empty_mem_possWitness {α : Type u_1} {P : TeamProperty α} {R : α → Finset α} (hP : ∅ ∈ P) : ∅ ∈ possWitness R P

theorem Team.flat_inter {α : Type u_1} (p q : α → Prop) : flat p ∩ flat q = flat fun (x : α) => p x ∧ q x

flat commutes with conjunction.

theorem Team.exists_nonempty_subset_forall_iff {α : Type u_1} (u : Finset α) (p : α → Prop) : (∃ t ⊆ u, t.Nonempty ∧ ∀ x ∈ t, p x) ↔ ∃ x ∈ u, p x

A non-empty subteam of u on which p holds pointwise exists exactly when p holds somewhere in u, since the witness may be taken to be a singleton.

theorem Team.poss_flat {α : Type u_1} (R : α → Finset α) (p : α → Prop) : poss R (flat p) = flat fun (x : α) => ∃ y ∈ R x, p y

flat commutes with the flat possibility modality.

theorem Team.nec_flat {α : Type u_1} (R : α → Finset α) (p : α → Prop) : nec R (flat p) = flat fun (x : α) => ∀ y ∈ R x, p y

flat commutes with the flat necessity modality.

Split and image connectives

def Team.tensor {α : Type u_1} [DecidableEq α] (P Q : TeamProperty α) : TeamProperty α

Tensor (split) disjunction holds of the teams that split into a part in P and a part in Q. It is the pointwise sup P ⊻ Q of Finset α (tensor_eq_sups), spelled out so that a split appears as t₁ ∪ t₂ = t.

Equations

• Team.tensor P Q = {t : Finset α | ∃ t₁ ∈ P, ∃ t₂ ∈ Q, t₁ ∪ t₂ = t}

theorem Team.tensor_eq_sups {α : Type u_1} [DecidableEq α] (P Q : TeamProperty α) : tensor P Q = P ⊻ Q

def Team.biUnionHom {α : Type u_1} [DecidableEq α] {β : Type u_2} [DecidableEq β] (R : α → Finset β) : SupBotHom (Finset α) (Finset β)

The image of a team under successor sets, t ↦ t.biUnion R, as a map of the bounded join-semilattices of teams.

Equations

• Team.biUnionHom R = { toFun := fun (t : Finset α) => t.biUnion R, map_sup' := ⋯, map_bot' := ⋯ }

@[simp]

theorem Team.biUnionHom_apply {α : Type u_1} [DecidableEq α] {β : Type u_2} [DecidableEq β] (R : α → Finset β) (t : Finset α) : (biUnionHom R) t = t.biUnion R

def Team.necImage {α : Type u_1} [DecidableEq α] (R : α → Finset α) (P : TeamProperty α) : TeamProperty α

The image necessity modality ([Vaa08] clause (T9), p. 245) holds of a team when the union of its successor sets is in P.

Equations

• Team.necImage R P = ⇑(Team.biUnionHom R) ⁻¹' P

def Team.possLax {α : Type u_1} [DecidableEq α] (R : α → Finset α) (P : TeamProperty α) : TeamProperty α

The lax possibility modality of modal inclusion logic ([AHY25] Definition 2.2) holds of a team when some team of successors in P reaches every point.

Equations

• Team.possLax R P = {t : Finset α | ∃ S ⊆ t.biUnion R, (∀ x ∈ t, ∃ y ∈ S, y ∈ R x) ∧ S ∈ P}

@[simp]

theorem Team.mem_tensor {α : Type u_1} {P : TeamProperty α} {t : Finset α} [DecidableEq α] {Q : TeamProperty α} : t ∈ tensor P Q ↔ ∃ t₁ ∈ P, ∃ t₂ ∈ Q, t₁ ∪ t₂ = t

@[simp]

theorem Team.mem_necImage {α : Type u_1} {P : TeamProperty α} {R : α → Finset α} {t : Finset α} [DecidableEq α] : t ∈ necImage R P ↔ t.biUnion R ∈ P

@[simp]

theorem Team.mem_possLax {α : Type u_1} {P : TeamProperty α} {R : α → Finset α} {t : Finset α} [DecidableEq α] : t ∈ possLax R P ↔ ∃ S ⊆ t.biUnion R, (∀ x ∈ t, ∃ y ∈ S, y ∈ R x) ∧ S ∈ P

@[instance_reducible]

instance Team.tensor.instDecidableMem {α : Type u_1} [DecidableEq α] [Fintype α] (P Q : TeamProperty α) [DecidablePred fun (x : Finset α) => x ∈ P] [DecidablePred fun (x : Finset α) => x ∈ Q] (t : Finset α) : Decidable (t ∈ tensor P Q)

Equations

• Team.tensor.instDecidableMem P Q t = { decide := decide (∃ a ∈ Finset.univ, (fun (t₁ : Finset α) => t₁ ∈ P ∧ ∃ t₂ ∈ Q, t₁ ∪ t₂ = t) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Team.poss.instDecidableMem {α : Type u_1} [DecidableEq α] [Fintype α] (R : α → Finset α) (P : TeamProperty α) [DecidablePred fun (x : Finset α) => x ∈ P] (t : Finset α) : Decidable (t ∈ poss R P)

Equations

• Team.poss.instDecidableMem R P t = { decide := decide (∀ a ∈ Finset.univ, (fun (x : α) => x ∈ t → ∃ s ⊆ R x, s.Nonempty ∧ s ∈ P) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Team.possWitness.instDecidableMem {α : Type u_1} [DecidableEq α] [Fintype α] (R : α → Finset α) (P : TeamProperty α) [DecidablePred fun (x : Finset α) => x ∈ P] (t : Finset α) : Decidable (t ∈ possWitness R P)

Equations

• Team.possWitness.instDecidableMem R P t = { decide := decide (∃ a ∈ Finset.univ, (fun (Y : Finset α) => (∀ x ∈ t, ∃ y ∈ Y, y ∈ R x) ∧ Y ∈ P) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Team.necImage.instDecidableMem {α : Type u_1} [DecidableEq α] (R : α → Finset α) (P : TeamProperty α) [DecidablePred fun (x : Finset α) => x ∈ P] (t : Finset α) : Decidable (t ∈ necImage R P)

Equations

• Team.necImage.instDecidableMem R P t = Team.necImage.instDecidableMem._aux_1 R P t

@[instance_reducible]

instance Team.possLax.instDecidableMem {α : Type u_1} [DecidableEq α] [Fintype α] (R : α → Finset α) (P : TeamProperty α) [DecidablePred fun (x : Finset α) => x ∈ P] (t : Finset α) : Decidable (t ∈ possLax R P)

Equations

• One or more equations did not get rendered due to their size.

Flat properties

theorem Team.isLowerSet_flat {α : Type u_1} [DecidableEq α] (p : α → Prop) : IsLowerSet (flat p)

theorem Team.supClosed_flat {α : Type u_1} [DecidableEq α] (p : α → Prop) : SupClosed (flat p)

theorem Team.empty_mem_flat {α : Type u_1} [DecidableEq α] (p : α → Prop) : ∅ ∈ flat p

theorem Team.ordConnected_flat {α : Type u_1} [DecidableEq α] (p : α → Prop) : Set.OrdConnected (flat p)

The non-emptiness atom

theorem Team.supClosed_ne {α : Type u_1} [DecidableEq α] : SupClosed ne

theorem Team.supClosed_singleton_empty {α : Type u_1} [DecidableEq α] : SupClosed {∅}

Tensor disjunction ([Ant21] Proposition 2.2.8)

The closure lemmas are those of ⊻ in the distributive lattice Finset α.

theorem IsLowerSet.tensor {α : Type u_1} {P : Team.TeamProperty α} [DecidableEq α] {Q : Team.TeamProperty α} (hP : IsLowerSet P) (hQ : IsLowerSet Q) : IsLowerSet (Team.tensor P Q)

theorem SupClosed.tensor {α : Type u_1} {P : Team.TeamProperty α} [DecidableEq α] {Q : Team.TeamProperty α} (hP : SupClosed P) (hQ : SupClosed Q) : SupClosed (Team.tensor P Q)

theorem Team.empty_mem_tensor {α : Type u_1} {P : TeamProperty α} [DecidableEq α] {Q : TeamProperty α} (hP : ∅ ∈ P) (hQ : ∅ ∈ Q) : ∅ ∈ tensor P Q

theorem Set.OrdConnected.tensor {α : Type u_1} {P : Team.TeamProperty α} [DecidableEq α] {Q : Team.TeamProperty α} (hP : OrdConnected P) (hQ : OrdConnected Q) (hP' : SupClosed P) (hQ' : SupClosed Q) : OrdConnected (Team.tensor P Q)

Tensor disjunction preserves convexity when both disjuncts are union-closed ([Ant25] Proposition 3.3.1).

The modalities of dependence and inclusion logic

theorem SupClosed.possWitness {α : Type u_1} {P : Team.TeamProperty α} {R : α → Finset α} [DecidableEq α] (hP : SupClosed P) : SupClosed (Team.possWitness R P)

theorem IsLowerSet.necImage {α : Type u_1} {P : Team.TeamProperty α} {R : α → Finset α} [DecidableEq α] (hP : IsLowerSet P) : IsLowerSet (Team.necImage R P)

theorem SupClosed.necImage {α : Type u_1} {P : Team.TeamProperty α} {R : α → Finset α} [DecidableEq α] (hP : SupClosed P) : SupClosed (Team.necImage R P)

theorem Team.empty_mem_necImage {α : Type u_1} {P : TeamProperty α} {R : α → Finset α} [DecidableEq α] (hP : ∅ ∈ P) : ∅ ∈ necImage R P

theorem IsLowerSet.possLax {α : Type u_1} {P : Team.TeamProperty α} {R : α → Finset α} [DecidableEq α] (hP : IsLowerSet P) : IsLowerSet (Team.possLax R P)

theorem SupClosed.possLax {α : Type u_1} {P : Team.TeamProperty α} {R : α → Finset α} [DecidableEq α] (hP : SupClosed P) : SupClosed (Team.possLax R P)

theorem Team.empty_mem_possLax {α : Type u_1} {P : TeamProperty α} {R : α → Finset α} [DecidableEq α] (hP : ∅ ∈ P) : ∅ ∈ possLax R P

flat commutes with tensor disjunction ([Ant21] Proposition 2.2.16)

theorem Team.mem_tensor_flat {α : Type u_1} {p q : α → Prop} {t : Finset α} [DecidableEq α] : t ∈ tensor (flat p) (flat q) ↔ ∀ x ∈ t, p x ∨ q x

A team of points satisfying p ∨ q splits into its p-points and its ¬p-points.

theorem Team.tensor_flat {α : Type u_1} [DecidableEq α] (p q : α → Prop) : tensor (flat p) (flat q) = flat fun (x : α) => p x ∨ q x

theorem Team.poss_union {α : Type u_1} [DecidableEq α] (R : α → Finset α) (P Q : TeamProperty α) : poss R (P ∪ Q) = tensor (poss R P) (poss R Q)

The flat possibility modality turns a union into a tensor disjunction. This is the law behind ◇(φ ⩔ ψ) ≡ ◇φ ∨ ◇ψ in [AAY24].

theorem Team.nec_union {α : Type u_1} [DecidableEq α] (R : α → Finset α) (P Q : TeamProperty α) : nec R (P ∪ Q) = tensor (nec R P) (nec R Q)

The flat necessity modality turns a union into a tensor disjunction.

flat commutes with the image modalities

On flat properties the single-witness, lax and image modalities agree with the flat ones: the witness team may be taken to be the p-successors of the team.

theorem Team.mem_possWitness_flat {α : Type u_1} {p : α → Prop} {R : α → Finset α} {t : Finset α} [DecidableEq α] : t ∈ possWitness R (flat p) ↔ ∀ x ∈ t, ∃ y ∈ R x, p y

theorem Team.possWitness_flat {α : Type u_1} [DecidableEq α] (R : α → Finset α) (p : α → Prop) : possWitness R (flat p) = flat fun (x : α) => ∃ y ∈ R x, p y

theorem Team.mem_possLax_flat {α : Type u_1} {p : α → Prop} {R : α → Finset α} {t : Finset α} [DecidableEq α] : t ∈ possLax R (flat p) ↔ ∀ x ∈ t, ∃ y ∈ R x, p y

theorem Team.possLax_flat {α : Type u_1} [DecidableEq α] (R : α → Finset α) (p : α → Prop) : possLax R (flat p) = flat fun (x : α) => ∃ y ∈ R x, p y

theorem Team.mem_necImage_flat {α : Type u_1} {p : α → Prop} {R : α → Finset α} {t : Finset α} [DecidableEq α] : t ∈ necImage R (flat p) ↔ ∀ x ∈ t, ∀ y ∈ R x, p y

theorem Team.necImage_flat {α : Type u_1} [DecidableEq α] (R : α → Finset α) (p : α → Prop) : necImage R (flat p) = flat fun (x : α) => ∀ y ∈ R x, p y