Sauerland's Epistemic Implicature Framework

@cite{sauerland-2004}

Categorical primitives for the primary/secondary implicature distinction of @cite{sauerland-2004}. Pure pragmatic theory — no RSA, no specific empirical paper. Consumed by Phenomena/.../Studies/ files (e.g., Numerals/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 Theories/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 φ

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 (see Theories/Semantics/Modality/Kratzer/Operators.lean::duality for the unification opportunity via Core.Logic.Opposition.Square.fromBox).

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.