Gricean diagnostics for pragmatic inference

[Gri75] [Sad78] [Hir85] [Hor91] [Geu10]

The classical cancellability and reinforceability tests, stated over a bare pair of an assertion φ : W → Prop and an inferred content W → Prop. Any strengthening mechanism — a Neo-Gricean recipe (Pragmatics/NeoGricean/), grammatical exhaustification (Semantics/Exhaustification/), a thresholded RSA posterior (Pragmatics/RSA/) — can submit its output to these predicates; no shared record type is required, so the diagnostics stay neutral between frameworks that disagree about what an implicature is.

[Gri75] introduced calculability and non-detachability as defining features; [Sad78] added cancellability and schematized the test battery; [Hor91] extends the reinforceability discussion via the redundancy diagnostic. Calculability and detachability are properties of a derivation, not of an (assertion, content) pair, so they are stated where the derivations live, not here.

Magri-style obligatory SI ([Mag09]) is not an IsCancellable failure, even common-ground-relativized: for "#Some Italians come from a warm country" with CK restricting to all-warm worlds, "in fact all" is a consistent continuation contradicting the EXH'd implicature, so IsCancellable holds. The contentful Magri claim — no CK-realizer of the strengthened meaning — is magri_blindOdd_no_ck_realizer in Studies/Magri2009.lean.

def Implicature.IsCancellable {W : Type u_1} (φ content : W → Prop) : Prop

An inferred content derived from an assertion φ is cancellable iff some continuation is consistent with φ and contradicts the content: "Some students passed — in fact, all of them did" is felicitous iff "all passed" is consistent with the assertion and contradicts not all. [Sad78]'s diagnostic.

Equations

• Implicature.IsCancellable φ content = ∃ (cancel : W → Prop), (∃ (w : W), φ w ∧ cancel w) ∧ ∀ (w : W), cancel w → ¬content w

theorem Implicature.IsCancellable.of_assertion_compatible_with_negation {W : Type u_1} {φ content : W → Prop} (h : ∃ (w : W), φ w ∧ ¬content w) : IsCancellable φ content

Cancellation by the negation of the content itself: if some assertion-world falsifies the content, ¬content witnesses cancellability. The most common cancellation form.

theorem Implicature.IsCancellable.false_of_assertion_implies_content {W : Type u_1} {φ content : W → Prop} (h : ∀ (w : W), φ w → content w) : ¬IsCancellable φ content

The load-bearing non-cancellability principle: if every assertion-world satisfies the content, no continuation cancels it. Fires for pex outputs from holds → presup.

def Implicature.IsReinforceable {W : Type u_1} (φ content : W → Prop) : Prop

An inferred content is reinforceable over assertion φ iff it is not already entailed by the assertion: "Some students passed, but not all" is non-redundant iff some passed does not entail not all. ([Sad78]; [Hor91]'s redundancy diagnostic.)

Equations

• Implicature.IsReinforceable φ content = ∃ (w : W), φ w ∧ ¬content w

theorem Implicature.IsReinforceable.toCancellable {W : Type u_1} {φ content : W → Prop} (h : IsReinforceable φ content) : IsCancellable φ content

Reinforceable ⇒ cancellable: the same witness works, so reinforceability is the stricter diagnostic. The converse may fail ([Hir85]).