Common Ground

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

Framework-agnostic context management following @cite{stalnaker-1974}: context sets, common ground as proposition lists, and decidable variants.

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

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

A context set is a predicate on worlds compatible with the common ground.

Equations

• Core.CommonGround.ContextSet W = (W → Prop)

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

The trivial context: all worlds possible.

Equations

• Core.CommonGround.ContextSet.trivial x✝ = True

def Core.CommonGround.ContextSet.absurd {W : Type u_1} : ContextSet W

The absurd context: no worlds possible.

Equations

• Core.CommonGround.ContextSet.absurd x✝ = False

def Core.CommonGround.ContextSet.mem {W : Type u_1} (c : ContextSet W) (w : W) : Prop

A world is in the context set.

Equations

• c.mem w = c w

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

The context set is non-empty.

Equations

• c.nonEmpty = ∃ (w : W), c w

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

A context entails a proposition iff it holds at all worlds in the context.

Equations

• (c ⊧ p) = ∀ (w : W), c w → p w = true

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

Equations

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

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

A proposition is compatible with a context if it holds at some world.

Equations

• c.compatible p = ∃ (w : W), c w ∧ p w = true

theorem Core.CommonGround.ContextSet.trivial_entails_iff {W : Type u_1} (p : BProp W) : (trivial ⊧ p) ↔ ∀ (w : W), p w = true

Trivial context entails only tautologies.

theorem Core.CommonGround.ContextSet.absurd_entails {W : Type u_1} (p : BProp W) : absurd ⊧ p

Absurd context entails everything.

def Core.CommonGround.ContextSet.update {W : Type u_1} (c : ContextSet W) (p : BProp W) : ContextSet W

Update a context with a proposition: keep only worlds where it holds.

Equations

• c.update p w = (c w ∧ p w = true)

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

Equations

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

theorem Core.CommonGround.ContextSet.update_restricts {W : Type u_1} (c : ContextSet W) (p : BProp W) (w : W) : c.update p w → c w

Update restricts the context.

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

Updated context entails the update proposition.

theorem Core.CommonGround.ContextSet.update_entailed {W : Type u_1} (c : ContextSet W) (p : BProp 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 : ContextSet W) (p q : BProp W) : (c.update p).update q = fun (w : W) => c w ∧ p w = true ∧ q w = true

Sequential updates are associative.

def Core.CommonGround.ContextSet.inter {W : Type u_1} (c₁ c₂ : ContextSet W) : ContextSet W

Intersection of contexts: worlds in both.

Equations

• c₁.inter c₂ w = (c₁ w ∧ c₂ w)

def Core.CommonGround.ContextSet.union {W : Type u_1} (c₁ c₂ : ContextSet W) : ContextSet W

Union of contexts: worlds in either.

Equations

• c₁.union c₂ w = (c₁ w ∨ c₂ w)

instance Core.CommonGround.ContextSet.instInter {W : Type u_1} : Inter (ContextSet W)

Equations

• Core.CommonGround.ContextSet.instInter = { inter := Core.CommonGround.ContextSet.inter }

instance Core.CommonGround.ContextSet.instUnion {W : Type u_1} : Union (ContextSet W)

Equations

• Core.CommonGround.ContextSet.instUnion = { union := Core.CommonGround.ContextSet.union }

def Core.CommonGround.ContextSet.fromProp {W : Type u_1} (p : BProp W) : ContextSet W

Create a context from a single proposition: worlds where it holds.

Equations

• Core.CommonGround.ContextSet.fromProp p w = (p w = true)

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

Updating trivial context with P gives context from P.

theorem Core.CommonGround.ContextSet.entails_mono {W : Type u_1} (c₁ c₂ : ContextSet W) (p : BProp W) (h_sub : ∀ (w : W), c₁ w → c₂ w) (h_ent : c₂ ⊧ p) : c₁ ⊧ p

Entailment is monotonic: smaller context entails more.

theorem Core.CommonGround.ContextSet.update_mono {W : Type u_1} (c₁ c₂ : ContextSet W) (p : BProp W) (h : ∀ (w : W), c₁ w → c₂ w) (w : W) : c₁.update p w → c₂.update p w

Update is monotonic in the context.

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

Common ground as a set of mutually believed propositions.

• propositions : List (BProp 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.

Equations

• cg.contextSet w = ((cg.propositions.all fun (p : BProp W) => p w) = true)

def Core.CommonGround.CG.add {W : Type u_1} (cg : CG W) (p : BProp 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 := [] }

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

Empty CG gives trivial context set.

theorem Core.CommonGround.CG.add_restricts {W : Type u_1} (cg : CG W) (p : BProp W) (w : W) : (cg.add p).contextSet w → cg.contextSet w

Adding a proposition restricts the context set.

@[reducible, inline]

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

Decidable context set: all worlds compatible with common knowledge. Mirrors ContextSet but uses Bool instead of Prop, enabling computation.

Equations

• Core.CommonGround.BContextSet W = (W → Bool)

def Core.CommonGround.BContextSet.toProp {W : Type u_1} (c : BContextSet W) : ContextSet W

Coerce a decidable context set to its classical (Prop-valued) counterpart.

Equations

• c.toProp w = (c w = true)

def Core.CommonGround.BContextSet.trivial {W : Type u_1} : BContextSet W

The trivial context: all worlds possible.

Equations

• Core.CommonGround.BContextSet.trivial x✝ = true

def Core.CommonGround.BContextSet.absurd {W : Type u_1} : BContextSet W

The absurd context: no worlds possible.

Equations

• Core.CommonGround.BContextSet.absurd x✝ = false

def Core.CommonGround.BContextSet.update {W : Type u_1} (c : BContextSet W) (p : W → Bool) : BContextSet W

Update a decidable context with a decidable proposition.

Equations

• c.update p w = (c w && p w)

def Core.CommonGround.BContextSet.filterWorlds {W : Type u_1} (c : BContextSet W) (worlds : List W) : List W

Filter a list of worlds to those compatible with the context.

Equations

• c.filterWorlds worlds = List.filter c worlds

def Core.CommonGround.BContextSet.entails {W : Type u_1} (c : BContextSet W) (worlds : List W) (p : W → Bool) : Bool

Decidable entailment: p holds at all context-compatible worlds.

Equations

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

theorem Core.CommonGround.BContextSet.trivial_toProp {W : Type u_1} : trivial.toProp = ContextSet.trivial

Trivial context set coerces to classical trivial.

theorem Core.CommonGround.BContextSet.update_toProp {W : Type u_1} (c : BContextSet W) (p : W → Bool) : (c.update p).toProp = c.toProp.update p

Update corresponds to classical update under coercion.

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

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

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

Equations

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

def Core.CommonGround.HasContextSet.updateCS {S : Type u_1} {W : Type u_2} [HasContextSet S W] (s : S) (p : BProp 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).update p

theorem Core.CommonGround.HasContextSet.entails_eq {S : Type u_1} {W : Type u_2} [HasContextSet S W] (s : S) (p : BProp W) : entails s p = (toContextSet s ⊧ p)

Entailment via HasContextSet reduces to ContextSet.entails.

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

Equations

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

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

Equations

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

instance Core.CommonGround.instHasContextSetBContextSet {W : Type u_1} : HasContextSet (BContextSet W) W

Equations

• Core.CommonGround.instHasContextSetBContextSet = { toContextSet := Core.CommonGround.BContextSet.toProp }

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 : BProp W) (w : W) : HasContextSet.toContextSet (cg.add p) w → HasContextSet.toContextSet cg w

Adding to CG restricts the HasContextSet extraction.