Gricean Diagnostics over Implicature

@cite{grice-1975} @cite{sadock-1978} @cite{hirschberg-1985} @cite{horn-1991} @cite{geurts-2010} @cite{potts-2005} @cite{delpinal-bassi-sauerland-2024}

Formalizes the standard Gricean diagnostic tests for distinguishing implicatures from entailments and presuppositions, stated uniformly over the Implicature W Prop type from Defs.lean. The headline application is the BPS bridge in Theories/Semantics/Exhaustification/Presuppositional.lean, which delivers two non-cancellability theorems for pex outputs: bps_not_cancellable (structural — assertion = p.holds makes content survive trivially) and bps_neg_not_cancellable (substantive — assertion = p.neg.holds makes content survive because PrProp.neg projects; the family-of-sentences test in @cite{bassi-delpinal-sauerland-2021}'s sense). The substrate's projecting PrProp.neg is what makes the projection theorem work; swapping in non-projecting PrProp.negExt would falsify it.

The four classical tests

Test	Sketch
Cancellability	A felicitous continuation contradicting the inference exists.
Reinforceability	The inference can be added explicitly without redundancy.
Calculability	The inference is derived (not lexically encoded).
Non-detachability	Paraphrases preserve the inference (form-independence).

@cite{grice-1975} introduced calculability and non-detachability as defining features. @cite{sadock-1978} added cancellability and schematized the four-test apparatus. @cite{hirschberg-1985} surveys the diagnostics and their interaction; @cite{horn-1991} extends the reinforceability discussion via the redundancy diagnostic.

Joint vs. mechanism-internal tests

Cancellable and Reinforceable are joint properties of an implicature together with the assertion that gave rise to it — they ask about the relationship between asserted content and inferred content. These take two arguments.

Calculable and NonDetachable are properties of how the inference was derived, and lift cleanly from the mechanism (and, for non-detachability, the kind) field of Implicature. These take one argument.

Strength specialization

The Gricean diagnostics defined here are specialized to the discrete / categorical ontology — they operate on Implicature W Prop. The S = Prop content lets us write ¬ i.content w and similar. For graded mechanisms (RSA-style Implicature W ℝ), the diagnostics do not apply directly: cancellability and reinforceability would require a thresholding interpretation, which is itself an empirical commitment. Future work could add a separate GradedDiagnostics.lean if and when graded-content study files demand it.

The kind- and mechanism-level helpers (isCalculable, isNonDetachable) and the failure-mode theorems are polymorphic in S because they only inspect the kind and mechanism fields.

Failure modes are diagnostic

A conventional implicature (Potts 2005) is by definition lexically encoded, so it fails calculability — and that failure is itself a theorem (lexical_not_calculable). A manner implicature is by definition form-relative, so it fails non-detachability (manner_is_detachable). These are not bugs; they're how the diagnostics divide the implicature space.

What this file delivers vs. what it does NOT

Delivered structurally (bps_not_cancellable): when assertion = p.holds, the inferred presup is trivially entailed by the assertion. The substantive content lives in the wrapper's choice to use holds, not in pex itself.

Delivered substantively (bps_neg_not_cancellable): when assertion = p.neg.holds (i.e., the speaker negates the pex output), the inferred presup still survives — because PrProp.neg is constructed to project the presupposition ((neg p).presup := p.presup). This is the family-of- sentences projection test in formal form. Falsifies for PrProp.negExt.

Not delivered as cancellability failure: Magri-style obligatory SI (@cite{magri-2009}) is not non-cancellable in the Sadock sense, even CK-relativized. For "#Some Italians come from a warm country" with CK restricting to all-warm worlds, "in fact all" is a consistent continuation at the CK world that contradicts the EXH'd implicature — so IsCancellable holds even with the CK restriction baked into the assertion. The contentful Magri claim is a different diagnostic — no CK-realizer of the strengthened meaning — formalized as magri_blindOdd_no_ck_realizer in Magri2009.lean. Magri obligatoriness ≠ IsCancellable failure; the docstring previously conflated these.

def ImplicatureMechanism.isCalculable : ImplicatureMechanism → Prop

A mechanism is calculable iff inferences derived by it could in principle be reconstructed from cooperative reasoning over alternatives. This is the case for every mechanism in the library except the lexical one, which by definition encodes the inference in the lexical entry.

Grice's calculability test is the philosophical anchor of the conversational/conventional distinction.

Equations

• ImplicatureMechanism.lexical.isCalculable = False
• x✝.isCalculable = True

@[implicit_reducible]

instance instDecidablePredImplicatureMechanismIsCalculable : DecidablePred ImplicatureMechanism.isCalculable

Equations

• instDecidablePredImplicatureMechanismIsCalculable ImplicatureMechanism.lexical = isFalse not_false
• instDecidablePredImplicatureMechanismIsCalculable ImplicatureMechanism.neoGricean = isTrue trivial
• instDecidablePredImplicatureMechanismIsCalculable ImplicatureMechanism.exhIE = isTrue trivial
• instDecidablePredImplicatureMechanismIsCalculable ImplicatureMechanism.exhII = isTrue trivial
• instDecidablePredImplicatureMechanismIsCalculable ImplicatureMechanism.exhIEII = isTrue trivial
• instDecidablePredImplicatureMechanismIsCalculable ImplicatureMechanism.rsa = isTrue trivial
• instDecidablePredImplicatureMechanismIsCalculable ImplicatureMechanism.ibr = isTrue trivial
• instDecidablePredImplicatureMechanismIsCalculable ImplicatureMechanism.bpsPresuppositional = isTrue trivial

def ImplicatureKind.isNonDetachable : ImplicatureKind → Prop

A kind is non-detachable iff inferences of that kind depend on asserted content rather than asserted form. The exception is manner, whose entire raison d'être is form-relativity.

@cite{horn-1984}, @cite{levinson-2000}.

Equations

• ImplicatureKind.manner.isNonDetachable = False
• x✝.isNonDetachable = True

@[implicit_reducible]

instance instDecidablePredImplicatureKindIsNonDetachable : DecidablePred ImplicatureKind.isNonDetachable

Equations

• instDecidablePredImplicatureKindIsNonDetachable ImplicatureKind.manner = isFalse not_false
• instDecidablePredImplicatureKindIsNonDetachable ImplicatureKind.scalar = isTrue trivial
• instDecidablePredImplicatureKindIsNonDetachable ImplicatureKind.freeChoice = isTrue trivial
• instDecidablePredImplicatureKindIsNonDetachable ImplicatureKind.ignorance = isTrue trivial
• instDecidablePredImplicatureKindIsNonDetachable ImplicatureKind.clausal = isTrue trivial
• instDecidablePredImplicatureKindIsNonDetachable ImplicatureKind.conventional = isTrue trivial

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

An implicature i derived from assertion φ is cancellable iff there exists a continuation cancel that:

1. is consistent with φ (∃ w, φ w ∧ cancel w), and
2. contradicts the implicature (∀ w, cancel w → ¬ i.content w).

This formalizes the standard Sadock test: "Some students passed — in fact, all of them did" is felicitous (the not all implicature cancels) iff the continuation "all of them did" is consistent with the assertion and contradicts "not all."

Negation of IsCancellable is the load-bearing diagnostic for the @cite{bassi-delpinal-sauerland-2021} Presuppositional EXH account: when pex outputs are wrapped as Implicature W Prop with assertion := PrProp.holds · p and content := p.presup, the non-cancellability follows from holds → presup via IsCancellable.false_of_assertion_implies_content. The substantive content of "presuppositions fail cancellability" comes from the structural assertion-vs-presupposition split in PrProp, not from stipulation. The bridge theorem bps_not_cancellable is in Theories/Semantics/Exhaustification/Presuppositional.lean.

Equations

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

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

Cancellation by the negation of the implicature itself: if there exists an assertion-world where the implicature fails, then ¬i.content witnesses cancellability. The most common cancellation form.

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

The load-bearing non-cancellability principle: if every assertion-world satisfies the implicature content, no continuation can cancel it. Used by the BPS bridge — when assertion is pex.holds and content is pex.presup, this fires from holds → presup.

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

An implicature i derived from assertion φ is reinforceable iff the implicature content is not already entailed by the assertion alone: ∃ w, φ w ∧ ¬ i.content w.

This formalizes the standard "can be reinforced without redundancy" test: "Some students passed, but not all" is felicitous (the not all implicature reinforces non-redundantly) iff the assertion some students passed does not already entail not all.

Note the equivalence: a reinforceable implicature is exactly one whose content is genuinely additional information beyond the assertion. By IsCancellable.of_assertion_compatible_with_negation, reinforceable inferences are cancellable (the same witness works), so reinforceability implies cancellability. The converse may fail (@cite{hirschberg-1985}).

Equations

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

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

Reinforceable ⇒ cancellable. The two diagnostics are not independent: reinforceability is the stricter condition.

def Implicature.IsCalculable {W : Type u_1} {S : Type u_2} (i : Implicature W S) : Prop

An implicature is calculable iff its mechanism is. Polymorphic in the strength type: only the mechanism field is inspected.

Equations

• i.IsCalculable = i.mechanism.isCalculable

@[implicit_reducible]

instance Implicature.instDecidableIsCalculable {W : Type u_1} {S : Type u_2} (i : Implicature W S) : Decidable i.IsCalculable

Equations

• i.instDecidableIsCalculable = Implicature.instDecidableIsCalculable._aux_1 i

theorem Implicature.isCalculable_iff_not_lexical {W : Type u_1} {S : Type u_2} (i : Implicature W S) : i.IsCalculable ↔ i.mechanism ≠ ImplicatureMechanism.lexical

The lexical mechanism is the unique non-calculable mechanism.

def Implicature.IsNonDetachable {W : Type u_1} {S : Type u_2} (i : Implicature W S) : Prop

An implicature is non-detachable iff its kind is. Polymorphic in the strength type: only the kind field is inspected.

Equations

• i.IsNonDetachable = i.kind.isNonDetachable

@[implicit_reducible]

instance Implicature.instDecidableIsNonDetachable {W : Type u_1} {S : Type u_2} (i : Implicature W S) : Decidable i.IsNonDetachable

Equations

• i.instDecidableIsNonDetachable = Implicature.instDecidableIsNonDetachable._aux_1 i

structure Implicature.GriceanProfile {W : Type u_1} (φ : W → Prop) (i : Implicature W Prop) : Prop

A bundle of the four standard diagnostics holding for an implicature relative to its assertion. Useful as a single hypothesis for downstream theorems.

• cancellable : IsCancellable φ i
• reinforceable : IsReinforceable φ i
• calculable : i.IsCalculable
• nonDetachable : i.IsNonDetachable

theorem Implicature.lexical_not_calculable {W : Type u_1} {S : Type u_2} (i : Implicature W S) (hLex : i.mechanism = ImplicatureMechanism.lexical) : ¬i.IsCalculable

The lexical mechanism is by definition not derived from cooperative reasoning — the inference is encoded in the lexical entry — so it fails calculability. The agreement with @cite{grice-1975}'s original conventional/conversational distinction is the contentful theorem here. (Conventional implicatures in @cite{potts-2005}'s sense are the canonical instantiation: kind .conventional paired with mechanism .lexical. The kind hypothesis is unnecessary for the proof; the mechanism alone suffices.)

theorem Implicature.manner_is_detachable {W : Type u_1} {S : Type u_2} (i : Implicature W S) (h : i.kind = ImplicatureKind.manner) : ¬i.IsNonDetachable

Manner implicatures are by definition form-relative, so they fail non-detachability. The agreement with @cite{horn-1984}'s Division of Pragmatic Labor is the contentful theorem.