Assertable: a typeclass for commitment-tracking dialogue states

@cite{stalnaker-1978} @cite{krifka-2015} @cite{farkas-bruce-2010} @cite{anderson-2021}

A unifying typeclass over discourse-state types that admit a one-step "speaker asserts φ" operation whose effect on the projected context set is to narrow it by φ (Stalnaker's classical assertion semantics, lifted to be framework-generic).

The typeclass extends HasContextSet S W (re-using the existing projection interface) and adds:

• initial : S — the empty / starting dialogue state.
• speakerAssert : S → (W → Prop) → S — record that the speaker has publicly committed to φ.
• speakerAssert_monotone — the typeclass law: every world surviving the asserted state was already in the prior context set AND satisfies the asserted proposition. This is the monotonicity-and-narrowing law in one shot, strong enough to prove compositional theorems (consecutive assertions, idempotence, etc.).

What the typeclass is for

The point of Assertable is to make the shape of "Stalnakerian narrowing" framework-generic. Every framework that admits an instance satisfies the cross-framework theorems (speakerAssert_initial_subset, speakerAssert_twice_narrows, speakerAssert_iter_subset_prior) for free, lifted out of the typeclass law. Any future framework-generic theorem about assertion composition can be quantified over [Assertable S W] rather than restated per framework.

The structurally important non-instance

Dialogue.FarkasBruce.DiscourseState does not instantiate Assertable. The reason is informationally important, not a gap to fill: F&B's assertDeclarative writes to dcS and pushes an issue onto the table, but does not write to cg. Their toContextSet projects only cg. So the candidate "narrowing" law toContextSet (assertDeclarative ds φ) ⊆ φ fails — the projection is unchanged by the assertion.

This is not a bug in F&B; it's the F&B speaker/listener split made visible. F&B requires a two-step assertDeclarative ∘ acceptTop to produce a Stalnakerian narrowing, and that two-step composite has a different type signature than Assertable.speakerAssert. The right place to host F&B's narrowing operator is a sibling typeclass (e.g., Proposable separating propose from settle); this is left for a future cross-framework refactor.

Sibling notion: stability

Some frameworks have a "stability" predicate (no pending issues, no open continuations). Stalnaker is always stable; Krifka is stable iff hasNoOpenContinuations; F&B is stable iff table.isEmpty. The predicate is genuine but is not a typeclass-required field — Stalnaker provides only the trivially-True version, which is uninformative as a hook for cross-framework theorems. We expose stability per-framework via the existing KrifkaState.hasNoOpenContinuations and Stalnaker.isStable.

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

A dialogue-state type that admits a Stalnakerian one-step assertion.

Instances satisfy two laws — speakerAssert_subset_prior (monotonicity: assertion never adds worlds) and speakerAssert_narrows (narrowing: every surviving world satisfies the asserted proposition). Their conjunction (speakerAssert_monotone, derived) is what compositional theorems consume.

Frameworks whose "assertion" semantics differ structurally from Stalnaker's one-step narrowing — notably Farkas-Bruce 2010, where assertDeclarative proposes via dcS and table without touching cg — do not instantiate this typeclass. See the module docstring.

• toContextSet : S → ContextSet W
• initial : S

  The empty/initial dialogue state.

• speakerAssert : S → (W → Prop) → S

  Speaker commits to φ.

• speakerAssert_subset_prior (s : S) (φ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (speakerAssert s φ) ⊆ Core.CommonGround.HasContextSet.toContextSet s

  Monotonicity: assertion never adds worlds — the surviving set is contained in the prior context set.

• speakerAssert_narrows (s : S) (φ : W → Prop) (w : W) : Core.CommonGround.HasContextSet.toContextSet (speakerAssert s φ) w → φ w

  Narrowing: every world surviving the asserted state satisfies the asserted proposition. The Stalnakerian half of the assertion law.

theorem Dialogue.Assertable.speakerAssert_monotone {S : Type u_1} {W : Type u_2} [Assertable S W] (s : S) (φ : W → Prop) (w : W) (h : Core.CommonGround.HasContextSet.toContextSet (speakerAssert s φ) w) : Core.CommonGround.HasContextSet.toContextSet s w ∧ φ w

The conjoined narrowing-and-monotonicity law: every world surviving the asserted state was already in the prior context set AND satisfies the asserted proposition.

Derived from the two typeclass fields. Useful when you need both halves of the post-assertion guarantee in a single hypothesis (e.g., for compositional theorems iterating the law across consecutive assertions).

theorem Dialogue.Assertable.speakerAssert_initial_subset {S : Type u_1} {W : Type u_2} [Assertable S W] (φ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (speakerAssert initial φ) ⊆ {w : W | φ w}

The headline framework-generic theorem. Asserting φ from initial yields a context set entirely contained in φ.

theorem Dialogue.Assertable.speakerAssert_twice_narrows {S : Type u_1} {W : Type u_2} [Assertable S W] (s : S) (φ ψ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (speakerAssert (speakerAssert s φ) ψ) ⊆ {w : W | φ w ∧ ψ w}

Two consecutive assertions narrow the context set by the conjunction of the two propositions.

Lifted from the two laws: the outer narrowing gives ψ w; the monotonicity step from outer→inner pulls w ∈ contextSet (speakerAssert s φ), and the inner narrowing then gives φ w.

theorem Dialogue.Assertable.speakerAssert_twice_subset_prior {S : Type u_1} {W : Type u_2} [Assertable S W] (s : S) (φ ψ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (speakerAssert (speakerAssert s φ) ψ) ⊆ Core.CommonGround.HasContextSet.toContextSet s

Iterated monotonicity: the chain of assertions stays within the initial context set.

@[implicit_reducible]

instance Dialogue.instStalnaker {W : Type u_1} : Assertable (Stalnaker.StalnakerState W) W

@cite{stalnaker-1978}'s common-ground-as-context-set instance.

speakerAssert s φ is s.add φ (set intersection). The two laws follow from Core.CommonGround.CG.contextSet reducing the asserted CG to φ ∩ s.contextSet: monotonicity is the right conjunct of set-intersection membership, narrowing is the left.

Equations

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

@[implicit_reducible]

instance Dialogue.instKrifka {W : Type u_1} : Assertable (Krifka.KrifkaState W) W

@cite{krifka-2015}'s commitment-space instance, binary case.

speakerAssert s φ is s.assert φ with default committer .speaker and default force .doxastic. KrifkaState.assert prepends IndexedWeightedCommitment.commit .speaker .doxastic φ to the space root; KrifkaState.contextSet requires every root commitment to project to True. At G = Prop, the new commit projects to φ itself (narrowing); the existing root commits project to the prior context set (monotonicity).

Equations

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