Neo-Gricean pragmatics: primary and secondary implicatures

import Linglib.Pragmatics.NeoGricean.Basic · namespace NeoGricean

The epistemic step of neo-Gricean scalar reasoning, after Sauerland's primary and secondary implicatures and Geurts's Standard Recipe. A speaker's epistemic state is a set of worlds s : Set W, and an epistemic proposition, what an utterance implicates about the speaker, is a set of states Set (Set W). Certainty Kφ is the principal down-set Set.Iic φ, so the primary implicature ¬Kψ is (Set.Iic ψ)ᶜ and the secondary implicature K¬ψ is Set.Iic ψᶜ, and competence Kψ ∨ K¬ψ is resolving the polar question Question.polar ψ. The empty state, a member of every Set.Iic, is the inconsistent speaker.

Asserting φ implicates Kφ by Quality and the primary implicature ¬Kψ of each alternative ψ that asymmetrically entails φ; for such a ψ, K¬ψ is a secondary implicature iff it is consistent with Kφ and all the primary implicatures.

Main definitions

NeoGricean.primaryImplicatures: the primary implicatures of the stronger alternatives, conjoined.
NeoGricean.IsSecondaryImplicature: the consistency condition on K¬ψ.

Main statements

NeoGricean.isSecondaryImplicature_iff: K¬ψ is a secondary implicature iff φ \ ψ entails no stronger alternative.
NeoGricean.compl_Iic_inter_polar: the Standard Recipe.

Implementation notes

The assertion enters the consistency check as Kφ, by Quality, as in Sauerland's own derivation for disjunction; against the bare proposition φ the secondary implicature K¬A of A or B would not be blocked.

Kφ and the primary implicatures are the hearer's inferences about the speaker's beliefs, not public commitments in the sense of Commitment.committed. The two meet at Quality, where Sincerity turns the speaker's commitment to the asserted φ into the belief Kφ.

References

Sauerland 2004, Scalar Implicatures in Complex Sentences formalized
Geurts 2010, Quantity Implicatures formalized
Soames 1982, How Presuppositions are Inherited: A Solution to the Projection Problem
Horn 1989, A Natural History of Negation
van Rooij & Schulz 2004, Exhaustive interpretation of complex sentences
Spector 2006, Aspects de la pragmatique des opérateurs logiques

Primary and secondary implicatures

The primary implicatures of φ against alts, conjoined: the states not certain of any alternative that asymmetrically entails φ (Sauerland 2004 (42)).

def primaryImplicatures L62–65

{W : Type u_1} (φ : Set W) (alts : Set (Set W)) :

Set (Set W)

primaryImplicatures φ alts = ⋂ ψ ∈ alts ∩ Set.Iio φ, (Set.Iic ψ)ᶜ

Used by mem_primaryImplicatures, IsSecondaryImplicature

Used in BaleEtAl2025, Geurts2010, Kennedy2015

L67–69

K¬ψ is a secondary implicature of asserting φ against alts iff ¬Kψ is a primary implicature and K¬ψ is consistent with Kφ and all the primary implicatures (Sauerland 2004 (43)).

def IsSecondaryImplicature L71–75

{W : Type u_1} (φ : Set W) (alts : Set (Set W)) (ψ : Set W) :

Prop

IsSecondaryImplicature φ alts ψ = (ψ ∈ alts ∧ ψ ⊂ φ ∧ ((Set.Iic φ ∩ primaryImplicatures φ alts ∩ Set.Iic ψᶜ) \ {∅}).Nonempty)

Built from

Used by isSecondaryImplicature_iff, isSecondaryImplicature_range_iff, isSecondaryImplicature_singleton

Used in Fox2007, Geurts2010, Kennedy2015, Rooth1992, Sauerland2004

The strengthened meaning φ \ ψ is the canonical witness: K¬ψ is a secondary implicature iff φ \ ψ entails no stronger alternative, so a blocked secondary implicature is always blocked by a single primary one.

theorem isSecondaryImplicature_iff L77–86

{W : Type u_1} {φ ψ : Set W} {alts : Set (Set W)} :

IsSecondaryImplicature φ alts ψ ↔ ψ ∈ alts ∧ ψ ⊂ φ ∧ ∀ χ ∈ alts, χ ⊂ φ → ¬φ \ ψ ⊆ χ

Built from

L88–90

L92–95

Competence and the Standard Recipe

The Standard Recipe: on consistent states, the weak implicature ¬Kψ together with competence about ψ, resolving the polar question whether ψ, is the strong implicature K¬ψ.

theorem compl_Iic_inter_polar L99–110

{W : Type u_1} (ψ : Set W) :

(Set.Iic ψ)ᶜ ∩ ↑(Question.polar ψ) = Set.Iic ψᶜ \ {∅}