Stalnaker's Common Ground Model of Assertion

@cite{stalnaker-1978} @cite{stalnaker-2002}Assertion as context set update: to assert p is to propose eliminating ¬p-worlds from the common ground. This is the simplest assertion theory and the baseline against which richer theories are compared.

Key Properties

• No commitment/belief separation: assertion IS adding to shared beliefs. There is no intermediate "commitment" stage.
• No retraction: the CG is monotonically updated (worlds are eliminated, never restored).
• No source marking: all CG updates are symmetric between participants.

Stalnaker's Norm

@cite{stalnaker-1978} identifies three norms on assertion:

1. The proposition expressed is true (sincerity)
2. The speaker believes the proposition (knowledge)
3. The proposition is not already in the common ground (informativity)

This module models the EFFECT of assertion (CG update), not the norms. The norms are relevant to Krifka's separation of commitment from belief.

@[reducible, inline]

abbrev Dialogue.Stalnaker.StalnakerState (W : Type u_1) : Type u_1

Stalnaker's discourse state IS the common ground. No separate commitment layer; assertion directly updates shared beliefs.

Equations

• Dialogue.Stalnaker.StalnakerState W = Core.CommonGround.CG W

def Dialogue.Stalnaker.initial {W : Type u_1} : StalnakerState W

Initial state: empty common ground (all worlds possible).

Equations

• Dialogue.Stalnaker.initial = Core.CommonGround.CG.empty

def Dialogue.Stalnaker.assert {W : Type u_1} (s : StalnakerState W) (p : Set W) : StalnakerState W

Assert p: add it to the common ground. This IS the full effect of assertion — no intermediate step.

Equations

• Dialogue.Stalnaker.assert s p = Core.CommonGround.CG.add s p

def Dialogue.Stalnaker.contextSet {W : Type u_1} (s : StalnakerState W) : Core.CommonGround.ContextSet W

Context set: directly from CG.

Equations

• Dialogue.Stalnaker.contextSet s = Core.CommonGround.CG.contextSet s

def Dialogue.Stalnaker.isStable {W : Type u_1} : StalnakerState W → Prop

Stalnaker states are always stable: there is no "table" or pending issue mechanism. Assertion is immediate.

Equations

• Dialogue.Stalnaker.isStable x✝ = True

@[implicit_reducible]

instance Dialogue.Stalnaker.instDecidableIsStable {W : Type u_1} (s : StalnakerState W) : Decidable (isStable s)

Equations

• Dialogue.Stalnaker.instDecidableIsStable s = isTrue ⋯

theorem Dialogue.Stalnaker.initial_trivial {W : Type u_1} : contextSet initial = Core.CommonGround.ContextSet.trivial

Empty CG gives trivial context set.

theorem Dialogue.Stalnaker.assert_restricts {W : Type u_1} (s : StalnakerState W) (p : Set W) : contextSet (assert s p) ⊆ contextSet s

Assertion restricts the context set.

theorem Dialogue.Stalnaker.always_stable {W : Type u_1} (s : StalnakerState W) : isStable s

Stalnaker states are always stable.

theorem Dialogue.Stalnaker.hasContextSet_eq_contextSet {W : Type u_1} (s : StalnakerState W) : Core.CommonGround.HasContextSet.toContextSet s = contextSet s

Theorem (not instance — the CG W instance from Core.CommonGround already resolves through the StalnakerState W := CG W abbrev): the HasContextSet projection on a Stalnaker state agrees with the local Stalnaker.contextSet def. Documents the bridge for grep.