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

instance Implicature.instDecidableEqBeliefState : DecidableEq BeliefState

Equations

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

def Implicature.instBEqBeliefState.beq : BeliefState → BeliefState → Bool

Equations

• Implicature.instBEqBeliefState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Implicature.instBEqBeliefState : BEq BeliefState

Equations

• Implicature.instBEqBeliefState = { beq := Implicature.instBEqBeliefState.beq }

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

Equations

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

instance Implicature.instReprBeliefState : Repr BeliefState

Equations

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

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

instance Implicature.instReprStandardRecipeResult : Repr StandardRecipeResult

Equations

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

def Implicature.instReprStandardRecipeResult.repr : StandardRecipeResult → Nat → 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

instance Implicature.instDecidableEqImplicatureOutcome : DecidableEq ImplicatureOutcome

Equations

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

instance Implicature.instBEqImplicatureOutcome : BEq ImplicatureOutcome

Equations

• Implicature.instBEqImplicatureOutcome = { beq := Implicature.instBEqImplicatureOutcome.beq }

def Implicature.instBEqImplicatureOutcome.beq : ImplicatureOutcome → ImplicatureOutcome → Bool

Equations

• Implicature.instBEqImplicatureOutcome.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Implicature.instReprImplicatureOutcome : Repr ImplicatureOutcome

Equations

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

def Implicature.instReprImplicatureOutcome.repr : ImplicatureOutcome → Nat → 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

instance Implicature.instDecidableEqSITrigger : DecidableEq SITrigger

Equations

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

def Implicature.instBEqSITrigger.beq : SITrigger → SITrigger → Bool

Equations

• Implicature.instBEqSITrigger.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Implicature.instBEqSITrigger : BEq SITrigger

Equations

• Implicature.instBEqSITrigger = { beq := Implicature.instBEqSITrigger.beq }

instance Implicature.instReprSITrigger : Repr SITrigger

Equations

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

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

Equations

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

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 : Nat

  Predicted baseline SI rate in neutral context (percentage)

instance Implicature.instReprNeoGriceanParams : Repr NeoGriceanParams

Equations

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

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

Equations

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

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)