Team Semantics Infrastructure

@cite{aloni-2022} @cite{ciardelli-groenendijk-roelofsen-2018}

Team semantics evaluates formulas relative to sets of evaluation points (teams) rather than single points. This module provides the core infrastructure.

Background

Team semantics originated in logic and has been applied to linguistics for:

• Inquisitive Semantics: questions as issues (sets of info states)
• Free Choice: Aloni's BSML derives FC via non-emptiness constraints
• Modified Numerals: first-order team semantics
• Exceptional Scope: indefinites with team-based evaluation

Key Concepts

• Team W: A set of worlds (characteristic function W -> Bool)
• Team operations: empty, full, singleton, subset, union, intersection, etc.

Architecture

This module provides general infrastructure. Specific applications:

• Systems/BSML/: Bilateral State-based Modal Logic
• Questions/Inquisitive.lean: Inquisitive semantics for questions

@[reducible, inline]

abbrev Semantics.Dynamic.TeamSemantics.Team (W : Type u_1) : Type u_1

A team is a set of worlds, represented as a characteristic function.

In team semantics, formulas are evaluated relative to teams rather than single worlds. A team represents an information state: the set of worlds compatible with current information.

This is equivalent to InfoState in Inquisitive Semantics.

Equations

• Semantics.Dynamic.TeamSemantics.Team W = (W → Bool)

def Semantics.Dynamic.TeamSemantics.Team.empty {W : Type u_1} : Team W

The empty team (inconsistent information state)

Equations

• Semantics.Dynamic.TeamSemantics.Team.empty x✝ = false

def Semantics.Dynamic.TeamSemantics.Team.full {W : Type u_1} : Team W

The full team (no information / total ignorance)

Equations

• Semantics.Dynamic.TeamSemantics.Team.full x✝ = true

def Semantics.Dynamic.TeamSemantics.Team.singleton {W : Type u_1} [DecidableEq W] (w : W) : Team W

Singleton team containing just one world

Equations

• Semantics.Dynamic.TeamSemantics.Team.singleton w w' = (w == w')

def Semantics.Dynamic.TeamSemantics.Team.isEmpty {W : Type u_1} (t : Team W) (worlds : List W) : Bool

Check if a team is empty (no worlds)

Equations

• t.isEmpty worlds = !worlds.any t

def Semantics.Dynamic.TeamSemantics.Team.isNonEmpty {W : Type u_1} (t : Team W) (worlds : List W) : Bool

Check if a team is non-empty

Equations

• t.isNonEmpty worlds = worlds.any t

def Semantics.Dynamic.TeamSemantics.Team.mem {W : Type u_1} (t : Team W) (w : W) : Bool

Team membership: world w is in team t

Equations

• t.mem w = t w

def Semantics.Dynamic.TeamSemantics.Team.subset {W : Type u_1} (t t' : Team W) (worlds : List W) : Bool

Team subset: t ⊆ t'

Equations

• t.subset t' worlds = worlds.all fun (w : W) => !t w || t' w

def Semantics.Dynamic.TeamSemantics.Team.inter {W : Type u_1} (t t' : Team W) : Team W

Team intersection: t ∩ t'

Equations

• t.inter t' w = (t w && t' w)

def Semantics.Dynamic.TeamSemantics.Team.union {W : Type u_1} (t t' : Team W) : Team W

Team union: t ∪ t'

Equations

• t.union t' w = (t w || t' w)

def Semantics.Dynamic.TeamSemantics.Team.compl {W : Type u_1} (t : Team W) : Team W

Team complement: W \ t

Equations

• t.compl w = !t w

def Semantics.Dynamic.TeamSemantics.Team.diff {W : Type u_1} (t t' : Team W) : Team W

Team difference: t \ t'

Equations

• t.diff t' w = (t w && !t' w)

def Semantics.Dynamic.TeamSemantics.Team.filter {W : Type u_1} (t : Team W) (p : W → Bool) : Team W

Filter team by predicate

Equations

• t.filter p w = (t w && p w)

def Semantics.Dynamic.TeamSemantics.Team.all {W : Type u_1} (t : Team W) (p : W → Bool) (worlds : List W) : Bool

All worlds in team satisfy predicate

Equations

• t.all p worlds = worlds.all fun (w : W) => !t w || p w

def Semantics.Dynamic.TeamSemantics.Team.any {W : Type u_1} (t : Team W) (p : W → Bool) (worlds : List W) : Bool

Some world in team satisfies predicate

Equations

• t.any p worlds = worlds.any fun (w : W) => t w && p w

def Semantics.Dynamic.TeamSemantics.Team.toList {W : Type u_1} (t : Team W) (worlds : List W) : List W

Convert team to list of worlds

Equations

• t.toList worlds = List.filter t worlds

def Semantics.Dynamic.TeamSemantics.Team.ofList {W : Type u_1} [DecidableEq W] (ws : List W) : Team W

Team from list of worlds

Equations

• Semantics.Dynamic.TeamSemantics.Team.ofList ws w = ws.contains w

def Semantics.Dynamic.TeamSemantics.Team.beq {W : Type u_1} (t t' : Team W) (worlds : List W) : Bool

Team equality (extensional, given finite world list)

Equations

• t.beq t' worlds = worlds.all fun (w : W) => t w == t' w