Implicature: Cross-Mechanism Spine

[Gri75] [Hor72] [Sta79] [Sau04] [CFS12] [BLF20] [FG12] [GS13] [DPBS24]

Defines the central Implicature W S type — the cross-mechanism representation of a pragmatic inference, parameterized by a world type W and a strength type S.

Why polymorphic in S?

The ontology of "what an implicature is" is contested in the literature:

• The discrete / grammaticalist tradition ([Sau04], [Chi04], [Fox07], [BLF20]) treats an implicature as a discrete proposition — instantiated by S := Prop.
• The graded / Bayesian tradition ([FG12], [GS13], [BLG16]) treats interpretation as a posterior shift; "the implicature" is a change in degrees of belief, not a discrete proposition. Instantiated by S := ℝ≥0 or similar graded type.
• Trivalent accounts (presupposition-bearing, partial) instantiate with S := Truth3.

Parameterizing rather than committing lets each mechanism use its native output type. The categorical Gricean diagnostics (Diagnostics.lean) are then specialized to S = Prop — they're an artifact of the discrete ontology and don't generalize to ℝ-valued contents. Cross-mechanism comparison between, say, RSA and Sauerland requires explicit projection (thresholding a posterior), which is itself a contestable empirical claim that should be formalized as such, not hidden in a coercion.

Strength type is explicit

Callers must supply S explicitly: Implicature W Prop for the categorical / Gricean / grammaticalist ontology, Implicature W ℝ≥0 for graded / RSA-style. There is no default — making the strength commitment visible at every use site is part of the make-incompatibilities-visible discipline.

Bridge architecture

Cross-mechanism agreement theorems (in sibling files) state results in terms of Agree, the pointwise content-equality relation. For S = Prop, this collapses to the iff version under propositional extensionality.

Naming

Following Filter.Filter-style mathlib precedent: the central struct Implicature is declared at the root, while supporting enums (ImplicatureKind, ImplicatureMechanism) and helper definitions live under namespace Implicature. The existing per-file sub-namespaces (Implicature.Markedness, Implicature.Scales, …) coexist because Lean permits a type and a namespace to share a name.

inductive ImplicatureKind : Type

Taxonomic classification of pragmatic inferences.

The post-Grice consensus distinguishes:

• scalar — derived from a Horn scale; canonical some ⇝ not all ([Hor72], [Sau04])
• freeChoice — distributive inference from disjunction under a modal: ◇(A ∨ B) ⇝ ◇A ∧ ◇B ([Kam73], [Zim00], [Fox07])
• ignorance — speaker-uncertainty inference; "the primary implicature" of [Sau04], going back to [Sta79] epistemic implicature
• clausal — ¬K(p) ∧ ¬K(q) from "p or q" ([Sta79])
• manner — marked-form-implicates-marked-meaning, the R-principle / M-principle ([Hor84], [Lev00] ch. 2)
• conventional — lexically encoded non-at-issue content; but, therefore, expressives ([Gri75], [Pot05])

• scalar : ImplicatureKind
• freeChoice : ImplicatureKind
• ignorance : ImplicatureKind
• clausal : ImplicatureKind
• manner : ImplicatureKind
• conventional : ImplicatureKind

@[implicit_reducible]

instance instDecidableEqImplicatureKind : DecidableEq ImplicatureKind

Equations

• instDecidableEqImplicatureKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprImplicatureKind : Repr ImplicatureKind

Equations

• instReprImplicatureKind = { reprPrec := instReprImplicatureKind.repr }

def instReprImplicatureKind.repr : ImplicatureKind → ℕ → Std.Format

Equations

• instReprImplicatureKind.repr ImplicatureKind.scalar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicatureKind.scalar")).group prec✝
• instReprImplicatureKind.repr ImplicatureKind.freeChoice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicatureKind.freeChoice")).group prec✝
• instReprImplicatureKind.repr ImplicatureKind.ignorance prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicatureKind.ignorance")).group prec✝
• instReprImplicatureKind.repr ImplicatureKind.clausal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicatureKind.clausal")).group prec✝
• instReprImplicatureKind.repr ImplicatureKind.manner prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicatureKind.manner")).group prec✝
• instReprImplicatureKind.repr ImplicatureKind.conventional prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicatureKind.conventional")).group prec✝

def ImplicatureKind.isConversational : ImplicatureKind → Prop

Is this kind a conversational implicature (as opposed to a conventional one)?

Grice's primary distinction. Conversational implicatures are calculable from the cooperative principle and pass the standard diagnostics (cancellability, reinforceability, non-detachability); conventional implicatures fail at least cancellability.

Equations

• ImplicatureKind.conventional.isConversational = False
• x✝.isConversational = True

@[implicit_reducible]

instance instDecidablePredImplicatureKindIsConversational : DecidablePred ImplicatureKind.isConversational

Equations

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

inductive ImplicatureMechanism : Type

The derivation mechanism that produced an implicature.

Tracking provenance lets cross-mechanism agreement and disagreement theorems be stated. Different mechanisms naturally produce different strength types (the S parameter of Implicature):

• neoGricean / exhIE / exhII / exhIEII — discrete outputs (S := Prop)
• rsa — graded posterior (S := ℝ≥0 or similar)
• ibr — discrete fixed-point output (S := Prop)
• bpsPresuppositional — pex output: assertion + presupposition (S := Prop); the inferred content is the presupposed component
• lexical — discrete; encoded in the lexical entry (S := Prop)

The mechanism field tracks provenance regardless of strength type.

Citations:

• neoGricean — Standard Recipe ([Geu10], [Sau04])
• exhIE — Innocent Exclusion ([Fox07])
• exhII — Innocent Inclusion ([BLF20])
• exhIEII — combined IE+II, the canonical post-2020 EXH ([BLF20])
• rsa — Bayesian listener-speaker recursion ([FG12], [GS13])
• ibr — Iterated Best Response ([Fra11])
• bpsPresuppositional — Presuppositional EXH (pex), the assertion/presupposition split that makes the inferred content project like a presupposition ([BDPS21], [DPBS24])
• lexical — encoded in lexical entries ([Pot05])

• neoGricean : ImplicatureMechanism
• exhIE : ImplicatureMechanism
• exhII : ImplicatureMechanism
• exhIEII : ImplicatureMechanism
• rsa : ImplicatureMechanism
• ibr : ImplicatureMechanism
• bpsPresuppositional : ImplicatureMechanism
• lexical : ImplicatureMechanism

@[implicit_reducible]

instance instDecidableEqImplicatureMechanism : DecidableEq ImplicatureMechanism

Equations

• instDecidableEqImplicatureMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprImplicatureMechanism : Repr ImplicatureMechanism

Equations

• instReprImplicatureMechanism = { reprPrec := instReprImplicatureMechanism.repr }

def instReprImplicatureMechanism.repr : ImplicatureMechanism → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprImplicatureMechanism.repr ImplicatureMechanism.rsa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicatureMechanism.rsa")).group prec✝
• instReprImplicatureMechanism.repr ImplicatureMechanism.ibr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicatureMechanism.ibr")).group prec✝

structure Implicature (W : Type u_1) (S : Type u_2) : Type (max u_1 u_2)

A pragmatic inference, parameterized by:

• W — the world type
• S — the strength type (default Prop for the discrete / Gricean / grammaticalist ontology; instantiate with ℝ≥0 for graded / RSA-style; with Truth3 for trivalent)

Every value carries:

• kind — taxonomic classification
• content — the inferred per-world strength (W → S)
• altsUsed — the alternative set that drove derivation
• mechanism — provenance, recording which derivation produced it

The S parameter encodes a real theoretical commitment: see the file docstring. For S = Prop, content is a discrete proposition and the Gricean diagnostics in Diagnostics.lean apply directly. For S = ℝ≥0 (RSA), the diagnostics require an interpretive projection.

• kind : ImplicatureKind

  Taxonomic classification (scalar / freeChoice / ignorance / ...).

• content : W → S

  The inferred per-world strength. For S = Prop, a discrete proposition; for graded S (e.g. ℝ≥0), a probability or score.

• altsUsed : Set (W → S)

  The alternative set that drove derivation.

• mechanism : ImplicatureMechanism

  The derivation mechanism that produced this inference.

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

Is this inference a conversational implicature? Lifts ImplicatureKind.isConversational to Implicature. Polymorphic in the strength type: classification doesn't depend on content.

Equations

• i.isConversational = i.kind.isConversational

@[implicit_reducible]

instance Implicature.instDecidableIsConversational {W : Type u_1} {S : Type u_2} (i : Implicature W S) : Decidable i.isConversational

Equations

• i.instDecidableIsConversational = Implicature.instDecidableIsConversational._aux_1 i

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

Two implicatures agree iff they assign the same strength to every world.

For the default S = Prop, this is ∀ w, i.content w = j.content w, which collapses to the iff version under propositional extensionality. For S = ℝ, it's literal numeric equality of the per-world scores.

Bridge theorems state cross-mechanism agreement in this form. Two implicatures with different mechanism fields can Agree (the canonical Sauerland ≡ exhIE result for non-FC cases per [CFS12] §3) or characteristically fail to agree (the FC non-equivalence per [BLF20]).

Equations

• i.Agree j = ∀ (w : W), i.content w = j.content w

theorem Implicature.Agree.refl {W : Type u_1} {S : Type u_2} (i : Implicature W S) : i.Agree i

theorem Implicature.Agree.symm {W : Type u_1} {S : Type u_2} {i j : Implicature W S} (h : i.Agree j) : j.Agree i

theorem Implicature.Agree.trans {W : Type u_1} {S : Type u_2} {i j k : Implicature W S} (hij : i.Agree j) (hjk : j.Agree k) : i.Agree k