def Implicature.ScalarImplicatures.scaleAlternatives (sm : Alternatives.ScaleMembership) (ctx : Core.NaturalLogic.ContextPolarity) : List String

Get scalar alternatives for a scale member in context. Delegates to HornScale members filtered by semantic entailment, polarity-aware.

Equations

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

structure Implicature.ScalarImplicatures.ImplicatureCheck : Type

Lightweight wrapper preserving the .implicatureArises accessor.

• implicatureArises : Bool

def Implicature.ScalarImplicatures.instReprImplicatureCheck.repr : ImplicatureCheck → ℕ → Std.Format

Equations

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

instance Implicature.ScalarImplicatures.instReprImplicatureCheck : Repr ImplicatureCheck

Equations

• Implicature.ScalarImplicatures.instReprImplicatureCheck = { reprPrec := Implicature.ScalarImplicatures.instReprImplicatureCheck.repr }

instance Implicature.ScalarImplicatures.instDecidableEqImplicatureCheck : DecidableEq ImplicatureCheck

Equations

• Implicature.ScalarImplicatures.instDecidableEqImplicatureCheck = Implicature.ScalarImplicatures.instDecidableEqImplicatureCheck.decEq

def Implicature.ScalarImplicatures.instDecidableEqImplicatureCheck.decEq (x✝ x✝¹ : ImplicatureCheck) : Decidable (x✝ = x✝¹)

Equations

• Implicature.ScalarImplicatures.instDecidableEqImplicatureCheck.decEq { implicatureArises := a } { implicatureArises := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Implicature.ScalarImplicatures.quantImplicatureArises (term alt : Alternatives.Quantifiers.QuantExpr) (ctx : Core.NaturalLogic.ContextPolarity) : Bool

Does an alternative arise as a scalar implicature of a quantifier term?

Equations

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

def Implicature.ScalarImplicatures.someNotAll_UE : ImplicatureCheck

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

Equations

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

def Implicature.ScalarImplicatures.someNotAll_DE : ImplicatureCheck

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

Equations

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

theorem Implicature.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 Implicature.ScalarImplicatures.allNotSome_DE : ImplicatureCheck

Theorem: In DE, "All" Has Implicatures

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

Equations

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

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

inductive Implicature.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 Implicature.ScalarImplicatures.instDecidableEqDisjunctionInference : DecidableEq DisjunctionInference

Equations

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

instance Implicature.ScalarImplicatures.instBEqDisjunctionInference : BEq DisjunctionInference

Equations

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

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

Equations

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

instance Implicature.ScalarImplicatures.instReprDisjunctionInference : Repr DisjunctionInference

Equations

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

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

Equations

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

structure Implicature.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?

instance Implicature.ScalarImplicatures.instReprDisjunctionAnalysis : Repr DisjunctionAnalysis

Equations

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

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

Equations

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

def Implicature.ScalarImplicatures.analyzeDisjunction (ctx : Core.NaturalLogic.ContextPolarity) : DisjunctionAnalysis

Analyze a simple disjunction in context.

Both exclusivity AND ignorance can arise together.

Equations

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

theorem Implicature.ScalarImplicatures.disjunction_exclusivity_ue : (analyzeDisjunction Core.NaturalLogic.ContextPolarity.upward).exclusivityArises = true

Theorem: Disjunction in UE Has Exclusivity

theorem Implicature.ScalarImplicatures.exclusivity_ignorance_compatible : (analyzeDisjunction Core.NaturalLogic.ContextPolarity.upward).compatible = true

Theorem: Both Inferences Are Compatible

"A or B" can simultaneously implicate:

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

structure Implicature.ScalarImplicatures.LongDisjunction : Type

The long disjunction problem (@cite{geurts-2010} 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 Implicature.ScalarImplicatures.instReprLongDisjunction.repr : LongDisjunction → ℕ → Std.Format

Equations

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

instance Implicature.ScalarImplicatures.instReprLongDisjunction : Repr LongDisjunction

Equations

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

def Implicature.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 Implicature.ScalarImplicatures.fullConjunction (terms : List String) : String

Generate the full conjunction of all terms.

Equations

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

def Implicature.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 Implicature.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

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

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

Theorem: Three-way disjunction has 3 core alternatives

theorem Implicature.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 Implicature.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 Implicature.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

• Implicature.ScalarImplicatures.substitutionAlternative disjuncts = Implicature.ScalarImplicatures.fullConjunction disjuncts

structure Implicature.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 Implicature.ScalarImplicatures.instReprSubstitutionComparison : Repr SubstitutionComparison

Equations

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

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

Equations

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

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

Compare substitution method to full closure.

Equations

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

theorem Implicature.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 Implicature.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 Implicature.ScalarImplicatures.ScalarImplicatureResult : Type

Complete scalar implicature derivation result.

• term : String

  The original utterance's scalar term

• strongerAlts : List String

  Stronger alternatives found

• implicatures : List String

  Implicatures derived (negations of stronger alternatives)

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

Equations

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

instance Implicature.ScalarImplicatures.instReprScalarImplicatureResult : Repr ScalarImplicatureResult

Equations

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

def Implicature.ScalarImplicatures.deriveScalarImplicatures (term : String) (sm : Alternatives.ScaleMembership) (ctx : Core.NaturalLogic.ContextPolarity) : ScalarImplicatureResult

Derive all scalar implicatures for a term via HornScale.

Equations

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

def Implicature.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 Implicature.ScalarImplicatures.some_ue_implicatures : someUE.implicatures = ["not(most)", "not(all)"]

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

def Implicature.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 Implicature.ScalarImplicatures.some_de_no_implicatures : someDE.implicatures = []

Theorem: "some" in DE derives NO implicatures

def Implicature.ScalarImplicatures.deriveFromWords (words : List String) (ctx : Core.NaturalLogic.ContextPolarity) : List ScalarImplicatureResult

Derive scalar implicatures from a list of words. Each word is looked up in the scale registry; scalar words produce implicatures based on polarity context.

Equations

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

def Implicature.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 Implicature.ScalarImplicatures.someStudentsSleep_result : List ScalarImplicatureResult

"some students sleep": scalar item is "some"

Equations

• Implicature.ScalarImplicatures.someStudentsSleep_result = Implicature.ScalarImplicatures.deriveFromWords ["some", "students", "sleep"] Core.NaturalLogic.ContextPolarity.upward

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

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

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

"some students sleep" derives "not(most)"

def Implicature.ScalarImplicatures.everyStudentsSleeps_result : List ScalarImplicatureResult

"every student sleeps": "every" is scale-top, no stronger alternatives

Equations

• Implicature.ScalarImplicatures.everyStudentsSleeps_result = Implicature.ScalarImplicatures.deriveFromWords ["every", "student", "sleeps"] Core.NaturalLogic.ContextPolarity.upward

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

"every student sleeps" has no implicatures

def Implicature.ScalarImplicatures.someStudentsSleep_DE_result : List ScalarImplicatureResult

"some students sleep" in DE: implicature blocked

Equations

• Implicature.ScalarImplicatures.someStudentsSleep_DE_result = Implicature.ScalarImplicatures.deriveFromWords ["some", "students", "sleep"] Core.NaturalLogic.ContextPolarity.downward

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

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

theorem Implicature.ScalarImplicatures.defaultism_predicts_high_rate : predictsHighNeutralRate levinsonParams = true

Derived: Defaultism predicts high neutral rate

theorem Implicature.ScalarImplicatures.contextualism_predicts_moderate_rate : predictsHighNeutralRate geurtsParams = false

Derived: Contextualism predicts moderate neutral rate

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

Derived: Only contextualism predicts task effect

theorem Implicature.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 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)

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.

def Implicature.someStudentsSleepNG : NeoGriceanStructure

Example: "some students sleep" in UE context

Equations

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

def Implicature.someStudentsSleepDE : NeoGriceanStructure

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

Equations

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