Neo-Gricean pragmatics: secondary implicatures and the Standard Recipe

This file defines [Sau04]'s derivation of secondary implicatures and the Standard Recipe of [Geu10]. A speaker's epistemic state is a set of worlds s : Set W (the same object as the ContextSet of Discourse/CommonGround.lean), and an epistemic proposition — what an utterance implicates about the speaker — is a set of states Set (Set W). Knowledge Kφ is the principal down-set Set.Iic φ (the states s ⊆ φ), so the primary implicature ¬Kψ is (Iic ψ)ᶜ, the secondary implicature K¬ψ is Iic ψᶜ, competence Kψ ∨ K¬ψ is Iic ψ ∪ Iic ψᶜ, and the empty state, a member of every Iic, is the inconsistent speaker. Asserting φ against alternatives alts commits the speaker to Kφ and the primary implicatures; K¬ψ is a secondary implicature iff it is consistent with that commitment.

Main definitions

• primaryImplicature, secondaryImplicature, competent: the epistemic propositions ¬Kψ, K¬ψ, Kψ ∨ K¬ψ.
• commitment: Kφ together with the primary implicatures of the alternatives.
• Consistent: an epistemic proposition holds of some nonempty state.
• IsSecondaryImplicature: [Sau04]'s condition for K¬ψ.

Main results

• isSecondaryImplicature_iff: K¬ψ is a secondary implicature iff the strengthened meaning φ \ ψ is consistent and entails no alternative — φ \ ψ itself is the canonical witness, so a blocked secondary implicature is always blocked by a single primary; the disjunction case (K¬(A∧B) arises, K¬A is blocked) is Studies/Sauerland2004.lean.
• isSecondaryImplicature_of_ssubset: a lone asymmetrically stronger alternative always yields its secondary implicature.
• primaryImplicature_inter_competent: the Standard Recipe as an identity — on consistent states, the weak implicature plus competence is the strong implicature.

References

• [Sau04] — primary vs secondary implicatures and the consistency condition
• [Geu10] — the Standard Recipe; textbook presentation
• [soames-1982], [Hor89] — the epistemic modalization ¬Kψ
• [vanrooij-schulz-2004], [Spe06] — the competence step Kψ ∨ K¬ψ

Epistemic propositions

def NeoGricean.primaryImplicature {W : Type u_1} (ψ : Set W) : Set (Set W)

The primary implicature ¬Kψ: the states that do not know ψ.

Equations

• NeoGricean.primaryImplicature ψ = (Set.Iic ψ)ᶜ

def NeoGricean.secondaryImplicature {W : Type u_1} (ψ : Set W) : Set (Set W)

The secondary implicature K¬ψ: the states that know ¬ψ.

Equations

• NeoGricean.secondaryImplicature ψ = Set.Iic ψᶜ

def NeoGricean.competent {W : Type u_1} (ψ : Set W) : Set (Set W)

Competence about ψ, Kψ ∨ K¬ψ: the states that know whether ψ.

Equations

• NeoGricean.competent ψ = Set.Iic ψ ∪ Set.Iic ψᶜ

@[simp]

theorem NeoGricean.mem_primaryImplicature {W : Type u_1} {s ψ : Set W} : s ∈ primaryImplicature ψ ↔ ¬s ⊆ ψ

@[simp]

theorem NeoGricean.mem_secondaryImplicature {W : Type u_1} {s ψ : Set W} : s ∈ secondaryImplicature ψ ↔ s ⊆ ψᶜ

@[simp]

theorem NeoGricean.mem_competent {W : Type u_1} {s ψ : Set W} : s ∈ competent ψ ↔ s ⊆ ψ ∨ s ⊆ ψᶜ

def NeoGricean.Consistent {W : Type u_1} (E : Set (Set W)) : Prop

An epistemic proposition is consistent iff some nonempty state satisfies it.

Equations

• NeoGricean.Consistent E = ∃ s ∈ E, s.Nonempty

Primary and secondary implicatures

Asserting φ against scalar alternatives alts commits the speaker to Kφ plus the primary implicature ¬Kψ for each alternative ([Sau04] (42), verified p. 383); K¬ψ is a secondary implicature exactly when it is consistent with that commitment ([Sau04] (43)).

def NeoGricean.commitment {W : Type u_1} (φ : Set W) (alts : Set (Set W)) : Set (Set W)

The speaker's commitment after asserting φ against alts: Kφ and the primary implicature of each alternative. Per [Sau04] the alternatives are the asymmetrically stronger ones (ψ ⊂ φ); the definition does not enforce the filter.

Equations

• NeoGricean.commitment φ alts = Set.Iic φ ∩ ⋂ χ ∈ alts, NeoGricean.primaryImplicature χ

@[simp]

theorem NeoGricean.mem_commitment {W : Type u_1} {s φ : Set W} {alts : Set (Set W)} : s ∈ commitment φ alts ↔ s ⊆ φ ∧ ∀ χ ∈ alts, ¬s ⊆ χ

def NeoGricean.IsSecondaryImplicature {W : Type u_1} (φ : Set W) (alts : Set (Set W)) (ψ : Set W) : Prop

K¬ψ is a secondary implicature of asserting φ against alts iff it is consistent with the commitment.

Equations

• NeoGricean.IsSecondaryImplicature φ alts ψ = NeoGricean.Consistent (NeoGricean.commitment φ alts ∩ NeoGricean.secondaryImplicature ψ)

theorem NeoGricean.isSecondaryImplicature_iff {W : Type u_1} {φ ψ : Set W} {alts : Set (Set W)} : IsSecondaryImplicature φ alts ψ ↔ (φ \ ψ).Nonempty ∧ ∀ χ ∈ alts, ¬φ \ ψ ⊆ χ

The strengthened meaning φ \ ψ is the canonical witness: K¬ψ is a secondary implicature iff φ \ ψ is consistent and entails no alternative. A blocked secondary implicature is thus always blocked by a single primary.

theorem NeoGricean.isSecondaryImplicature_singleton {W : Type u_1} {φ ψ χ : Set W} : IsSecondaryImplicature φ {χ} ψ ↔ (φ \ ψ).Nonempty ∧ ¬φ \ ψ ⊆ χ

For a lone alternative χ, K¬ψ is a secondary implicature iff φ \ ψ is consistent and does not entail χ.

theorem NeoGricean.isSecondaryImplicature_singleton_self {W : Type u_1} {φ ψ : Set W} : IsSecondaryImplicature φ {ψ} ψ ↔ (φ \ ψ).Nonempty

Against its own alternative alone, K¬ψ is a secondary implicature iff the strengthened meaning φ \ ψ is consistent.

theorem NeoGricean.isSecondaryImplicature_of_ssubset {W : Type u_1} {φ ψ : Set W} (h : ψ ⊂ φ) : IsSecondaryImplicature φ {ψ} ψ

A lone asymmetrically stronger alternative always yields its secondary implicature: the some ⇝ not all case.

Competence and the Standard Recipe

Competence about ψ is [Sau04]'s Kψ ∨ K¬ψ — the speaker knows whether ψ, which is support of the polar question Question.polar ψ by Question.mem_polar.

theorem NeoGricean.not_subset_compl_of_subset {W : Type u_1} {s ψ : Set W} (hs : s.Nonempty) (h : s ⊆ ψ) : ¬s ⊆ ψᶜ

A consistent speaker cannot both know ψ and know ¬ψ.

theorem NeoGricean.subset_compl_iff_not_subset {W : Type u_1} {s ψ : Set W} (hs : s.Nonempty) (hc : s ⊆ ψ ∨ s ⊆ ψᶜ) : s ⊆ ψᶜ ↔ ¬s ⊆ ψ

The Standard Recipe, pointwise: for a consistent speaker competent about ψ, the strong implicature K¬ψ is exactly the weak implicature ¬Kψ.

theorem NeoGricean.primaryImplicature_inter_competent {W : Type u_1} (ψ : Set W) : primaryImplicature ψ ∩ competent ψ = secondaryImplicature ψ \ {∅}

The Standard Recipe: on consistent states, the weak implicature plus competence is the strong implicature.