Neo-Gricean Pragmatics: Basic Definitions

Core formalization of the Standard Recipe from @cite{geurts-2010} Chapter 2.

Key Concepts

1. Belief States (Geurts p.39 diagram)

   • Belief: Bel_S(ψ)
   • Disbelief: Bel_S(¬ψ)
   • No Opinion: ¬Bel_S(ψ) ∧ ¬Bel_S(¬ψ)

2. Standard Recipe (Geurts p.32) The derivation mechanism for quantity implicatures:

   • Step 1: Speaker said φ
   • Step 2: There exists stronger alternative ψ
   • Step 3: Speaker didn't say ψ
   • Step 4: Therefore ¬Bel_S(ψ) (weak implicature)
   • Step 5: With competence, Bel_S(¬ψ) (strong implicature)

3. Competence Assumption Speaker knows whether ψ: Bel_S(ψ) ∨ Bel_S(¬ψ)

Reference: Geurts, B. (2010). Quantity Implicatures. Cambridge University Press.

inductive Implicature.BeliefState : Type

Speaker's belief state about a proposition ψ.

Following Geurts' diagram on p.39:

• belief: Bel_S(ψ) — speaker believes ψ is true
• disbelief: Bel_S(¬ψ) — speaker believes ψ is false
• noOpinion: ¬Bel_S(ψ) ∧ ¬Bel_S(¬ψ) — speaker has no opinion

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

@[implicit_reducible]

instance Implicature.instDecidableEqBeliefState : DecidableEq BeliefState

Equations

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

@[implicit_reducible]

instance Implicature.instReprBeliefState : Repr BeliefState

Equations

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

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

Equations

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

def Implicature.competent : BeliefState → Bool

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

A competent speaker is not agnostic — they have an opinion one way or the other.

Equations

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

def Implicature.nonBelief : BeliefState → Bool

Non-belief: speaker doesn't believe ψ. Formally: ¬Bel_S(ψ)

This is the weak implicature -- speaker might believe ¬ψ or have no opinion.

Equations

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

def Implicature.strongImpl : BeliefState → Bool

Strong implicature: speaker believes ¬ψ. Formally: Bel_S(¬ψ)

This requires competence to derive from nonBelief.

Equations

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

structure Implicature.StandardRecipeResult : Type

The result of applying the Standard Recipe to an utterance.

• weakImplicature: ¬Bel_S(ψ) — always derivable from Quantity
• competenceHolds: Bel_S(ψ) ∨ Bel_S(¬ψ) — depends on context
• strongImplicature: Bel_S(¬ψ) — only if both weak + competence

• weakImplicature : Bool
• competenceHolds : Bool
• strongImplicature : Bool

@[implicit_reducible]

instance Implicature.instReprStandardRecipeResult : Repr StandardRecipeResult

Equations

• Implicature.instReprStandardRecipeResult = { reprPrec := Implicature.instReprStandardRecipeResult.repr }

def Implicature.instReprStandardRecipeResult.repr : StandardRecipeResult → ℕ → Std.Format

Equations

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

def Implicature.applyStandardRecipe (b : BeliefState) : StandardRecipeResult

Apply the Standard Recipe to derive implicatures.

Given a belief state about the alternative ψ, determine what implicatures arise.

Equations

• Implicature.applyStandardRecipe b = { weakImplicature := Implicature.nonBelief b, competenceHolds := Implicature.competent b, strongImplicature := Implicature.strongImpl b }

theorem Implicature.competence_strengthening (b : BeliefState) : nonBelief b = true → competent b = true → strongImpl b = true

Theorem: Competence Strengthening

weak implicature + competence → strong implicature

If the speaker doesn't believe ψ (weak) AND is competent (knows whether ψ), then the speaker must believe ¬ψ (strong).

Formally: ¬Bel_S(ψ) ∧ (Bel_S(ψ) ∨ Bel_S(¬ψ)) → Bel_S(¬ψ)

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

Theorem: Weak Without Strong

A weak implicature can hold without the strong implicature (when the speaker lacks competence).

theorem Implicature.strong_implies_weak (b : BeliefState) : strongImpl b = true → nonBelief b = true

Theorem: Strong Implies Weak

If the strong implicature holds, the weak implicature holds. Bel_S(¬ψ) → ¬Bel_S(ψ)

theorem Implicature.strong_implies_competent (b : BeliefState) : strongImpl b = true → competent b = true

Theorem: Strong Implies Competent

If the strong implicature holds, the speaker is competent. Bel_S(¬ψ) → (Bel_S(ψ) ∨ Bel_S(¬ψ))

theorem Implicature.no_belief_weak (b : BeliefState) : b ≠ BeliefState.belief → nonBelief b = true

Theorem: No Belief Implies Weak Implicature

If the speaker doesn't believe ψ, the weak implicature holds. This is direct from the definition.

inductive Implicature.ImplicatureOutcome : Type

Three possible outcomes for a hearer processing an implicature:

1. Undecided: Weak implicature only (¬Bel_S(ψ)), competence not assumed
2. Strong: Competence holds, derive Bel_S(¬ψ)
3. Incompetent: Competence rejected, speaker has no opinion

Following Geurts' discussion on p.40.

• undecided : ImplicatureOutcome
• strongInference : ImplicatureOutcome
• incompetent : ImplicatureOutcome

@[implicit_reducible]

instance Implicature.instDecidableEqImplicatureOutcome : DecidableEq ImplicatureOutcome

Equations

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

@[implicit_reducible]

instance Implicature.instReprImplicatureOutcome : Repr ImplicatureOutcome

Equations

• Implicature.instReprImplicatureOutcome = { reprPrec := Implicature.instReprImplicatureOutcome.repr }

def Implicature.instReprImplicatureOutcome.repr : ImplicatureOutcome → ℕ → Std.Format

Equations

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

def Implicature.outcomeOf : BeliefState → ImplicatureOutcome

Map a belief state to its implicature outcome.

Equations

• Implicature.outcomeOf Implicature.BeliefState.belief = Implicature.ImplicatureOutcome.undecided
• Implicature.outcomeOf Implicature.BeliefState.disbelief = Implicature.ImplicatureOutcome.strongInference
• Implicature.outcomeOf Implicature.BeliefState.noOpinion = Implicature.ImplicatureOutcome.incompetent

theorem Implicature.outcomes_exhaustive (b : BeliefState) : outcomeOf b = ImplicatureOutcome.undecided ∧ nonBelief b = false ∨ outcomeOf b = ImplicatureOutcome.strongInference ∧ strongImpl b = true ∨ outcomeOf b = ImplicatureOutcome.incompetent ∧ nonBelief b = true ∧ competent b = false

Theorem: Outcomes are Exhaustive and Distinct

The three outcomes partition the space of competent/weak combinations.

inductive Implicature.SITrigger : Type

When do scalar implicatures get triggered?

Both views are Neo-Gricean (pragmatic, maxim-based), but differ on triggering:

• Defaultism (Levinson): SIs fire by default, automatically
• Contextualism (Geurts): SIs depend on context (QUD, salience)

Reference:

• Levinson, S. (2000). Presumptive Meanings. MIT Press.
• Geurts, B. (2010). Quantity Implicatures. Ch. 5.

• default : SITrigger
• contextual : SITrigger

@[implicit_reducible]

instance Implicature.instDecidableEqSITrigger : DecidableEq SITrigger

Equations

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

def Implicature.instReprSITrigger.repr : SITrigger → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Implicature.instReprSITrigger : Repr SITrigger

Equations

• Implicature.instReprSITrigger = { reprPrec := Implicature.instReprSITrigger.repr }

structure Implicature.NeoGriceanParams : Type

Parameters that characterize a Neo-Gricean theory variant.

• trigger : SITrigger

  When do SIs get triggered?

• competenceEnabled : Bool

  Is competence assumption enabled?

• predictedNeutralRate : ℕ

  Predicted baseline SI rate in neutral context (percentage)

def Implicature.instReprNeoGriceanParams.repr : NeoGriceanParams → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Implicature.instReprNeoGriceanParams : Repr NeoGriceanParams

Equations

• Implicature.instReprNeoGriceanParams = { reprPrec := Implicature.instReprNeoGriceanParams.repr }

def Implicature.levinsonParams : NeoGriceanParams

Levinson's Defaultism: SIs are presumptive meanings that arise automatically.

Key claims:

• SIs are "default" inferences
• They arise rapidly and automatically
• Context can cancel them, but they're the default

Prediction: High SI rates (~90%+) even in neutral contexts.

Equations

• Implicature.levinsonParams = { trigger := Implicature.SITrigger.default, competenceEnabled := true, predictedNeutralRate := 90 }

def Implicature.geurtsParams : NeoGriceanParams

Geurts' Contextualism: SIs depend on the Question Under Discussion.

Key claims:

• SIs are not automatic defaults
• They arise when alternatives are contextually salient
• The QUD determines which alternatives matter

Prediction: Moderate SI rates (~35%) in truly neutral contexts; asking about the SI raises salience and inflates rates.

Equations

• Implicature.geurtsParams = { trigger := Implicature.SITrigger.contextual, competenceEnabled := true, predictedNeutralRate := 35 }

def Implicature.predictsTaskEffect (p : NeoGriceanParams) : Bool

Does this theory variant predict a task effect?

Contextualism predicts that asking "does this imply not-all?" will raise SI rates by making the alternative salient.

Defaultism predicts no task effect since SIs are automatic.

Equations

• Implicature.predictsTaskEffect p = match p.trigger with | Implicature.SITrigger.default => false | Implicature.SITrigger.contextual => true

def Implicature.predictsHighNeutralRate (p : NeoGriceanParams) : Bool

Does this theory variant predict high SI rates in neutral contexts?

Equations

• Implicature.predictsHighNeutralRate p = decide (p.predictedNeutralRate > 50)

structure Implicature.NeoGriceanStructure : Type

Implicature's internal representation for implicature analysis.

Bundles the Standard Recipe result with context information.

• result : StandardRecipeResult

  The Standard Recipe result (weak/strong implicature, competence)

• polarity : Core.NaturalLogic.ContextPolarity

  Context polarity (upward vs downward entailing)

• scalarPosition : Option ℕ

  Position of the scalar item (if any)

• params : NeoGriceanParams

  Which variant of Implicature (for baseline rate)

@[implicit_reducible]

instance Implicature.instReprNeoGriceanStructure : Repr NeoGriceanStructure

Equations

• Implicature.instReprNeoGriceanStructure = { reprPrec := Implicature.instReprNeoGriceanStructure.repr }

def Implicature.instReprNeoGriceanStructure.repr : NeoGriceanStructure → ℕ → Std.Format

Equations

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

def Implicature.isScalarQuantifierWord (w : Word) : Bool

Check if a word is a scalar quantifier

Equations

• Implicature.isScalarQuantifierWord w = (w.form == "some" || w.form == "every" || w.form == "all" || w.form == "most")

def Implicature.findScalarPositionInWords (ws : List Word) : Option ℕ

Find the position of a scalar item in a word list

Equations

• Implicature.findScalarPositionInWords ws = List.findIdx? Implicature.isScalarQuantifierWord ws

def Implicature.determinePolarityFromWords (ws : List Word) : Core.NaturalLogic.ContextPolarity

Determine context polarity from words. Simplified: checks for negation markers.

Equations

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

def Implicature.parseToNeoGricean (ws : List Word) : Option NeoGriceanStructure

Parse words into Implicature structure.

For now, uses a simplified analysis:

• Finds scalar item position
• Determines polarity from negation markers
• Assumes competence holds and derives strong implicature in UE

Equations

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