def NeoGricean.Competence.competencePlus (truth : Bool) (b : BeliefState) : Bool

Competence+: Speaker's belief matches truth.

This is stronger than basic competence:

• Basic: Bel_S(ψ) ∨ Bel_S(¬ψ) (speaker has an opinion)
• Plus: Bel_S(ψ) ↔ ψ (speaker's opinion is correct)

Competence+ entails basic competence, but not vice versa.

Equations

• NeoGricean.Competence.competencePlus true NeoGricean.BeliefState.belief = true
• NeoGricean.Competence.competencePlus false NeoGricean.BeliefState.disbelief = true
• NeoGricean.Competence.competencePlus truth b = false

theorem NeoGricean.Competence.competence_plus_implies_basic (truth : Bool) (b : BeliefState) : competencePlus truth b = true → competent b = true

Theorem: Competence+ Implies Basic Competence

If Competence+ holds, basic competence holds.

theorem NeoGricean.Competence.basic_not_implies_plus : ∃ (truth : Bool), ∃ (b : BeliefState), competent b = true ∧ competencePlus truth b = false

Theorem: Basic Competence Doesn't Imply Competence+

A speaker can be competent (have an opinion) but wrong.

structure NeoGricean.Competence.DisjunctionState : Type

Represents a disjunction "A or B" with speaker's epistemic state.

For disjunctions, the standard competence assumption leads to problems. If speaker is competent about A (knows whether A):

• Case 1: Bel_S(A) → but then why say "A or B"? (Quality violation)
• Case 2: Bel_S(¬A) → combined with "A or B" means Bel_S(B)

This explains why disjunction triggers IGNORANCE implicatures, not scalar implicatures.

• beliefA : BeliefState

  Speaker's belief about A

• beliefB : BeliefState

  Speaker's belief about B

def NeoGricean.Competence.instReprDisjunctionState.repr : DisjunctionState → Nat → Std.Format

Equations

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

instance NeoGricean.Competence.instReprDisjunctionState : Repr DisjunctionState

Equations

• NeoGricean.Competence.instReprDisjunctionState = { reprPrec := NeoGricean.Competence.instReprDisjunctionState.repr }

def NeoGricean.Competence.competentAboutBoth (d : DisjunctionState) : Bool

Check if the speaker is competent about both disjuncts.

Equations

• NeoGricean.Competence.competentAboutBoth d = (NeoGricean.competent d.beliefA && NeoGricean.competent d.beliefB)

def NeoGricean.Competence.qualityConsistent (d : DisjunctionState) : Bool

Check if saying "A or B" is consistent with Quality maxim.

Quality: Don't say what you believe to be false. If speaker believes A is true, saying "A or B" is misleading. If speaker believes B is true, saying "A or B" is misleading.

Equations

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

theorem NeoGricean.Competence.disjunction_blocks_full_competence (d : DisjunctionState) : competentAboutBoth d = true → qualityConsistent d = true → d.beliefA = BeliefState.disbelief ∧ d.beliefB = BeliefState.disbelief

Theorem: Competence About Both Disjuncts Violates Quality

If the speaker is competent about both A and B, and "A or B" is asserted, Quality is likely violated (speaker should have been more specific).

theorem NeoGricean.Competence.disjunction_implies_partial_ignorance (d : DisjunctionState) : qualityConsistent d = true → ¬(d.beliefA = BeliefState.belief ∧ d.beliefB = BeliefState.disbelief) ∧ ¬(d.beliefA = BeliefState.disbelief ∧ d.beliefB = BeliefState.belief) ∧ ¬(d.beliefA = BeliefState.belief ∧ d.beliefB = BeliefState.belief)

Theorem: Disjunction Suggests Ignorance

If "A or B" is asserted consistently with Quality, speaker lacks full competence about both disjuncts.

Specifically: speaker doesn't believe exactly one disjunct is true.

structure NeoGricean.Competence.ImplicatureProcessing : Type

Detailed outcome of implicature processing, including the reason.

• 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

instance NeoGricean.Competence.instReprImplicatureProcessing : Repr ImplicatureProcessing

Equations

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

def NeoGricean.Competence.instReprImplicatureProcessing.repr : ImplicatureProcessing → Nat → Std.Format

Equations

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

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

Process an alternative given competence assumption.

Equations

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

theorem NeoGricean.Competence.outcome_i_undecided (b : BeliefState) : b ≠ BeliefState.belief → have p := processAlternative false b; p.weakHolds = true ∧ p.strongDerived = false

Theorem: Outcome i (Undecided)

When competence is not assumed, only weak implicature holds.

theorem NeoGricean.Competence.outcome_ii_strong : have p := processAlternative true BeliefState.disbelief; p.weakHolds = true ∧ p.competenceAssumed = true ∧ p.strongDerived = true

Theorem: Outcome ii (Strong)

When competence is assumed and speaker disbelieves, strong implicature is derived.

theorem NeoGricean.Competence.outcome_iii_incompetent : have p := processAlternative true BeliefState.noOpinion; p.weakHolds = true ∧ p.competenceAssumed = false ∧ p.strongDerived = false

Theorem: Outcome iii (Incompetent)

When speaker has no opinion, competence assumption fails, only weak implicature holds.

inductive NeoGricean.Competence.CompetenceContext : Type

Factors that affect whether competence is assumed.

Following Geurts' discussion, competence is more likely assumed when:

• The proposition is simple/common knowledge
• The speaker is an authority on the topic
• Context suggests speaker should know

Competence is blocked for disjunctions due to Quality interaction.

• simpleAssertion : CompetenceContext
• disjunction : CompetenceContext
• authority : CompetenceContext
• uncertain : CompetenceContext

instance NeoGricean.Competence.instDecidableEqCompetenceContext : DecidableEq CompetenceContext

Equations

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

instance NeoGricean.Competence.instBEqCompetenceContext : BEq CompetenceContext

Equations

• NeoGricean.Competence.instBEqCompetenceContext = { beq := NeoGricean.Competence.instBEqCompetenceContext.beq }

def NeoGricean.Competence.instBEqCompetenceContext.beq : CompetenceContext → CompetenceContext → Bool

Equations

• NeoGricean.Competence.instBEqCompetenceContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def NeoGricean.Competence.instReprCompetenceContext.repr : CompetenceContext → Nat → Std.Format

Equations

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

instance NeoGricean.Competence.instReprCompetenceContext : Repr CompetenceContext

Equations

• NeoGricean.Competence.instReprCompetenceContext = { reprPrec := NeoGricean.Competence.instReprCompetenceContext.repr }

def NeoGricean.Competence.shouldAssumeCompetence : CompetenceContext → Bool

Should competence be assumed in this context?

Equations

• NeoGricean.Competence.shouldAssumeCompetence NeoGricean.Competence.CompetenceContext.simpleAssertion = true
• NeoGricean.Competence.shouldAssumeCompetence NeoGricean.Competence.CompetenceContext.disjunction = false
• NeoGricean.Competence.shouldAssumeCompetence NeoGricean.Competence.CompetenceContext.authority = true
• NeoGricean.Competence.shouldAssumeCompetence NeoGricean.Competence.CompetenceContext.uncertain = false

theorem NeoGricean.Competence.disjunction_context_weak_only : shouldAssumeCompetence CompetenceContext.disjunction = false

Theorem: Disjunction Context Blocks Competence

In disjunction context, we don't assume competence, so only weak implicatures (ignorance) arise.