Sauerland's Epistemic Implicature Framework

[Sau04]

Categorical primitives for the primary/secondary implicature distinction of [Sau04]. Pure pragmatic theory — no RSA, no specific empirical paper. Consumed by Studies/ files (e.g., Studies/Kennedy2015.lean) that need a categorical implicature operator alongside or instead of an RSA derivation.

Sauerland's Framework

Sauerland distinguishes:

• Primary implicatures: ¬Kψ ("speaker doesn't know ψ")
• Secondary implicatures: K¬ψ ("speaker knows ¬ψ")

Secondary implicatures are derived from primary ones via an additional "competence" assumption: the speaker either knows ψ or knows ¬ψ.

Key insight: Secondary K¬ψ is blocked if it contradicts the assertion or the primary implicatures.

Main Results

1. Epistemic duality (duality): ¬K¬φ ↔ Pφ.
2. Primary-possibility correspondence: ¬Kψ → P¬ψ.
3. Blocking: Pψ → ¬K¬ψ — possibility blocks secondary implicatures.

The asymmetric-entailment primitive used to characterize Sauerland's primary-implicature alternatives lives in Semantics/Entailment/AsymStronger.lean as asymStrongerOn. A consumer wanting "the alternatives that trigger primary implicatures" writes alts.filter (asymStrongerOn e.possible · φ) directly — no wrapper needed.

The categorical-vs-graded relationship between Sauerland and RSA (RSA as the α → ∞ limit of Sauerland exclusion) is the subject of IBR/RSABridge.lean (rsa_speaker_to_ibr); this file provides only the categorical side.

structure Implicature.EpistemicBlocking.EpistemicState (W : Type u_1) : Type u_1

An epistemic state represents what the speaker knows. We model this as a finite set of worlds the speaker considers possible.

• possible : Finset W

  Worlds compatible with speaker's knowledge

• nonempty : self.possible.Nonempty

  Non-empty (speaker knows something is true)

def Implicature.EpistemicBlocking.knows {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) : Prop

K operator: speaker knows φ iff φ is true in all epistemically possible worlds.

Equations

• Implicature.EpistemicBlocking.knows e φ = ∀ w ∈ e.possible, φ w

@[implicit_reducible]

instance Implicature.EpistemicBlocking.instDecidableKnowsOfDecidablePred {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) [DecidablePred φ] : Decidable (knows e φ)

Equations

• Implicature.EpistemicBlocking.instDecidableKnowsOfDecidablePred e φ = Implicature.EpistemicBlocking.instDecidableKnowsOfDecidablePred._aux_1 e φ

def Implicature.EpistemicBlocking.possible {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) : Prop

P operator: speaker considers φ possible.

Equations

• Implicature.EpistemicBlocking.possible e φ = ∃ w ∈ e.possible, φ w

@[implicit_reducible]

instance Implicature.EpistemicBlocking.instDecidablePossibleOfDecidablePred {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) [DecidablePred φ] : Decidable (possible e φ)

Equations

• Implicature.EpistemicBlocking.instDecidablePossibleOfDecidablePred e φ = Implicature.EpistemicBlocking.instDecidablePossibleOfDecidablePred._aux_1 e φ

K/P as restricted modality

knows/possible are box/diamond over the (world-independent) epistemic accessibility accessFrom e, which is serial because e.possible is nonempty. The epistemic square of opposition is then Core.Logic.Modal.modalSquare (accessFrom e) with modalSquare_relations discharged by this IsSerial instance — no bespoke square construction.

def Implicature.EpistemicBlocking.accessFrom {W : Type u_1} (e : EpistemicState W) : Core.Logic.Modal.AccessRel W

Epistemic accessibility: from any world, the speaker's live possibilities.

Equations

• Implicature.EpistemicBlocking.accessFrom e x✝ w' = (w' ∈ e.possible)

instance Implicature.EpistemicBlocking.instIsSerialAccessFrom {W : Type u_1} (e : EpistemicState W) : Core.Logic.Modal.IsSerial (accessFrom e)

theorem Implicature.EpistemicBlocking.knows_eq_box {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) (w : W) : knows e φ = Core.Logic.Modal.box (accessFrom e) φ w

K is □ over epistemic accessibility.

theorem Implicature.EpistemicBlocking.possible_eq_diamond {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) (w : W) : possible e φ = Core.Logic.Modal.diamond (accessFrom e) φ w

P is ◇ over epistemic accessibility.

theorem Implicature.EpistemicBlocking.duality {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) : (¬knows e fun (w : W) => ¬φ w) ↔ possible e φ

Standard epistemic duality: ¬K¬φ ↔ Pφ. One of five sibling theorem dualitys — the box–diamond duality underlying the modal square of opposition (Core.Logic.Modal.modalSquare_relations).

def Implicature.EpistemicBlocking.hasSecondaryImplicature {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) : Prop

Secondary implicature: speaker knows the alternative is false.

Equations

• Implicature.EpistemicBlocking.hasSecondaryImplicature e ψ = Implicature.EpistemicBlocking.knows e fun (w : W) => ¬ψ w

theorem Implicature.EpistemicBlocking.secondary_blocked_if_possible {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) : possible e ψ → ¬knows e fun (w : W) => ¬ψ w

Key insight: if ψ is possible, then K¬ψ is blocked.

theorem Implicature.EpistemicBlocking.primary_possibility_correspondence {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) : ¬knows e ψ → possible e fun (w : W) => ¬ψ w

Primary-Possibility Correspondence: ¬Kψ (speaker doesn't know ψ) → P¬ψ (speaker considers ¬ψ possible).

theorem Implicature.EpistemicBlocking.blocking_correspondence {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) : possible e ψ → ¬hasSecondaryImplicature e ψ

Blocking Correspondence: Secondary K¬ψ is blocked when Pψ holds.