Neo-Gricean pragmatics: epistemic states and the Standard Recipe

[Sau04] [Geu10]

The epistemic layer of Neo-Gricean implicature: an EpistemicState (the worlds compatible with the speaker's knowledge) with knows (K) and possible (P) realized as box/diamond over a serial accessibility from Core.Logic.Modal, and the Standard Recipe run over the derived three-way BeliefState classification.

[Sau04] distinguishes primary implicatures ¬Kψ from secondary implicatures K¬ψ, a secondary arising only when K¬ψ is consistent with the assertion together with all primary implicatures. The epistemic modalization ¬Kψ goes back to [Soa82] and [Hor89]; the competence step Kψ ∨ K¬ψ strengthening primaries to secondaries is formalized by [Sau04], [vRS04], and [Spe06]; [Geu10] is the textbook presentation.

This file provides the modal substrate, the consistency-gated derivation (SatisfiesPrimaries, SecondaryLicensed), and the recipe over the belief-state classification. secondary_blocked_if_possible and primary_possibility are instances of K/P duality; the flagship multi-alternative blocking case is exercised in Studies/Sauerland2004.lean.

The asymmetric-entailment primitive characterizing primary-implicature alternatives is asymStrongerOn in Semantics/Entailment/AsymStronger.lean; a consumer writes alts.filter (asymStrongerOn e.possible · φ) directly. For the graded counterpart of competence (the RSA knowledgeability parameter) see Pragmatics/RSA/; Studies/Franke2011/RSABridge.lean relates RSA speakers to IBR argmax behaviour.

Epistemic states and the K/P operators

structure NeoGricean.EpistemicState (W : Type u_2) : Type u_2

An epistemic state: the (nonempty, finite) set of worlds compatible with the speaker's knowledge.

• possible : Finset W

  Worlds compatible with speaker's knowledge

• nonempty : self.possible.Nonempty

  Non-empty (speaker knows something is true)

def NeoGricean.knows {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) : Prop

K operator: the speaker knows φ iff φ holds in all epistemically possible worlds.

Equations

• NeoGricean.knows e φ = ∀ w ∈ e.possible, φ w

@[implicit_reducible]

instance NeoGricean.instDecidableKnowsOfDecidablePred {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) [DecidablePred φ] : Decidable (knows e φ)

Equations

• NeoGricean.instDecidableKnowsOfDecidablePred e φ = NeoGricean.instDecidableKnowsOfDecidablePred._aux_1 e φ

def NeoGricean.possible {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) : Prop

P operator: the speaker considers φ possible.

Equations

• NeoGricean.possible e φ = ∃ w ∈ e.possible, φ w

@[implicit_reducible]

instance NeoGricean.instDecidablePossibleOfDecidablePred {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) [DecidablePred φ] : Decidable (possible e φ)

Equations

• NeoGricean.instDecidablePossibleOfDecidablePred e φ = NeoGricean.instDecidablePossibleOfDecidablePred._aux_1 e φ

K/P as restricted modality

knows/possible are box/diamond over the (world-independent) epistemic accessibility accessFrom e, serial because e.possible is nonempty. The epistemic square of opposition is Core.Logic.Modal.modalSquare (accessFrom e) with modalSquare_relations discharged by this IsSerial instance.

def NeoGricean.accessFrom {W : Type u_1} (e : EpistemicState W) : Core.Logic.Modal.AccessRel W

Epistemic accessibility: from any world, the speaker's live possibilities.

Equations

• NeoGricean.accessFrom e x✝ w' = (w' ∈ e.possible)

instance NeoGricean.instIsSerialAccessFrom {W : Type u_1} (e : EpistemicState W) : Core.Logic.Modal.IsSerial (accessFrom e)

theorem NeoGricean.knows_eq_box {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) (w : W) : knows e φ = Core.Logic.Modal.box (accessFrom e) φ w

K is □ over epistemic accessibility.

theorem NeoGricean.possible_eq_diamond {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) (w : W) : possible e φ = Core.Logic.Modal.diamond (accessFrom e) φ w

P is ◇ over epistemic accessibility.

theorem NeoGricean.duality {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) : (¬knows e fun (w : W) => ¬φ w) ↔ possible e φ

Epistemic duality: ¬K¬φ ↔ Pφ — the box–diamond duality underlying the modal square of opposition (Core.Logic.Modal.modalSquare_relations).

def NeoGricean.hasSecondaryImplicature {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) : Prop

Secondary implicature: the speaker knows the alternative is false.

Equations

• NeoGricean.hasSecondaryImplicature e ψ = NeoGricean.knows e fun (w : W) => ¬ψ w

@[implicit_reducible]

instance NeoGricean.instDecidableHasSecondaryImplicatureOfDecidablePred {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) [DecidablePred ψ] : Decidable (hasSecondaryImplicature e ψ)

Equations

• NeoGricean.instDecidableHasSecondaryImplicatureOfDecidablePred e ψ = NeoGricean.instDecidableHasSecondaryImplicatureOfDecidablePred._aux_1 e ψ

theorem NeoGricean.secondary_blocked_if_possible {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) : possible e ψ → ¬hasSecondaryImplicature e ψ

If ψ is epistemically possible, K¬ψ fails. An instance of duality; the substrate fact used when checking a candidate secondary implicature against the speaker's state.

theorem NeoGricean.primary_possibility {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) : ¬knows e ψ → possible e fun (w : W) => ¬ψ w

A primary implicature ¬Kψ entails that ¬ψ is epistemically possible. An instance of duality.

The Sauerland derivation

Asserting φ against scalar alternatives alts commits the speaker to Kφ plus, for each alternative, the primary implicature ¬Kψ ([Sau04] (42), verified p. 383). A secondary implicature K¬ψ arises exactly when it is consistent with that commitment set ([Sau04] (43)): here, when some epistemic state realizes the commitments together with K¬ψ. secondaryLicensed_iff_reinforceable identifies the single-alternative case with the reinforceability diagnostic; the flagship multi-alternative blocking case (K¬A blocked for a disjunction because it forces KB) is Studies/Sauerland2004.lean.

def NeoGricean.SatisfiesPrimaries {W : Type u_1} (e : EpistemicState W) (φ : W → Prop) (alts : List (W → Prop)) : Prop

The speaker commitment after asserting φ against alts: the assertion is known (Kφ) and every primary implicature holds (¬Kψ for each alternative). Per [Sau04] (42), the caller supplies only the asymmetrically-stronger alternatives (ψ ⇒ φ but not φ ⇒ ψ, e.g. via asymStrongerOn); the definition itself does not enforce the filter.

Equations

• NeoGricean.SatisfiesPrimaries e φ alts = (NeoGricean.knows e φ ∧ ∀ ψ ∈ alts, ¬NeoGricean.knows e ψ)

def NeoGricean.SecondaryLicensed {W : Type u_1} (φ : W → Prop) (alts : List (W → Prop)) (ψ : W → Prop) : Prop

Sauerland's consistency condition: the secondary implicature K¬ψ is licensed iff some epistemic state realizes the assertion, all primary implicatures, and K¬ψ jointly.

Equations

• NeoGricean.SecondaryLicensed φ alts ψ = ∃ (e : NeoGricean.EpistemicState W), NeoGricean.SatisfiesPrimaries e φ alts ∧ NeoGricean.hasSecondaryImplicature e ψ

theorem NeoGricean.secondaryLicensed_iff_strengthening_consistent {W : Type u_1} [Fintype W] (φ ψ : W → Prop) [DecidablePred φ] [DecidablePred ψ] : SecondaryLicensed φ [ψ] ψ ↔ ∃ (w : W), φ w ∧ ¬ψ w

For a lone alternative, Sauerland licensing reduces to consistency of the strengthened meaning: K¬ψ is compatible with the commitments Kφ ∧ ¬Kψ exactly when φ ∧ ¬ψ is realizable at some world — the same condition under which the content ¬ψ is a non-redundant strengthening of φ (Implicature.IsReinforceable φ ψ in the diagnostics' pair form).

The three-way belief-state classification

BeliefState is the decidable classification of a speaker's attitude toward one alternative ψ: Bel_S(ψ), Bel_S(¬ψ), or no opinion. EpistemicState.beliefState grounds the enum in the modal substrate, so the Standard Recipe below is a projection of K/P reasoning, not a parallel encoding.

inductive NeoGricean.BeliefState : Type

Speaker's belief state about a proposition ψ: belief Bel_S(ψ), disbelief Bel_S(¬ψ), or no opinion ¬Bel_S(ψ) ∧ ¬Bel_S(¬ψ).

• belief : BeliefState
• disbelief : BeliefState
• noOpinion : BeliefState

@[implicit_reducible]

instance NeoGricean.instDecidableEqBeliefState : DecidableEq BeliefState

Equations

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

@[implicit_reducible]

instance NeoGricean.instReprBeliefState : Repr BeliefState

Equations

• NeoGricean.instReprBeliefState = { reprPrec := NeoGricean.instReprBeliefState.repr }

def NeoGricean.instReprBeliefState.repr : BeliefState → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def NeoGricean.EpistemicState.beliefState {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) [DecidablePred ψ] : BeliefState

Classify an epistemic state by its attitude toward ψ: Kψ is belief, K¬ψ disbelief, anything else no opinion.

Equations

• One or more equations did not get rendered due to their size.

def NeoGricean.competent : BeliefState → Bool

Competence: the speaker knows whether ψ, Bel_S(ψ) ∨ Bel_S(¬ψ).

Equations

• NeoGricean.competent NeoGricean.BeliefState.belief = true
• NeoGricean.competent NeoGricean.BeliefState.disbelief = true
• NeoGricean.competent NeoGricean.BeliefState.noOpinion = false

def NeoGricean.nonBelief : BeliefState → Bool

Non-belief ¬Bel_S(ψ) — the weak (primary) implicature.

Equations

• NeoGricean.nonBelief NeoGricean.BeliefState.belief = false
• NeoGricean.nonBelief NeoGricean.BeliefState.disbelief = true
• NeoGricean.nonBelief NeoGricean.BeliefState.noOpinion = true

def NeoGricean.strongImpl : BeliefState → Bool

Strong (secondary) implicature Bel_S(¬ψ).

Equations

• NeoGricean.strongImpl NeoGricean.BeliefState.belief = false
• NeoGricean.strongImpl NeoGricean.BeliefState.disbelief = true
• NeoGricean.strongImpl NeoGricean.BeliefState.noOpinion = false

theorem NeoGricean.beliefState_disbelief_iff {W : Type u_1} (e : EpistemicState W) (ψ : W → Prop) [DecidablePred ψ] (h : ¬knows e ψ) : e.beliefState ψ = BeliefState.disbelief ↔ hasSecondaryImplicature e ψ

The classification is faithful: disbelief holds exactly when the secondary implicature K¬ψ does.

theorem NeoGricean.competence_strengthening {b : BeliefState} (hweak : nonBelief b = true) (hcomp : competent b = true) : strongImpl b = true

Competence strengthening: ¬Bel_S(ψ) ∧ (Bel_S(ψ) ∨ Bel_S(¬ψ)) → Bel_S(¬ψ).

theorem NeoGricean.weak_without_strong : ∃ (b : BeliefState), nonBelief b = true ∧ strongImpl b = false

A weak implicature can hold without the strong one (incompetent speaker).

theorem NeoGricean.strong_implies_weak {b : BeliefState} (h : strongImpl b = true) : nonBelief b = true

Bel_S(¬ψ) → ¬Bel_S(ψ).

theorem NeoGricean.strong_implies_competent {b : BeliefState} (h : strongImpl b = true) : competent b = true

Bel_S(¬ψ) → Bel_S(ψ) ∨ Bel_S(¬ψ).

Running the recipe

processAlternative applies the Standard Recipe to one alternative, gated by whether the hearer assumes competence. The three outcome_* theorems are [Geu10]'s outcome typology.

structure NeoGricean.ImplicatureProcessing : Type

Outcome of processing one alternative: the inferred belief state, whether the weak implicature holds, whether competence was assumed (and consistent), and whether the strong implicature was derived.

• beliefState : BeliefState

  The belief state inferred

• weakHolds : Bool

  Whether weak implicature ¬Bel_S(ψ) holds

• competenceAssumed : Bool

  Whether competence was assumed

• strongDerived : Bool

  Whether strong implicature Bel_S(¬ψ) was derived

def NeoGricean.instReprImplicatureProcessing.repr : ImplicatureProcessing → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance NeoGricean.instReprImplicatureProcessing : Repr ImplicatureProcessing

Equations

• NeoGricean.instReprImplicatureProcessing = { reprPrec := NeoGricean.instReprImplicatureProcessing.repr }

def NeoGricean.processAlternative (assumeCompetence : Bool) (b : BeliefState) : ImplicatureProcessing

Run the Standard Recipe on one alternative under a competence assumption.

Equations

• One or more equations did not get rendered due to their size.

theorem NeoGricean.outcome_i_undecided {b : BeliefState} (hne : b ≠ BeliefState.belief) : (processAlternative false b).weakHolds = true ∧ (processAlternative false b).strongDerived = false

Outcome i (undecided): without the competence assumption, only the weak implicature arises.

theorem NeoGricean.outcome_ii_strong : (processAlternative true BeliefState.disbelief).weakHolds = true ∧ (processAlternative true BeliefState.disbelief).competenceAssumed = true ∧ (processAlternative true BeliefState.disbelief).strongDerived = true

Outcome ii (strong): competence assumed and consistent — the strong implicature is derived.

theorem NeoGricean.outcome_iii_incompetent : (processAlternative true BeliefState.noOpinion).weakHolds = true ∧ (processAlternative true BeliefState.noOpinion).competenceAssumed = false ∧ (processAlternative true BeliefState.noOpinion).strongDerived = false

Outcome iii (incompetent): the speaker has no opinion, so the competence assumption fails and only the weak implicature survives.