Common Ground

Stalnakerian context management ([Sta73], [Sta74], [Sta78], [Sta02]): context sets and their update, common ground as proposition lists, and the interfaces connecting discourse-state representations to both.

Main definitions

• ContextSet W — worlds compatible with the context (a synonym for Set W), with ContextSet.update.
• CommonGround W — common ground as a list of propositions.
• CommonGround.HasContextSet — extraction of a context set from a discourse state.
• CommonGround.HasAssertion — discourse states whose assertion operation projects onto ContextSet.update ([Sta73] p. 455); a played history lands on the free model (toContextSet_play) and its projection is permutation-invariant (toContextSet_play_perm).

Proposal-based ([FB10]) and graded non-monotonic ([And21]) assertion models are deliberate non-instances; see FarkasBruce2010.assert_not_narrowing and Anderson2021.graded_update_keeps_false_world.

structure CommonGround (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.

@[reducible, inline]

abbrev CommonGround.ContextSet (W : Type u_2) : Type u_2

The set of worlds compatible with the common ground.

Equations

• CommonGround.ContextSet W = Set W

@[reducible, inline]

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

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

Equations

• CommonGround.ContextSet.trivial = Set.univ

@[reducible, inline]

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

Entailment: every world in the context satisfies the proposition.

Equations

• c.entails p = (c ⊆ p)

@[reducible, inline]

abbrev 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 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

theorem 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 CommonGround.ContextSet.update_comm {W : Type u_1} (c p q : Set W) : (update c p).update q = (update c q).update p

Successive updates commute: assertion order is irrelevant.

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

Updating twice with the same proposition is updating once.

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

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

Equations

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

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

Add a proposition to the common ground.

Equations

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

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

Empty common ground (no shared beliefs).

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

theorem CommonGround.empty_contextSet {W : Type u_1} : empty.contextSet = Set.univ

Empty common ground gives the trivial (universal) context set.

@[simp]

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

Adding a proposition intersects it into the context set.

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

Adding a proposition restricts the context set.

instance CommonGround.instLeftCommutativeSetInter {W : Type u_1} : LeftCommutative fun (x1 x2 : Set W) => x1 ∩ x2

theorem CommonGround.contextSet_perm {W : Type u_1} {l₁ l₂ : List (Set W)} (p : l₁.Perm l₂) : { propositions := l₁ }.contextSet = { propositions := l₂ }.contextSet

The context set is invariant under permutation of the propositions: the common ground is order-indifferent on its worlds-side projection.

Uniform context-set extraction

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

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

• toContextSet : S → ContextSet W

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

Canonical instances

@[implicit_reducible]

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

Equations

• CommonGround.instHasContextSetContextSet = { toContextSet := id }

@[implicit_reducible]

instance CommonGround.instHasContextSet {W : Type u_1} : HasContextSet (CommonGround W) W

Equations

• CommonGround.instHasContextSet = { toContextSet := CommonGround.contextSet }

@[simp]

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

The CommonGround instance agrees with CommonGround.contextSet.

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

Adding to the common ground restricts the HasContextSet extraction.

Stalnakerian assertion

class CommonGround.HasAssertion (S : Type u_2) (W : outParam (Type u_3)) extends CommonGround.HasContextSet S W : Type (max u_2 u_3)

A discourse state with a Stalnakerian assert: the projected context set updates by exactly the asserted proposition ([Sta78]).

• toContextSet : S → ContextSet W
• initial : S

  The initial dialogue state.

• assert : S → Set W → S

  Assert φ.

• toContextSet_initial : HasContextSet.toContextSet initial = ContextSet.trivial

  Nothing is presupposed initially: every world is live.

• toContextSet_assert (s : S) (φ : Set W) : HasContextSet.toContextSet (assert s φ) = (HasContextSet.toContextSet s).update φ

  Assertion narrows the projected context set by exactly φ.

theorem CommonGround.HasAssertion.assert_subset_prior {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) : HasContextSet.toContextSet (assert s φ) ⊆ HasContextSet.toContextSet s

Contraction: assertion only removes worlds.

theorem CommonGround.HasAssertion.assert_narrows {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) : HasContextSet.toContextSet (assert s φ) ⊆ φ

Narrowing: every surviving world satisfies the asserted proposition.

theorem CommonGround.HasAssertion.mem_assert {W : Type u_1} {S : Type u_2} [HasAssertion S W] {s : S} {φ : Set W} {w : W} : w ∈ HasContextSet.toContextSet (assert s φ) ↔ w ∈ HasContextSet.toContextSet s ∧ w ∈ φ

Membership in the post-assertion context set, characterized.

@[simp]

theorem CommonGround.HasAssertion.assert_initial {W : Type u_1} {S : Type u_2} [HasAssertion S W] (φ : Set W) : HasContextSet.toContextSet (assert initial φ) = φ

Asserting φ in the initial context yields exactly φ.

theorem CommonGround.HasAssertion.assert_comm {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ ψ : Set W) : HasContextSet.toContextSet (assert (assert s φ) ψ) = HasContextSet.toContextSet (assert (assert s ψ) φ)

Assertion order is irrelevant on the projected context set.

theorem CommonGround.HasAssertion.assert_idem {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) : HasContextSet.toContextSet (assert (assert s φ) φ) = HasContextSet.toContextSet (assert s φ)

Re-asserting φ does not change the projected context set.

theorem CommonGround.HasAssertion.assert_of_entails {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) (h : HasContextSet.toContextSet s ⊆ φ) : HasContextSet.toContextSet (assert s φ) = HasContextSet.toContextSet s

Asserting what the state already entails is a no-op on the projected context set ([Sta73] p. 454).

theorem CommonGround.HasAssertion.assert_twice {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ ψ : Set W) : HasContextSet.toContextSet (assert (assert s φ) ψ) = HasContextSet.toContextSet s ∩ φ ∩ ψ

Two consecutive assertions narrow the context set by the conjunction.

theorem CommonGround.HasAssertion.assert_twice_narrows {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ ψ : Set W) : HasContextSet.toContextSet (assert (assert s φ) ψ) ⊆ φ ∩ ψ

Two consecutive assertions land inside the conjunction.

@[implicit_reducible]

instance CommonGround.instHasAssertionContextSet {W : Type u_1} : HasAssertion (ContextSet W) W

The regular model: the context set itself, asserted-into by update. Every HasAssertion state projects onto this flow.

Equations

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

@[implicit_reducible]

instance CommonGround.instHasAssertion {W : Type u_1} : HasAssertion (CommonGround W) W

The free model: proposition lists, asserted-into by add; the projection is contextSet ([Sta73] p. 450's duality map). This IS the bare Stalnakerian framework ([Sta78]).

Equations

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

Assertion histories

def CommonGround.HasAssertion.play {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (h : List (Set W)) : S

Play a history of assertions from a state.

Equations

• CommonGround.HasAssertion.play s h = List.foldl CommonGround.HasAssertion.assert s h

@[simp]

theorem CommonGround.HasAssertion.play_nil {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) : play s [] = s

@[simp]

theorem CommonGround.HasAssertion.play_cons {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) (t : List (Set W)) : play s (φ :: t) = play (assert s φ) t

theorem CommonGround.HasAssertion.toContextSet_play {W : Type u_1} {S : Type u_2} [HasAssertion S W] (h : List (Set W)) : HasContextSet.toContextSet (play initial h) = { propositions := h }.contextSet

The context set of a played history is the common ground of that history: play from initial lands on the free model ([Sta73] p. 450).

theorem CommonGround.HasAssertion.toContextSet_play_perm {W : Type u_1} {S : Type u_2} [HasAssertion S W] {h₁ h₂ : List (Set W)} (p : h₁.Perm h₂) : HasContextSet.toContextSet (play initial h₁) = HasContextSet.toContextSet (play initial h₂)

Assertion order is irrelevant: permuted histories project to the same context set. States may differ — frameworks can record order — but the projection cannot.