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 Theories.Pragmatics.Assertion.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

• Theories.Pragmatics.Assertion.Stalnaker.StalnakerState W = Core.CommonGround.CG W

def Theories.Pragmatics.Assertion.Stalnaker.initial {W : Type u_1} : StalnakerState W

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

Equations

• Theories.Pragmatics.Assertion.Stalnaker.initial = Core.CommonGround.CG.empty

def Theories.Pragmatics.Assertion.Stalnaker.assert {W : Type u_1} (s : StalnakerState W) (p : BProp W) : StalnakerState W

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

Equations

• Theories.Pragmatics.Assertion.Stalnaker.assert s p = Core.CommonGround.CG.add s p

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

Context set: directly from CG.

Equations

• Theories.Pragmatics.Assertion.Stalnaker.contextSet s = Core.CommonGround.CG.contextSet s

def Theories.Pragmatics.Assertion.Stalnaker.isStable {W : Type u_1} : StalnakerState W → Bool

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

Equations

• Theories.Pragmatics.Assertion.Stalnaker.isStable x✝ = true

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

Empty CG gives trivial context set.

theorem Theories.Pragmatics.Assertion.Stalnaker.assert_restricts {W : Type u_1} (s : StalnakerState W) (p : BProp W) (w : W) : contextSet (assert s p) w → contextSet s w

Assertion restricts the context set.

theorem Theories.Pragmatics.Assertion.Stalnaker.always_stable {W : Type u_1} (s : StalnakerState W) : isStable s = true

Stalnaker states are always stable.