Common Ground

@cite{stalnaker-1974} @cite{stalnaker-2002}

Framework-agnostic context management following @cite{stalnaker-1974}: context sets (Set W), common ground as proposition lists (CG W), and the HasContextSet interface unifying both with the various discourse-state representations across Theories/.

Multi-agent epistemic operators (knowledge, belief, common knowledge) are in Theories/Semantics/Modality/EpistemicLogic.lean.

@[reducible, inline]

abbrev Core.CommonGround.ContextSet (W : Type u_1) : Type u_1

A context set is the set of worlds compatible with the common ground.

Just Set W. The namespace ContextSet.* provides discourse-meaningful aliases (entails, update, compatible) backed by mathlib Set ops.

Equations

• Core.CommonGround.ContextSet W = Set W

@[reducible, inline]

abbrev Core.CommonGround.ContextSet.trivial {W : Type u_1} : ContextSet W

The trivial context: all worlds possible. Alias for Set.univ.

Equations

• Core.CommonGround.ContextSet.trivial = Set.univ

@[reducible, inline]

abbrev Core.CommonGround.ContextSet.entails {W : Type u_1} (c : ContextSet W) (p : Set W) : Prop

Entailment: every world in the context satisfies the proposition. Thin alias for (· ⊆ ·) so that the ⊧ notation reads naturally.

Equations

• (c ⊧ p) = (c ⊆ p)

def Core.CommonGround.ContextSet.«term_⊧_» : Lean.TrailingParserDescr

Entailment: every world in the context satisfies the proposition. Thin alias for (· ⊆ ·) so that the ⊧ notation reads naturally.

Equations

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

@[reducible, inline]

abbrev Core.CommonGround.ContextSet.nonEmpty {W : Type u_1} (c : ContextSet W) : Prop

The context set has at least one world. Alias for Set.Nonempty.

Equations

• c.nonEmpty = Set.Nonempty c

@[reducible, inline]

abbrev Core.CommonGround.ContextSet.compatible {W : Type u_1} (c : ContextSet W) (p : Set W) : Prop

Compatibility: some world in the context satisfies the proposition.

Equations

• c.compatible p = Set.Nonempty (c ∩ p)

@[reducible, inline]

abbrev Core.CommonGround.ContextSet.update {W : Type u_1} (c : ContextSet W) (p : Set W) : ContextSet W

Update: keep only worlds where the proposition holds. Alias for (· ∩ ·).

Equations

• c.update p = c ∩ p

def Core.CommonGround.ContextSet.«term_+_» : Lean.TrailingParserDescr

Update: keep only worlds where the proposition holds. Alias for (· ∩ ·).

Equations

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

theorem Core.CommonGround.ContextSet.update_entails {W : Type u_1} (c : ContextSet W) (p : Set W) : c.update p ⊧ p

Updated context entails the update proposition.

theorem Core.CommonGround.ContextSet.update_restricts {W : Type u_1} (c : ContextSet W) (p : Set W) : c.update p ⊆ c

Updated context is contained in the original.

theorem Core.CommonGround.ContextSet.update_entailed {W : Type u_1} (c : ContextSet W) (p : Set W) (h : c ⊧ p) : c.update p = c

Updating with what's already entailed doesn't change the context.

theorem Core.CommonGround.ContextSet.update_assoc {W : Type u_1} (c p q : Set W) : (update c p).update q = update c (update p q)

Sequential updates are associative.

theorem Core.CommonGround.ContextSet.trivial_update {W : Type u_1} (p : Set W) : trivial.update p = p

Updating trivial context with p gives p.

theorem Core.CommonGround.ContextSet.entails_mono {W : Type u_1} {c₁ c₂ : ContextSet W} {p : Set W} (h_sub : c₁ ⊆ c₂) (h_ent : c₂ ⊧ p) : c₁ ⊧ p

Entailment is monotonic: a smaller context entails everything a larger one does.

theorem Core.CommonGround.ContextSet.update_mono {W : Type u_1} {c₁ c₂ : ContextSet W} (p : Set W) (h : c₁ ⊆ c₂) : c₁.update p ⊆ c₂.update p

Update is monotonic in the context.

structure Core.CommonGround.CG (W : Type u_1) : Type u_1

Common ground as a list of mutually believed propositions.

• propositions : List (Set W)

  The propositions in the common ground

def Core.CommonGround.CG.contextSet {W : Type u_1} (cg : CG W) : ContextSet W

The context set determined by a common ground: intersection of its propositions.

Equations

• cg.contextSet = List.foldr (fun (x1 x2 : Core.CommonGround.ContextSet W) => x1 ∩ x2) Set.univ cg.propositions

def Core.CommonGround.CG.add {W : Type u_1} (cg : CG W) (p : Set W) : CG W

Add a proposition to the common ground.

Equations

• cg.add p = { propositions := p :: cg.propositions }

def Core.CommonGround.CG.empty {W : Type u_1} : CG W

Empty common ground (no shared beliefs).

Equations

• Core.CommonGround.CG.empty = { propositions := [] }

@[implicit_reducible]

instance Core.CommonGround.CG.instInhabited {W : Type u_1} : Inhabited (CG W)

Equations

• Core.CommonGround.CG.instInhabited = { default := Core.CommonGround.CG.empty }

@[simp]

theorem Core.CommonGround.CG.empty_contextSet {W : Type u_1} : empty.contextSet = ContextSet.trivial

Empty CG gives the trivial (universal) context set.

@[simp]

theorem Core.CommonGround.CG.contextSet_add {W : Type u_1} (cg : CG W) (p : Set W) : (cg.add p).contextSet = p ∩ cg.contextSet

Adding a proposition intersects it into the context set.

theorem Core.CommonGround.CG.add_restricts {W : Type u_1} (cg : CG W) (p : Set W) : (cg.add p).contextSet ⊆ cg.contextSet

Adding a proposition restricts the context set.

HasContextSet: Uniform Access to Context Sets

@cite{ginzburg-2012} @cite{stalnaker-2002} @cite{krifka-2015}

Common ground appears in many guises across discourse theories: CG W (@cite{stalnaker-2002}), CommitmentSlate W (@cite{krifka-2015}), CommitmentSpace W (commitment trees), DistributionalCG W (probabilistic), DGB (dialogue gameboard FACTS), and InfoState (TTR gameboard). All of these induce a context set — the set of worlds compatible with accumulated information.

HasContextSet provides uniform extraction, enabling framework-agnostic discourse operations and bridge theorems connecting the representations.

class Core.CommonGround.HasContextSet (S : Type u_1) (W : outParam (Type u_2)) : Type (max u_1 u_2)

A discourse state from which a context set can be extracted.

Every discourse state representation (Stalnaker CG, Krifka commitment spaces, Ginzburg DGB, distributional CG, TTR gameboard) projects to a context set: the worlds compatible with the state's accumulated information.

• toContextSet : S → ContextSet W

@[reducible, inline]

abbrev Core.CommonGround.HasContextSet.entails {S : Type u_1} {W : Type u_2} [HasContextSet S W] (s : S) (p : Set W) : Prop

A discourse state entails a proposition if its context set does.

Equations

• Core.CommonGround.HasContextSet.entails s p = (Core.CommonGround.HasContextSet.toContextSet s ⊆ p)

@[reducible, inline]

abbrev Core.CommonGround.HasContextSet.updateCS {S : Type u_1} {W : Type u_2} [HasContextSet S W] (s : S) (p : Set W) : ContextSet W

Updating a discourse state's context set with a proposition.

Equations

• Core.CommonGround.HasContextSet.updateCS s p = Core.CommonGround.HasContextSet.toContextSet s ∩ p

@[implicit_reducible]

instance Core.CommonGround.instHasContextSetContextSet {W : Type u_1} : HasContextSet (ContextSet W) W

Equations

• Core.CommonGround.instHasContextSetContextSet = { toContextSet := id }

@[implicit_reducible]

instance Core.CommonGround.instHasContextSetCG {W : Type u_1} : HasContextSet (CG W) W

Equations

• Core.CommonGround.instHasContextSetCG = { toContextSet := Core.CommonGround.CG.contextSet }

theorem Core.CommonGround.hasContextSet_CG_eq {W : Type u_1} (cg : CG W) : HasContextSet.toContextSet cg = cg.contextSet

The CG instance agrees with CG.contextSet.

theorem Core.CommonGround.hasContextSet_add_restricts {W : Type u_1} (cg : CG W) (p : Set W) : HasContextSet.toContextSet (cg.add p) ⊆ HasContextSet.toContextSet cg

Adding to CG restricts the HasContextSet extraction.