Common ground

The common ground of a conversation is the filter of propositions the interlocutors mutually accept ([Sta78], [Sta02]; independently [Kar74a]): acceptance is closed under entailment and finite conjunction and contains the trivial proposition, which are exactly the filter axioms (in modal-logic terms: "every augmented model is a filter", [Che80] §7.3; in belief-revision terms, a deductively closed belief set, [Gar88]). Stalnaker's context set — the worlds compatible with everything accepted — is the kernel Filter.ker, [Che80]'s smallest proposition ⋂ Nα, and a bare context set cs : Set W is the principal common ground 𝓟 cs, with acceptance p ∈ 𝓟 cs ↔ cs ⊆ p (Filter.mem_principal); Filter.giPrincipalKer is the two-sidedness of this duality, and the principal (augmented) case is exactly the Kripke case ([Che80] Theorem 7.9). Assertion of φ is · ⊓ 𝓟 φ ([Sta78]): intersective update of the context set is Filter.ker_inf, and commutativity and idempotence of assertion are lattice laws. A consistent context is a Filter.NeBot; the absurd context is ⊥.

HasCommonGround and HasAssertion connect richer discourse-state representations (commitment slates, gameboards, probabilistic states) to this projection.

Implementation notes

The filter axioms are the body-of-information view of the common ground ([Geu24]'s survey) and deliberately carry no epistemology: whether what grounds them is iterated common belief ([Sta02]), common acceptance as a primitive ([Sta14a]), or [Led14]'s non-iterated minimal theory is stated separately, as Filter.GroundedIn in Logic/Modal/Epistemic.lean — the epistemology, and in particular closure of acceptance under conjunction (the filter's inter_sets, [Led14] §2.C's contested axiom), is the disputed idealization in that debate, not a commitment every consumer inherits. Proposal-based ([FB10]) and graded non-monotonic ([And21]) assertion models are deliberate non-instances of HasAssertion; see FarkasBruce2010.assert_not_narrowing and Anderson2021.graded_update_keeps_false_world.

Main definitions

• HasCommonGround: discourse states projecting to a common ground Filter W, with the derived contextSet.
• HasAssertion: discourse states with a Stalnakerian assert, projecting to · ⊓ 𝓟 φ, and assertion histories HasAssertion.play.

Main results

• HasAssertion.contextSet_assert: assertion intersects the context set by exactly the asserted proposition ([Sta73] p. 455).
• HasAssertion.commonGround_play: a played history lands on the principal filter of the history's intersection ([Sta73] p. 450's duality map), so the projection is permutation-invariant (commonGround_play_perm) — states may record assertion order, but the common ground cannot.

Discourse states and their common ground

class HasCommonGround (S : Type u_2) (W : outParam (Type u_3)) : Type (max u_2 u_3)

A discourse state projecting to a common ground: the filter of propositions the interlocutors mutually accept at that state.

• commonGround : S → Filter W

  The common ground of the state.

def HasCommonGround.contextSet {W : Type u_1} {S : Type u_2} [HasCommonGround S W] (s : S) : Set W

The context set of a discourse state: the worlds compatible with everything accepted.

Equations

• HasCommonGround.contextSet s = (commonGround s).ker

@[instance_reducible]

instance instHasCommonGroundFilter {W : Type u_1} : HasCommonGround (Filter W) W

A filter is its own common ground.

Equations

• instHasCommonGroundFilter = { commonGround := id }

@[simp]

theorem HasCommonGround.commonGround_filter {W : Type u_1} (f : Filter W) : commonGround f = f

@[instance_reducible]

instance instHasCommonGroundSet {W : Type u_1} : HasCommonGround (Set W) W

A bare context set is the principal common ground.

Equations

• instHasCommonGroundSet = { commonGround := Filter.principal }

@[simp]

theorem HasCommonGround.commonGround_set {W : Type u_1} (s : Set W) : commonGround s = Filter.principal s

Stalnakerian assertion

class HasAssertion (S : Type u_2) (W : outParam (Type u_3)) extends HasCommonGround S W : Type (max u_2 u_3)

A discourse state with a Stalnakerian assert: the projected common ground grows by exactly the asserted proposition ([Sta78]).

• commonGround : S → Filter W
• initial : S

  The initial dialogue state.

• assert : S → Set W → S

  Assert φ.

• commonGround_initial : commonGround initial = ⊤

  Nothing is presupposed initially.

• commonGround_assert (s : S) (φ : Set W) : commonGround (assert s φ) = commonGround s ⊓ Filter.principal φ

  Assertion adds exactly φ to the common ground.

@[instance_reducible]

instance instHasAssertionFilter {W : Type u_1} : HasAssertion (Filter W) W

The regular model: a common ground asserted-into by · ⊓ 𝓟 φ. Every HasAssertion state projects onto this flow.

Equations

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

theorem HasAssertion.mem_commonGround_assert {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) : φ ∈ commonGround (assert s φ)

The asserted proposition is accepted.

theorem HasAssertion.commonGround_assert_le {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) : commonGround (assert s φ) ≤ commonGround s

Assertion strengthens the common ground.

@[simp]

theorem HasAssertion.contextSet_assert {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) : HasCommonGround.contextSet (assert s φ) = HasCommonGround.contextSet s ∩ φ

Assertion intersects the context set by exactly the asserted proposition ([Sta73] p. 455).

@[simp]

theorem HasAssertion.commonGround_assert_initial {W : Type u_1} {S : Type u_2} [HasAssertion S W] (φ : Set W) : commonGround (assert initial φ) = Filter.principal φ

Asserting in the initial state yields the principal common ground.

theorem HasAssertion.commonGround_assert_assert {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ ψ : Set W) : commonGround (assert (assert s φ) ψ) = commonGround s ⊓ Filter.principal (φ ∩ ψ)

Two consecutive assertions add the conjunction.

theorem HasAssertion.commonGround_assert_comm {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ ψ : Set W) : commonGround (assert (assert s φ) ψ) = commonGround (assert (assert s ψ) φ)

Assertion order is irrelevant on the common ground.

theorem HasAssertion.commonGround_assert_idem {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) : commonGround (assert (assert s φ) φ) = commonGround (assert s φ)

Re-assertion is a no-op on the common ground.

theorem HasAssertion.commonGround_assert_of_mem {W : Type u_1} {S : Type u_2} [HasAssertion S W] (s : S) (φ : Set W) (h : φ ∈ commonGround s) : commonGround (assert s φ) = commonGround s

Asserting what is already accepted is a no-op on the common ground ([Sta73] p. 454).

Assertion histories

def 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

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

@[simp]

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

@[simp]

theorem 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 HasAssertion.commonGround_play {W : Type u_1} {S : Type u_2} [HasAssertion S W] (h : List (Set W)) (s : S) : commonGround (play s h) = commonGround s ⊓ Filter.principal {w : W | ∀ p ∈ h, w ∈ p}

A played history adds the principal filter of the history's intersection.

theorem HasAssertion.commonGround_play_initial {W : Type u_1} {S : Type u_2} [HasAssertion S W] (h : List (Set W)) : commonGround (play initial h) = Filter.principal {w : W | ∀ p ∈ h, w ∈ p}

From the initial state, a played history is its common ground: the free model of Stalnakerian assertion ([Sta73] p. 450).

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

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