Implicature: Cross-Mechanism Spine

@cite{grice-1975} @cite{horn-1972} @cite{gazdar-1979} @cite{sauerland-2004} @cite{chierchia-fox-spector-2012} @cite{bar-lev-fox-2020} @cite{frank-goodman-2012} @cite{goodman-stuhlmuller-2013} @cite{delpinal-bassi-sauerland-2024}

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 (@cite{sauerland-2004}, @cite{chierchia-2004}, @cite{fox-2007}, @cite{bar-lev-fox-2020}) treats an implicature as a discrete proposition — instantiated by S := Prop.
• The graded / Bayesian tradition (@cite{frank-goodman-2012}, @cite{goodman-stuhlmuller-2013}, @cite{bergen-levy-goodman-2016}) 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 (@cite{horn-1972}, @cite{sauerland-2004})
• freeChoice — distributive inference from disjunction under a modal: ◇(A ∨ B) ⇝ ◇A ∧ ◇B (@cite{kamp-1973}, @cite{zimmermann-2000}, @cite{fox-2007})
• ignorance — speaker-uncertainty inference; "the primary implicature" of @cite{sauerland-2004}, going back to @cite{gazdar-1979} epistemic implicature
• clausal — ¬K(p) ∧ ¬K(q) from "p or q" (@cite{gazdar-1979})
• manner — marked-form-implicates-marked-meaning, the R-principle / M-principle (@cite{horn-1984}, @cite{levinson-2000} ch. 2)
• conventional — lexically encoded non-at-issue content; but, therefore, expressives (@cite{grice-1975}, @cite{potts-2005})

• 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 ⋯

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✝

@[implicit_reducible]

instance instReprImplicatureKind : Repr ImplicatureKind

Equations

• instReprImplicatureKind = { reprPrec := instReprImplicatureKind.repr }

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 (@cite{geurts-2010}, @cite{sauerland-2004})
• exhIE — Innocent Exclusion (@cite{fox-2007})
• exhII — Innocent Inclusion (@cite{bar-lev-fox-2020})
• exhIEII — combined IE+II, the canonical post-2020 EXH (@cite{bar-lev-fox-2020})
• rsa — Bayesian listener-speaker recursion (@cite{frank-goodman-2012}, @cite{goodman-stuhlmuller-2013})
• ibr — Iterated Best Response (@cite{franke-2011})
• bpsPresuppositional — Presuppositional EXH (pex), the assertion/presupposition split that makes the inferred content project like a presupposition (@cite{bassi-delpinal-sauerland-2021}, @cite{delpinal-bassi-sauerland-2024})
• lexical — encoded in lexical entries (@cite{potts-2005})

• 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 ⋯

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✝

@[implicit_reducible]

instance instReprImplicatureMechanism : Repr ImplicatureMechanism

Equations

• instReprImplicatureMechanism = { reprPrec := instReprImplicatureMechanism.repr }

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 @cite{chierchia-fox-spector-2012} §3) or characteristically fail to agree (the FC non-equivalence per @cite{bar-lev-fox-2020}).

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