Team algebra — pure Finset combinatorics for team semantics

@cite{anttila-2021} @cite{vaananen-2007} @cite{yang-vaananen-2017}

The combinatorial primitives underlying team-semantic logics — BSML (Aloni 2022), QBSML (Aloni & van Ormondt 2023), propositional team logic PT⁺ (Yang & Väänänen 2017), modal team logic MTL (Hella et al., Lück), modal dependence logic MDᵂ (Yang), and inquisitive variants.

This file is theory-neutral: nothing in it knows about evaluation, support, or formulas. It provides only the partition relations on teams and the frame conditions on accessibility.

Naming: "team" vs. "state"

We use "team" (Hodges 1997, Väänänen 2007) — the foundational term in dependence/independence logic and propositional team logic. Aloni's "state-based modal logic" papers use "state" for the same object (a subset of evaluation points), inheriting via Anttila 2021. The two terms are interchangeable in this layer; "team" is preferred here because it generalizes cleanly: a team can be a set of worlds (BSML), a set of (world, assignment) pairs (QBSML), a set of assignments (dependence logic), etc., without the "state" connotation of "set of worlds".

Two layers in this file

1. Team partition (splitsAs, splitsAsNE): the structural condition underlying team-semantic split disjunction.

2. Frame conditions on accessibility (isStateBased, isIndisputable): Anttila Definition 2.2.10-equivalent properties of a relation R : W → Finset W relative to a base team. Used to distinguish epistemic and deontic modalities (Aloni 2022 §6.1).

We retain the term "state-based" in isStateBased because that is its established name in the Aloni / Anttila literature — the property holds of an accessibility relation, not of a team-semantic logic generally.

@[reducible, inline]

abbrev Core.Logic.Team.splitsAs {α : Type u_1} [DecidableEq α] (s t₁ t₂ : Finset α) : Prop

Binary cover: team s is the union of teams t₁ and t₂. The two sub-teams may overlap; only their union must equal s. This is the structural condition under team-semantic split disjunction (also called tensor disjunction in dependence logic; cf. Anttila 2021 Definition 2.1.5, Yang & Väänänen 2017).

Argument order s t₁ t₂ reads as "splits team s into t₁ and t₂".

Defined as abbrev so that t₁ ∪ t₂ = s reduces transparently in proofs — consumers don't need unfold splitsAs and can pattern-match on the underlying union equation directly.

Equations

• Core.Logic.Team.splitsAs s t₁ t₂ = (t₁ ∪ t₂ = s)

@[reducible, inline]

abbrev Core.Logic.Team.splitsAsNE {α : Type u_1} [DecidableEq α] (s t₁ t₂ : Finset α) : Prop

Binary cover with both parts non-empty. Used by pragmatically-enriched split disjunction in BSML+ / QBSML+ (Aloni 2022 §3.3): [φ ∨ ψ]⁺ requires both sub-teams to be non-empty (forced by the NE conjunct propagating through enrichment).

Equations

• Core.Logic.Team.splitsAsNE s t₁ t₂ = (t₁ ∪ t₂ = s ∧ t₁.Nonempty ∧ t₂.Nonempty)

theorem Core.Logic.Team.splitsAsNE_imp_splitsAs {α : Type u_1} [DecidableEq α] (s t₁ t₂ : Finset α) (h : splitsAsNE s t₁ t₂) : splitsAs s t₁ t₂

theorem Core.Logic.Team.splitsAs_self_empty {α : Type u_1} [DecidableEq α] (s : Finset α) : splitsAs s s ∅

The trivial split: s = s ∪ ∅. Used by classical formulas, which are supported on the empty team vacuously.

theorem Core.Logic.Team.splitsAs_empty_self {α : Type u_1} [DecidableEq α] (s : Finset α) : splitsAs s ∅ s

theorem Core.Logic.Team.splitsAs_self_self {α : Type u_1} [DecidableEq α] (s : Finset α) : splitsAs s s s

The reflexive split: s = s ∪ s (parts may overlap).

theorem Core.Logic.Team.splitsAs_symm {α : Type u_1} [DecidableEq α] {s t₁ t₂ : Finset α} (h : splitsAs s t₁ t₂) : splitsAs s t₂ t₁

theorem Core.Logic.Team.splitsAsNE_symm {α : Type u_1} [DecidableEq α] {s t₁ t₂ : Finset α} (h : splitsAsNE s t₁ t₂) : splitsAs s t₂ t₁ ∧ t₂.Nonempty ∧ t₁.Nonempty

theorem Core.Logic.Team.splitsAs_left_subset {α : Type u_1} [DecidableEq α] {s t₁ t₂ : Finset α} (h : splitsAs s t₁ t₂) : t₁ ⊆ s

Substate property: if splitsAs s t₁ t₂, then t₁ ⊆ s.

theorem Core.Logic.Team.splitsAs_right_subset {α : Type u_1} [DecidableEq α] {s t₁ t₂ : Finset α} (h : splitsAs s t₁ t₂) : t₂ ⊆ s

@[implicit_reducible]

instance Core.Logic.Team.instDecidableSplitsAs {α : Type u_1} [DecidableEq α] (s t₁ t₂ : Finset α) : Decidable (splitsAs s t₁ t₂)

Equations

• Core.Logic.Team.instDecidableSplitsAs s t₁ t₂ = decEq (t₁ ∪ t₂) s

@[implicit_reducible]

instance Core.Logic.Team.instDecidableSplitsAsNE {α : Type u_1} [DecidableEq α] (s t₁ t₂ : Finset α) : Decidable (splitsAsNE s t₁ t₂)

Equations

• Core.Logic.Team.instDecidableSplitsAsNE s t₁ t₂ = instDecidableAnd

def Core.Logic.Team.isStateBased {W : Type u_1} (R : W → Finset W) (s : Finset W) : Prop

R is state-based on team s iff every world in s is R-accessible exactly to s. Strictly stronger than indisputability.

Aloni 2022 Definition 5; Anttila 2021 Definition 4.10-style. The name is established in the BSML literature even though we use "team" for the underlying object — the property pertains to the accessibility relation, not the team itself.

Equations

• Core.Logic.Team.isStateBased R s = ∀ w ∈ s, R w = s

def Core.Logic.Team.isIndisputable {W : Type u_1} (R : W → Finset W) (s : Finset W) : Prop

R is indisputable on team s iff all worlds in s see the same set of accessible worlds. Equivalently: R is constant on s.

Aloni 2022 Definition 5 (indisputable ↔ deontic-with-knowledgeable-speaker).

Equations

• Core.Logic.Team.isIndisputable R s = ∀ w₁ ∈ s, ∀ w₂ ∈ s, R w₁ = R w₂

theorem Core.Logic.Team.isStateBased_imp_isIndisputable {W : Type u_1} (R : W → Finset W) (s : Finset W) (h : isStateBased R s) : isIndisputable R s

State-based implies indisputable.

@[implicit_reducible]

instance Core.Logic.Team.instDecidableIsStateBasedOfDecidableEqOfFintype {W : Type u_1} (R : W → Finset W) (s : Finset W) [DecidableEq W] [Fintype W] : Decidable (isStateBased R s)

Equations

• Core.Logic.Team.instDecidableIsStateBasedOfDecidableEqOfFintype R s = id inferInstance

@[implicit_reducible]

instance Core.Logic.Team.instDecidableIsIndisputableOfDecidableEqOfFintype {W : Type u_1} (R : W → Finset W) (s : Finset W) [DecidableEq W] [Fintype W] : Decidable (isIndisputable R s)

Equations

• Core.Logic.Team.instDecidableIsIndisputableOfDecidableEqOfFintype R s = id inferInstance