structure NeoGricean.ScalarImplicatures.ImplicatureDerivation : Type

A scalar implicature derivation attempt.

Records whether the implicature arises and why/why not.

• term : String

  The scalar term used

• alternative : String

  The potential stronger alternative

• polarity : Core.NaturalLogic.ContextPolarity

  The context polarity

• alternativeIsStronger : Bool

  Does the alternative count as stronger in this context?

• implicatureArises : Bool

  Does the implicature arise?

def NeoGricean.ScalarImplicatures.instReprImplicatureDerivation.repr : ImplicatureDerivation → ℕ → Std.Format

Equations

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

instance NeoGricean.ScalarImplicatures.instReprImplicatureDerivation : Repr ImplicatureDerivation

Equations

• NeoGricean.ScalarImplicatures.instReprImplicatureDerivation = { reprPrec := NeoGricean.ScalarImplicatures.instReprImplicatureDerivation.repr }

def NeoGricean.ScalarImplicatures.deriveImplicature (term alternative : String) (ctx : Alternatives.SentenceContext) (checker : Alternatives.EntailmentChecker String) : ImplicatureDerivation

Attempt to derive a scalar implicature.

Equations

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

def NeoGricean.ScalarImplicatures.someNotAll_UE : ImplicatureDerivation

Example: "some" → "not all" in UE context

Equations

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

def NeoGricean.ScalarImplicatures.someNotAll_DE : ImplicatureDerivation

Example: "some" → "not all" blocked in DE context

Equations

• NeoGricean.ScalarImplicatures.someNotAll_DE = NeoGricean.ScalarImplicatures.deriveImplicature "some" "all" NeoGricean.Alternatives.underNegation NeoGricean.Alternatives.quantifierCheckerString

theorem NeoGricean.ScalarImplicatures.de_blocks_some_not_all : someNotAll_UE.implicatureArises = true ∧ someNotAll_DE.implicatureArises = false

Theorem: DE Blocks "Some → Not All"

In UE context, the implicature arises. In DE context, the implicature is blocked.

def NeoGricean.ScalarImplicatures.allNotSome_DE : ImplicatureDerivation

Theorem: In DE, "All" Has Implicatures

In DE context, "all" can implicate "not some" (reversed!).

Equations

• NeoGricean.ScalarImplicatures.allNotSome_DE = NeoGricean.ScalarImplicatures.deriveImplicature "all" "some" NeoGricean.Alternatives.underNegation NeoGricean.Alternatives.quantifierCheckerString

theorem NeoGricean.ScalarImplicatures.de_all_has_implicature : allNotSome_DE.implicatureArises = true

inductive NeoGricean.ScalarImplicatures.DisjunctionInference : Type

Two types of inferences from disjunction.

1. Exclusivity (scalar): "A or B" → "not (A and B)" Derived from Horn set ⟨or, and⟩.

2. Ignorance (non-scalar): "A or B" → "speaker doesn't know which" Derived from competence failure for individual disjuncts.

• exclusivity : DisjunctionInference
• ignorance : DisjunctionInference

instance NeoGricean.ScalarImplicatures.instDecidableEqDisjunctionInference : DecidableEq DisjunctionInference

Equations

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

instance NeoGricean.ScalarImplicatures.instBEqDisjunctionInference : BEq DisjunctionInference

Equations

• NeoGricean.ScalarImplicatures.instBEqDisjunctionInference = { beq := NeoGricean.ScalarImplicatures.instBEqDisjunctionInference.beq }

def NeoGricean.ScalarImplicatures.instBEqDisjunctionInference.beq : DisjunctionInference → DisjunctionInference → Bool

Equations

• NeoGricean.ScalarImplicatures.instBEqDisjunctionInference.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.ScalarImplicatures.instReprDisjunctionInference : Repr DisjunctionInference

Equations

• NeoGricean.ScalarImplicatures.instReprDisjunctionInference = { reprPrec := NeoGricean.ScalarImplicatures.instReprDisjunctionInference.repr }

def NeoGricean.ScalarImplicatures.instReprDisjunctionInference.repr : DisjunctionInference → ℕ → Std.Format

Equations

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

structure NeoGricean.ScalarImplicatures.DisjunctionAnalysis : Type

Result of analyzing a disjunctive utterance.

• statement : String

  The disjunctive statement

• exclusivityArises : Bool

  Does exclusivity implicature arise?

• ignoranceArises : Bool

  Does ignorance implicature arise?

• compatible : Bool

  Can both arise together?

def NeoGricean.ScalarImplicatures.instReprDisjunctionAnalysis.repr : DisjunctionAnalysis → ℕ → Std.Format

Equations

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

instance NeoGricean.ScalarImplicatures.instReprDisjunctionAnalysis : Repr DisjunctionAnalysis

Equations

• NeoGricean.ScalarImplicatures.instReprDisjunctionAnalysis = { reprPrec := NeoGricean.ScalarImplicatures.instReprDisjunctionAnalysis.repr }

def NeoGricean.ScalarImplicatures.analyzeDisjunction (ctx : Alternatives.SentenceContext) : DisjunctionAnalysis

Analyze a simple disjunction in UE context.

Both exclusivity AND ignorance can arise together.

Equations

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

theorem NeoGricean.ScalarImplicatures.disjunction_exclusivity_ue : (analyzeDisjunction Alternatives.simpleAssertion).exclusivityArises = true

Theorem: Disjunction in UE Has Exclusivity

theorem NeoGricean.ScalarImplicatures.exclusivity_ignorance_compatible : (analyzeDisjunction Alternatives.simpleAssertion).compatible = true

Theorem: Both Inferences Are Compatible

"A or B" can simultaneously implicate:

• "not both" (exclusivity)
• "speaker doesn't know which" (ignorance)

structure NeoGricean.ScalarImplicatures.LongDisjunction : Type

The long disjunction problem (Geurts p.61-64).

For "A or B or C", the alternatives are not just {A, B, C}. We need ALL conjunctive closures:

• Core: A, B, C
• Binary: A∧B, A∧C, B∧C
• Full: A∧B∧C

The substitution method (replacing "or" with "and") fails to generate all necessary alternatives for n > 2.

• disjuncts : List String

  The disjuncts

• coreAlternatives : List String

  Core alternatives (individual disjuncts)

• derivedAlternatives : List String

  Derived alternatives (conjunctions)

def NeoGricean.ScalarImplicatures.instReprLongDisjunction.repr : LongDisjunction → ℕ → Std.Format

Equations

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

instance NeoGricean.ScalarImplicatures.instReprLongDisjunction : Repr LongDisjunction

Equations

• NeoGricean.ScalarImplicatures.instReprLongDisjunction = { reprPrec := NeoGricean.ScalarImplicatures.instReprLongDisjunction.repr }

def NeoGricean.ScalarImplicatures.binaryConjunctions (terms : List String) : List String

Generate all binary conjunctions from a list.

Equations

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

def NeoGricean.ScalarImplicatures.fullConjunction (terms : List String) : String

Generate the full conjunction of all terms.

Equations

• NeoGricean.ScalarImplicatures.fullConjunction terms = "∧".intercalate terms

def NeoGricean.ScalarImplicatures.analyzeLongDisjunction (disjuncts : List String) : LongDisjunction

Analyze a long disjunction, computing all alternatives.

Equations

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

def NeoGricean.ScalarImplicatures.threeWayExample : LongDisjunction

Example: Three-way disjunction

"A or B or C" has alternatives:

• Core: A, B, C
• Derived: A∧B, A∧C, B∧C, A∧B∧C

Equations

• NeoGricean.ScalarImplicatures.threeWayExample = NeoGricean.ScalarImplicatures.analyzeLongDisjunction ["A", "B", "C"]

theorem NeoGricean.ScalarImplicatures.three_way_core : threeWayExample.coreAlternatives.length = 3

Theorem: Three-way disjunction has 3 core alternatives

theorem NeoGricean.ScalarImplicatures.three_way_derived : threeWayExample.derivedAlternatives.length = 4

Theorem: Three-way disjunction has 4 derived alternatives

The 4 derived alternatives are: A∧B, A∧C, B∧C, A∧B∧C

theorem NeoGricean.ScalarImplicatures.three_way_total : threeWayExample.coreAlternatives.length.add threeWayExample.derivedAlternatives.length = 7

Theorem: Total alternatives for 3-way = 7

Core (3) + Derived (4) = 7 alternatives

def NeoGricean.ScalarImplicatures.substitutionAlternative (disjuncts : List String) : String

The simple substitution method: replace "or" with "and".

For "A or B": substitute to get "A and B" ✓ For "A or B or C": substitute to get "A and B and C" ✓ But MISSES: "A and B", "A and C", "B and C" ✗

This is why we need closure under conjunction.

Equations

• NeoGricean.ScalarImplicatures.substitutionAlternative disjuncts = NeoGricean.ScalarImplicatures.fullConjunction disjuncts

structure NeoGricean.ScalarImplicatures.SubstitutionComparison : Type

What substitution method produces vs what's needed.

• n : ℕ

  Number of disjuncts

• substitutionResult : ℕ

  What substitution gives

• neededAlternatives : ℕ

  What's actually needed

• substitutionSuffices : Bool

  Does substitution suffice?

instance NeoGricean.ScalarImplicatures.instReprSubstitutionComparison : Repr SubstitutionComparison

Equations

• NeoGricean.ScalarImplicatures.instReprSubstitutionComparison = { reprPrec := NeoGricean.ScalarImplicatures.instReprSubstitutionComparison.repr }

def NeoGricean.ScalarImplicatures.instReprSubstitutionComparison.repr : SubstitutionComparison → ℕ → Std.Format

Equations

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

def NeoGricean.ScalarImplicatures.compareSubstitution (n : ℕ) : SubstitutionComparison

Compare substitution method to full closure.

Equations

• NeoGricean.ScalarImplicatures.compareSubstitution n = { n := n, substitutionResult := 1, neededAlternatives := 2 ^ n - n - 1, substitutionSuffices := 2 ^ n - n - 1 == 1 }

theorem NeoGricean.ScalarImplicatures.substitution_works_n2 : (compareSubstitution 2).substitutionSuffices = true

Theorem: Substitution Works for n=2

For "A or B", substitution gives "A and B" which is the only alternative.

theorem NeoGricean.ScalarImplicatures.substitution_fails_n3 : (compareSubstitution 3).substitutionSuffices = false ∧ (compareSubstitution 3).neededAlternatives = 4

Theorem: Substitution Fails for n=3

For "A or B or C", substitution gives 1 alternative but we need 4 (A∧B, A∧C, B∧C, A∧B∧C).

structure NeoGricean.ScalarImplicatures.ScalarImplicatureResult : Type

Complete scalar implicature derivation result.

• term : String

  The original utterance's scalar term

• hornSet : Alternatives.HornSet String

  The Horn set used

• context : Alternatives.SentenceContext

  The context

• strongerAlts : List String

  Stronger alternatives found

• implicatures : List String

  Implicatures derived (negations of stronger alternatives)

def NeoGricean.ScalarImplicatures.instReprScalarImplicatureResult.repr : ScalarImplicatureResult → ℕ → Std.Format

Equations

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

instance NeoGricean.ScalarImplicatures.instReprScalarImplicatureResult : Repr ScalarImplicatureResult

Equations

• NeoGricean.ScalarImplicatures.instReprScalarImplicatureResult = { reprPrec := NeoGricean.ScalarImplicatures.instReprScalarImplicatureResult.repr }

def NeoGricean.ScalarImplicatures.deriveScalarImplicatures (term : String) (hornSet : Alternatives.HornSet String) (checker : Alternatives.EntailmentChecker String) (context : Alternatives.SentenceContext) : ScalarImplicatureResult

Derive all scalar implicatures for a term.

Equations

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

def NeoGricean.ScalarImplicatures.someUE : ScalarImplicatureResult

Example: Complete derivation for "some" in UE context

Equations

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

theorem NeoGricean.ScalarImplicatures.some_ue_implicatures : someUE.implicatures = ["not(most)", "not(all)"]

Theorem: "some" in UE derives "not(most)" and "not(all)"

def NeoGricean.ScalarImplicatures.someDE : ScalarImplicatureResult

Example: Complete derivation for "some" in DE context

Equations

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

theorem NeoGricean.ScalarImplicatures.some_de_no_implicatures : someDE.implicatures = []

Theorem: "some" in DE derives NO implicatures

def NeoGricean.ScalarImplicatures.getScaleInfo (sm : Semantics.Montague.ScaleMembership) : Alternatives.HornSet String × Alternatives.EntailmentChecker String

Map scale membership to the appropriate HornSet and EntailmentChecker.

Uses string-based versions for interface with SemDeriv, but these are backed by type-safe implementations grounded in Core.Scale.

Equations

• NeoGricean.ScalarImplicatures.getScaleInfo (Semantics.Montague.ScaleMembership.quantifier pos) = (NeoGricean.Alternatives.quantifierSetString, NeoGricean.Alternatives.quantifierCheckerString)
• NeoGricean.ScalarImplicatures.getScaleInfo (Semantics.Montague.ScaleMembership.connective pos) = (NeoGricean.Alternatives.connectiveSetString, NeoGricean.Alternatives.connectiveCheckerString)
• NeoGricean.ScalarImplicatures.getScaleInfo (Semantics.Montague.ScaleMembership.modal pos) = (NeoGricean.Alternatives.connectiveSetString, NeoGricean.Alternatives.connectiveCheckerString)

def NeoGricean.ScalarImplicatures.toSentenceContext (ctx : Core.NaturalLogic.ContextPolarity) : Alternatives.SentenceContext

Create a SentenceContext from a ContextPolarity.

Equations

• One or more equations did not get rendered due to their size.
• NeoGricean.ScalarImplicatures.toSentenceContext Core.NaturalLogic.ContextPolarity.upward = { polarity := Core.NaturalLogic.ContextPolarity.upward, description := "Upward-entailing context" }
• NeoGricean.ScalarImplicatures.toSentenceContext Core.NaturalLogic.ContextPolarity.downward = { polarity := Core.NaturalLogic.ContextPolarity.downward, description := "Downward-entailing context" }

def NeoGricean.ScalarImplicatures.deriveFromDerivation {m : Semantics.Montague.Model} (d : Semantics.Montague.Derivation.Derivation m) (ctx : Core.NaturalLogic.ContextPolarity) : List ScalarImplicatureResult

Derive scalar implicatures from a semantic derivation.

This is the key function that connects syntax to pragmatics:

1. Takes a SemDeriv.Derivation (produced by any syntax theory)
2. Extracts scalar items from the derivation
3. For each scalar item, derives implicatures based on its scale
4. Returns all derived implicatures

Syntax-agnostic: Works with CCG, HPSG, Minimalism, or any theory that implements the SemDeriv interface.

Equations

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

def NeoGricean.ScalarImplicatures.hasImplicature (results : List ScalarImplicatureResult) (alt : String) : Bool

Check if any implicature in the results negates a given alternative.

Equations

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

def NeoGricean.ScalarImplicatures.someStudentsSleep_result : List ScalarImplicatureResult

Example: "some students sleep" via CCG

Using the CCG derivation from CCG/Interpret.lean:

Equations

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

theorem NeoGricean.ScalarImplicatures.some_students_derives_not_all : hasImplicature someStudentsSleep_result "all" = true

Theorem: "some students sleep" derives "not(all)"

This is the key milestone theorem: starting from a semantic derivation (which could come from CCG), NeoGricean pragmatics derives "not all".

theorem NeoGricean.ScalarImplicatures.some_students_derives_not_most : hasImplicature someStudentsSleep_result "most" = true

Theorem: "some students sleep" derives "not(most)" as well

def NeoGricean.ScalarImplicatures.everyStudentsSleeps_result : List ScalarImplicatureResult

Example: "every student sleeps" in UE

"every" is at the top of the quantifier scale, so no stronger alternatives.

Equations

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

theorem NeoGricean.ScalarImplicatures.every_students_no_implicatures : (everyStudentsSleeps_result.all fun (x : ScalarImplicatureResult) => x.implicatures.isEmpty) = true

Theorem: "every student sleeps" has no implicatures

Since "every/all" is the strongest quantifier, there are no stronger alternatives to negate.

def NeoGricean.ScalarImplicatures.someStudentsSleep_DE_result : List ScalarImplicatureResult

Example: "some students sleep" in DE context

In a downward-entailing context (e.g., "No one thinks some students sleep"), the "not all" implicature is blocked.

Equations

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

theorem NeoGricean.ScalarImplicatures.some_students_de_no_not_all : hasImplicature someStudentsSleep_DE_result "all" = false

Theorem: "some" in DE has no "not all" implicature

Downward-entailing contexts block the standard scalar implicature.

theorem NeoGricean.ScalarImplicatures.defaultism_predicts_high_rate : predictsHighNeutralRate levinsonParams = true

Derived: Defaultism predicts high neutral rate

theorem NeoGricean.ScalarImplicatures.contextualism_predicts_moderate_rate : predictsHighNeutralRate geurtsParams = false

Derived: Contextualism predicts moderate neutral rate

theorem NeoGricean.ScalarImplicatures.only_contextualism_predicts_task_effect : predictsTaskEffect levinsonParams = false ∧ predictsTaskEffect geurtsParams = true

Derived: Only contextualism predicts task effect

theorem NeoGricean.ScalarImplicatures.variants_make_different_predictions : levinsonParams.predictedNeutralRate ≠ geurtsParams.predictedNeutralRate ∧ predictsTaskEffect levinsonParams ≠ predictsTaskEffect geurtsParams

Derived: The two variants make different predictions

This is what makes them empirically distinguishable.

structure NeoGricean.ScalarImplicatures.HornScale (World : Type u_1) : Type u_1

A Horn scale with semantic content.

The key property: stronger entails weaker but not vice versa. This asymmetry drives scalar implicatures via exhaustification.

• name : String

  Name of the scale

• weakerTerm : String

  The weaker scalar term (e.g., "some")

• strongerTerm : String

  The stronger scalar term (e.g., "all")

• weaker : Prop' World

  Semantic denotation of weaker term

• stronger : Prop' World

  Semantic denotation of stronger term

• entailment : self.stronger ⊆ₚ self.weaker

  Stronger entails weaker

• nonTrivial : ¬self.weaker ⊆ₚ self.stronger

  Weaker does not entail stronger (non-trivial scale)

def NeoGricean.ScalarImplicatures.HornScale.alts {World : Type u_1} (s : HornScale World) : Set (Prop' World)

Alternative set for a Horn scale: {weaker, stronger}.

Equations

• s.alts = {s.weaker, s.stronger}

structure NeoGricean.ScalarImplicatures.HurfordSemantic (World : Type u_1) : Type u_1

Semantic structure for a Hurford configuration. Allows proving when exhaustification rescues the violation.

• disjunctA : Prop' World

  First disjunct meaning

• disjunctB : Prop' World

  Second disjunct meaning

• entailment : (self.disjunctA ⊆ₚ self.disjunctB) ∨ self.disjunctB ⊆ₚ self.disjunctA

  The entailment that creates the violation

• alts : Set (Prop' World)

  Alternative set for exhaustification

def NeoGricean.ScalarImplicatures.HurfordSemantic.isRescued {World : Type u_1} (h : HurfordSemantic World) : Prop

A Hurford violation is rescued iff after exhaustifying the weaker disjunct, the entailment no longer holds.

Since the structure tracks that either A⊆B or B⊆A, rescue means exhaustification breaks whichever entailment held.

Equations

• h.isRescued = ((¬NeoGricean.Exhaustivity.exhIE h.alts h.disjunctA ⊆ₚ h.disjunctB) ∨ ¬NeoGricean.Exhaustivity.exhIE h.alts h.disjunctB ⊆ₚ h.disjunctA)

def NeoGricean.ScalarImplicatures.HurfordSemantic.isRescuedFromBA {World : Type u_1} (h : HurfordSemantic World) : Prop

For cases where B⊆A (stronger entails weaker), rescue requires exh(B) ⊄ A.

This is the relevant check when the original entailment goes from B to A.

Equations

• h.isRescuedFromBA = ¬NeoGricean.Exhaustivity.exhIE h.alts h.disjunctB ⊆ₚ h.disjunctA

structure NeoGricean.ScalarImplicatures.SinghSemantic (World : Type u_1) : Type u_1

Semantic structure for Singh configurations.

• weaker : Prop' World

  Weaker disjunct meaning

• stronger : Prop' World

  Stronger disjunct meaning

• entailment : self.stronger ⊆ₚ self.weaker

  Stronger entails weaker

• alts : Set (Prop' World)

  Alternative set

• weakerFirst : Bool

  Is weaker mentioned first?

def NeoGricean.ScalarImplicatures.SinghSemantic.exhBreaksEntailment {World : Type u_1} (s : SinghSemantic World) : Prop

Fox & Spector's prediction: weak-first is felicitous because exh(weak) can break the entailment to strong.

Equations

• s.exhBreaksEntailment = ¬NeoGricean.Exhaustivity.exhIE s.alts s.weaker ⊆ₚ s.stronger

def NeoGricean.ScalarImplicatures.SinghSemantic.predictedFelicitous {World : Type u_1} (s : SinghSemantic World) : Prop

The asymmetry: felicitous iff (weak-first AND exh breaks entailment). Strong-first can't be rescued because exh(strong) is vacuous.

Equations

• s.predictedFelicitous = (s.weakerFirst = true ∧ s.exhBreaksEntailment)

@[reducible, inline]

abbrev NeoGricean.ScalarImplicatures.QuantWorld : Type

Worlds for quantifier scale: number satisfying predicate (0 to 3).

Equations

• NeoGricean.ScalarImplicatures.QuantWorld = Fin 4

def NeoGricean.ScalarImplicatures.someQ : Prop' QuantWorld

"Some Ps are Q" = at least one.

Equations

• NeoGricean.ScalarImplicatures.someQ w = (↑w ≥ 1)

def NeoGricean.ScalarImplicatures.allQ : Prop' QuantWorld

"All Ps are Q" = all three.

Equations

• NeoGricean.ScalarImplicatures.allQ w = (↑w = 3)

theorem NeoGricean.ScalarImplicatures.all_entails_some : allQ ⊆ₚ someQ

All entails some.

theorem NeoGricean.ScalarImplicatures.some_not_entails_all : ¬someQ ⊆ₚ allQ

Some does not entail all.

def NeoGricean.ScalarImplicatures.someAllScale : HornScale QuantWorld

The some/all Horn scale with semantic content.

Equations

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

inductive NeoGricean.ScalarImplicatures.ConnWorld : Type

Worlds for connective scale.

• neither : ConnWorld
• onlyA : ConnWorld
• onlyB : ConnWorld
• both : ConnWorld

instance NeoGricean.ScalarImplicatures.instDecidableEqConnWorld : DecidableEq ConnWorld

Equations

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

def NeoGricean.ScalarImplicatures.instReprConnWorld.repr : ConnWorld → ℕ → Std.Format

Equations

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

instance NeoGricean.ScalarImplicatures.instReprConnWorld : Repr ConnWorld

Equations

• NeoGricean.ScalarImplicatures.instReprConnWorld = { reprPrec := NeoGricean.ScalarImplicatures.instReprConnWorld.repr }

def NeoGricean.ScalarImplicatures.orConn : Prop' ConnWorld

"A or B" (inclusive).

Equations

• NeoGricean.ScalarImplicatures.orConn NeoGricean.ScalarImplicatures.ConnWorld.neither = False
• NeoGricean.ScalarImplicatures.orConn NeoGricean.ScalarImplicatures.ConnWorld.onlyA = True
• NeoGricean.ScalarImplicatures.orConn NeoGricean.ScalarImplicatures.ConnWorld.onlyB = True
• NeoGricean.ScalarImplicatures.orConn NeoGricean.ScalarImplicatures.ConnWorld.both = True

def NeoGricean.ScalarImplicatures.andConn : Prop' ConnWorld

"A and B".

Equations

• NeoGricean.ScalarImplicatures.andConn NeoGricean.ScalarImplicatures.ConnWorld.neither = False
• NeoGricean.ScalarImplicatures.andConn NeoGricean.ScalarImplicatures.ConnWorld.onlyA = False
• NeoGricean.ScalarImplicatures.andConn NeoGricean.ScalarImplicatures.ConnWorld.onlyB = False
• NeoGricean.ScalarImplicatures.andConn NeoGricean.ScalarImplicatures.ConnWorld.both = True

theorem NeoGricean.ScalarImplicatures.and_entails_or : andConn ⊆ₚ orConn

And entails or.

theorem NeoGricean.ScalarImplicatures.or_not_entails_and : ¬orConn ⊆ₚ andConn

Or does not entail and.

def NeoGricean.ScalarImplicatures.orAndScale : HornScale ConnWorld

The or/and Horn scale with semantic content.

Equations

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

inductive NeoGricean.ScalarImplicatures.ModalWorld : Type

Worlds for modal scale: accessibility relation outcomes.

• none : ModalWorld
• some : ModalWorld
• all : ModalWorld

instance NeoGricean.ScalarImplicatures.instDecidableEqModalWorld : DecidableEq ModalWorld

Equations

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

instance NeoGricean.ScalarImplicatures.instReprModalWorld : Repr ModalWorld

Equations

• NeoGricean.ScalarImplicatures.instReprModalWorld = { reprPrec := NeoGricean.ScalarImplicatures.instReprModalWorld.repr }

def NeoGricean.ScalarImplicatures.instReprModalWorld.repr : ModalWorld → ℕ → Std.Format

Equations

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

def NeoGricean.ScalarImplicatures.possibleP : Prop' ModalWorld

"Possibly P" = at least one accessible world has P.

Equations

• NeoGricean.ScalarImplicatures.possibleP NeoGricean.ScalarImplicatures.ModalWorld.none = False
• NeoGricean.ScalarImplicatures.possibleP NeoGricean.ScalarImplicatures.ModalWorld.some = True
• NeoGricean.ScalarImplicatures.possibleP NeoGricean.ScalarImplicatures.ModalWorld.all = True

def NeoGricean.ScalarImplicatures.necessaryP : Prop' ModalWorld

"Necessarily P" = all accessible worlds have P.

Equations

• NeoGricean.ScalarImplicatures.necessaryP NeoGricean.ScalarImplicatures.ModalWorld.none = False
• NeoGricean.ScalarImplicatures.necessaryP NeoGricean.ScalarImplicatures.ModalWorld.some = False
• NeoGricean.ScalarImplicatures.necessaryP NeoGricean.ScalarImplicatures.ModalWorld.all = True

theorem NeoGricean.ScalarImplicatures.necessary_entails_possible : necessaryP ⊆ₚ possibleP

Necessary entails possible.

theorem NeoGricean.ScalarImplicatures.possible_not_entails_necessary : ¬possibleP ⊆ₚ necessaryP

Possible does not entail necessary.

def NeoGricean.ScalarImplicatures.possibleNecessaryScale : HornScale ModalWorld

The possible/necessary Horn scale.

Equations

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

theorem NeoGricean.ScalarImplicatures.someAll_implicature (w : QuantWorld) : Exhaustivity.exhIE someAllScale.alts someQ w → ¬allQ w

Prediction: exh(some) → ¬all.

At any world where exhIE(some) holds, "all" is false. This derives the implicature "some → not all".

theorem NeoGricean.ScalarImplicatures.orAnd_implicature (w : ConnWorld) : Exhaustivity.exhIE orAndScale.alts orConn w → ¬andConn w

Prediction: exh(or) → ¬and.

At any world where exhIE(or) holds, "and" is false. This derives the implicature "or → not both".

theorem NeoGricean.ScalarImplicatures.possibleNecessary_implicature (w : ModalWorld) : Exhaustivity.exhIE possibleNecessaryScale.alts possibleP w → ¬necessaryP w

Prediction: exh(possible) → ¬necessary.

def NeoGricean.ScalarImplicatures.someOrAll_semantic : HurfordSemantic QuantWorld

Semantic structure for "some or all" (rescued Hurford case).

Equations

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

theorem NeoGricean.ScalarImplicatures.someOrAll_is_rescued : someOrAll_semantic.isRescued

Prediction: "some or all" is rescued because exh(some) doesn't entail all.

inductive NeoGricean.ScalarImplicatures.HyponymWorld : Type

World type for hyponymy: 3 regions of people

• notAmerican : HyponymWorld
• americanOnly : HyponymWorld
• californian : HyponymWorld

instance NeoGricean.ScalarImplicatures.instDecidableEqHyponymWorld : DecidableEq HyponymWorld

Equations

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

def NeoGricean.ScalarImplicatures.instReprHyponymWorld.repr : HyponymWorld → ℕ → Std.Format

Equations

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

instance NeoGricean.ScalarImplicatures.instReprHyponymWorld : Repr HyponymWorld

Equations

• NeoGricean.ScalarImplicatures.instReprHyponymWorld = { reprPrec := NeoGricean.ScalarImplicatures.instReprHyponymWorld.repr }

def NeoGricean.ScalarImplicatures.americanP : Prop' HyponymWorld

"American" predicate

Equations

• NeoGricean.ScalarImplicatures.americanP NeoGricean.ScalarImplicatures.HyponymWorld.notAmerican = False
• NeoGricean.ScalarImplicatures.americanP NeoGricean.ScalarImplicatures.HyponymWorld.americanOnly = True
• NeoGricean.ScalarImplicatures.americanP NeoGricean.ScalarImplicatures.HyponymWorld.californian = True

def NeoGricean.ScalarImplicatures.californianP : Prop' HyponymWorld

"Californian" predicate

Equations

• NeoGricean.ScalarImplicatures.californianP NeoGricean.ScalarImplicatures.HyponymWorld.californian = True
• NeoGricean.ScalarImplicatures.californianP w = False

theorem NeoGricean.ScalarImplicatures.californian_entails_american : californianP ⊆ₚ americanP

Californian entails American (hyponymy)

def NeoGricean.ScalarImplicatures.americanCalifornian_semantic : HurfordSemantic HyponymWorld

Semantic structure for "American or Californian" (true Hurford violation).

Key: The alternative set contains NO scalar alternatives beyond the disjuncts. Hyponymy is a fixed lexical relation, not a scalar implicature.

Equations

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

theorem NeoGricean.ScalarImplicatures.exh_californian_entails_american : Exhaustivity.exhIE americanCalifornian_semantic.alts californianP ⊆ₚ americanP

Key Lemma: With no scalar alternatives, exh is vacuous.

exhIE {A, B} B = B when B is the strongest in the set. Since californianP ⊆ americanP, californianP has no proper stronger alternative.

The proof shows that exh(californianP) still entails americanP because:

1. The only alternatives are {americanP, californianP}
2. californianP is already the strongest term (it entails americanP)
3. So exh(californianP) = californianP (no strengthening possible)
4. And californianP ⊆ americanP remains

theorem NeoGricean.ScalarImplicatures.americanCalifornian_not_rescued : ¬americanCalifornian_semantic.isRescuedFromBA

Prediction: "American or Californian" is not rescued.

Since exh(californianP) ⊆ americanP (the ORIGINAL entailment is preserved), the disjunction remains redundant → infelicitous.

For hyponymy cases like this, the entailment is B⊆A (californian ⊆ american), so we use isRescuedFromBA which checks whether exh(B) ⊄ A.

def NeoGricean.ScalarImplicatures.orThenBoth_semantic : SinghSemantic ConnWorld

Semantic structure for "A or B, or both" (weak-first Singh case).

Equations

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

def NeoGricean.ScalarImplicatures.bothThenOr_semantic : SinghSemantic ConnWorld

Semantic structure for "both, or A or B" (strong-first Singh case).

Equations

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

theorem NeoGricean.ScalarImplicatures.orAnd_exh_breaks_entailment : ¬Exhaustivity.exhIE {orConn, andConn} orConn ⊆ₚ andConn

Prediction: exh(or) breaks entailment to and.

theorem NeoGricean.ScalarImplicatures.orThenBoth_predicted_felicitous : orThenBoth_semantic.predictedFelicitous

Prediction: "A or B, or both" (weak-first) is predicted felicitous.

theorem NeoGricean.ScalarImplicatures.bothThenOr_not_predicted_felicitous : ¬bothThenOr_semantic.predictedFelicitous

Prediction: "both, or A or B" (strong-first) is not predicted felicitous.

Even though exh breaks entailment, strong-first fails because exh(strong) is vacuous (nothing to exclude).

theorem NeoGricean.ScalarImplicatures.all_scale_implicatures_derived : (∀ (w : QuantWorld), Exhaustivity.exhIE someAllScale.alts someQ w → ¬allQ w) ∧ (∀ (w : ConnWorld), Exhaustivity.exhIE orAndScale.alts orConn w → ¬andConn w) ∧ ∀ (w : ModalWorld), Exhaustivity.exhIE possibleNecessaryScale.alts possibleP w → ¬necessaryP w

Main Result: Theory correctly predicts all three Horn scale implicatures.

For each scale, exh(weaker) → ¬stronger.

theorem NeoGricean.ScalarImplicatures.singh_asymmetry_derived : orThenBoth_semantic.predictedFelicitous ∧ ¬bothThenOr_semantic.predictedFelicitous

Main Result: Theory correctly predicts Singh asymmetry.

Weak-first is felicitous, strong-first is not.

structure NeoGricean.NeoGriceanTheory : Type

Marker type for the NeoGricean theory

structure NeoGricean.NeoGriceanStructure : Type

NeoGricean'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 NeoGricean (for baseline rate)

instance NeoGricean.instReprNeoGriceanStructure : Repr NeoGriceanStructure

Equations

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

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

Equations

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

def NeoGricean.isScalarQuantifierWord (w : Word) : Bool

Check if a word is a scalar quantifier

Equations

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

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

Find the position of a scalar item in a word list

Equations

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

def NeoGricean.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 NeoGricean.parseToNeoGricean (ws : List Word) : Option NeoGriceanStructure

Parse words into NeoGricean 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.

instance NeoGricean.instImplicatureTheoryNeoGriceanTheory : Interfaces.ImplicatureTheory NeoGriceanTheory

Equations

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

theorem NeoGricean.neogricean_predicts_de_blocking : Interfaces.ImplicatureTheory.predictsDEBlocking NeoGriceanTheory = true

NeoGricean predicts DE blocking

theorem NeoGricean.neogricean_predicts_task_effect : Interfaces.ImplicatureTheory.predictsTaskEffect NeoGriceanTheory = true

NeoGricean predicts task effect (under contextualism)

theorem NeoGricean.neogricean_baseline_rate : Interfaces.ImplicatureTheory.predictedBaselineRate NeoGriceanTheory = 35

NeoGricean baseline rate is 35% (Geurts contextualism)

def NeoGricean.someStudentsSleepNG : NeoGriceanStructure

Example: "some students sleep" in UE context

Equations

• NeoGricean.someStudentsSleepNG = { result := NeoGricean.applyStandardRecipe NeoGricean.BeliefState.disbelief, polarity := Core.NaturalLogic.ContextPolarity.upward, scalarPosition := some 0 }

def NeoGricean.someStudentsSleepDE : NeoGriceanStructure

Example: "some students sleep" in DE context (under negation)

Equations

• NeoGricean.someStudentsSleepDE = { result := NeoGricean.applyStandardRecipe NeoGricean.BeliefState.noOpinion, polarity := Core.NaturalLogic.ContextPolarity.downward, scalarPosition := some 0 }

theorem NeoGricean.ue_triggers_implicature : Interfaces.ImplicatureTheory.implicatureStatus someStudentsSleepNG 0 = Interfaces.ImplicatureStatus.triggered

In UE, implicature is triggered

theorem NeoGricean.de_blocks_implicature : Interfaces.ImplicatureTheory.implicatureStatus someStudentsSleepDE 0 = Interfaces.ImplicatureStatus.blocked

In DE, implicature is blocked

theorem NeoGricean.wrong_position_absent : Interfaces.ImplicatureTheory.implicatureStatus someStudentsSleepNG 1 = Interfaces.ImplicatureStatus.absent

Wrong position returns absent