Scalar Implicatures: Empirical Data + canonical some/all model

Theory-neutral empirical patterns for scalar implicatures, plus the canonical 3-world SomeAllWorld model used by every study file in the directory that evaluates some/all sentence meanings.

Phenomena Covered

1. DE Blocking: Scalar implicatures blocked in downward-entailing contexts
2. Weak vs Strong: ¬Bel_S(ψ) vs Bel_S(¬ψ) distinction
3. Horn Scales: Scale examples with implicatures
4. Hurford's Constraint: Entailing disjunctions and rescue by exhaustification
5. Singh's Asymmetry: Order effects in scalar disjunctions

Canonical world model

SomeAllWorld is the minimal scenario type for evaluating the some/all scalar contrast: three worlds covering "no entity has the property" / "at least one but not all do" / "all do". The three predicates atLeastOne/universal/notUniversal give the literal some/all/SI meanings. Used by Hurford.lean, Embedded/Basic.lean, Embedded/Attitudes.lean (as a component of BeliefWorld), and the GeurtsPouscoulous2009 study file.

Key References

• Horn, L. (1972). On the Semantic Properties of Logical Operators in English.
• Hurford, J. (1974). Exclusive or inclusive disjunction. Foundations of Language.
• Gazdar, G. (1979). Pragmatics: Implicature, Presupposition, and Logical Form.
• Singh, R. (2008). On the interpretation of disjunction.
• Geurts, B. (2010). Quantity Implicatures. Cambridge University Press. Ch. 2-3.
• @cite{fox-spector-2018}. Economy and embedded exhaustification.

Canonical some/all world model

inductive Phenomena.ScalarImplicatures.SomeAllWorld : Type

The minimal scenario type for evaluating the some/all scalar contrast. Three worlds, parameterized by an implicit entity-set whose property-holders are being counted: zero (none), at least one but not all (someNotAll), or all (all).

• none : SomeAllWorld
• someNotAll : SomeAllWorld
• all : SomeAllWorld

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instDecidableEqSomeAllWorld : DecidableEq SomeAllWorld

Equations

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

def Phenomena.ScalarImplicatures.instReprSomeAllWorld.repr : SomeAllWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instReprSomeAllWorld : Repr SomeAllWorld

Equations

• Phenomena.ScalarImplicatures.instReprSomeAllWorld = { reprPrec := Phenomena.ScalarImplicatures.instReprSomeAllWorld.repr }

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instInhabitedSomeAllWorld : Inhabited SomeAllWorld

Equations

• Phenomena.ScalarImplicatures.instInhabitedSomeAllWorld = { default := Phenomena.ScalarImplicatures.instInhabitedSomeAllWorld.default }

def Phenomena.ScalarImplicatures.instInhabitedSomeAllWorld.default : SomeAllWorld

Equations

• Phenomena.ScalarImplicatures.instInhabitedSomeAllWorld.default = Phenomena.ScalarImplicatures.SomeAllWorld.none

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instFintypeSomeAllWorld : Fintype SomeAllWorld

Equations

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

def Phenomena.ScalarImplicatures.SomeAllWorld.atLeastOne : SomeAllWorld → Prop

Literal some meaning: at least one entity has the property.

Equations

• Phenomena.ScalarImplicatures.SomeAllWorld.none.atLeastOne = False
• x✝.atLeastOne = True

def Phenomena.ScalarImplicatures.SomeAllWorld.universal : SomeAllWorld → Prop

Literal all meaning: every entity has the property.

Equations

• Phenomena.ScalarImplicatures.SomeAllWorld.all.universal = True
• x✝.universal = False

def Phenomena.ScalarImplicatures.SomeAllWorld.notUniversal (w : SomeAllWorld) : Prop

The canonical scalar implicature of some: not all. Defined as the negation of universal.

Equations

• w.notUniversal = ¬w.universal

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.SomeAllWorld.instDecidablePredAtLeastOne : DecidablePred atLeastOne

Equations

• Phenomena.ScalarImplicatures.SomeAllWorld.none.instDecidablePredAtLeastOne = isFalse not_false
• Phenomena.ScalarImplicatures.SomeAllWorld.someNotAll.instDecidablePredAtLeastOne = isTrue trivial
• Phenomena.ScalarImplicatures.SomeAllWorld.all.instDecidablePredAtLeastOne = isTrue trivial

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.SomeAllWorld.instDecidablePredUniversal : DecidablePred universal

Equations

• Phenomena.ScalarImplicatures.SomeAllWorld.none.instDecidablePredUniversal = isFalse not_false
• Phenomena.ScalarImplicatures.SomeAllWorld.someNotAll.instDecidablePredUniversal = isFalse not_false
• Phenomena.ScalarImplicatures.SomeAllWorld.all.instDecidablePredUniversal = isTrue trivial

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.SomeAllWorld.instDecidableNotUniversal (w : SomeAllWorld) : Decidable w.notUniversal

Equations

• w.instDecidableNotUniversal = Phenomena.ScalarImplicatures.SomeAllWorld.instDecidableNotUniversal._aux_1 w

theorem Phenomena.ScalarImplicatures.SomeAllWorld.universal_imp_atLeastOne {w : SomeAllWorld} (h : w.universal) : w.atLeastOne

all asymmetrically entails some: this is the structural source of the some/all scalar contrast.

theorem Phenomena.ScalarImplicatures.SomeAllWorld.notUniversal_iff_not_universal {w : SomeAllWorld} : w.notUniversal ↔ ¬w.universal

The SI of some is exactly the complement of all.

structure Phenomena.ScalarImplicatures.DEBlockingDatum : Type

Empirical pattern: Scalar implicatures in DE contexts.

In upward-entailing (UE) contexts, "some" implicates "not all". In downward-entailing (DE) contexts, this implicature is blocked.

Examples:

• UE: "John ate some cookies" → "not all cookies"
• DE: "No one ate some cookies" → no "not all" implicature

• ueExample : String

  Example in UE context

• deExample : String

  Example in DE context

• scalarTerm : String

  Scalar term used

• strongerAlt : String

  Stronger alternative on the scale

• implicatureInUE : Bool

  Does the implicature arise in UE?

• implicatureInDE : Bool

  Does the implicature arise in DE?

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instReprDEBlockingDatum : Repr DEBlockingDatum

Equations

• Phenomena.ScalarImplicatures.instReprDEBlockingDatum = { reprPrec := Phenomena.ScalarImplicatures.instReprDEBlockingDatum.repr }

def Phenomena.ScalarImplicatures.instReprDEBlockingDatum.repr : DEBlockingDatum → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.someAllBlocking : DEBlockingDatum

Classic example: "some" in DE blocks "not all" implicature. Source: @cite{ladusaw-1980}, @cite{geurts-2010} Ch. 3.2

Equations

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

def Phenomena.ScalarImplicatures.orAndBlocking : DEBlockingDatum

"or" in DE blocks "not and" implicature. Source: @cite{geurts-2010} Ch. 3.2

Equations

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

def Phenomena.ScalarImplicatures.possibleNecessaryBlocking : DEBlockingDatum

"possible" in DE contexts. Source: @cite{horn-1989}

Equations

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

def Phenomena.ScalarImplicatures.everyRestrictorDE : DEBlockingDatum

Restrictor of "every" is DE. Source: @cite{ladusaw-1980}, @cite{barwise-cooper-1981}

Equations

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

def Phenomena.ScalarImplicatures.deBlockingExamples : List DEBlockingDatum

All DE blocking examples.

Equations

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

structure Phenomena.ScalarImplicatures.WeakStrongDatum : Type

Empirical pattern: Weak vs strong implicatures.

From "some students came":

• Weak: Speaker doesn't believe all came (¬Bel_S(all))
• Strong: Speaker believes not all came (Bel_S(¬all))

The strong requires a competence assumption.

Source: @cite{soames-1982}, @cite{geurts-2010} Ch. 2.3

• utterance : String

  The utterance

• alternative : String

  The scalar alternative

• weakImplicature : String

  Weak implicature description

• strongImplicature : String

  Strong implicature description

• weakRequiresCompetence : Bool

  Does weak require competence?

• strongRequiresCompetence : Bool

  Does strong require competence?

def Phenomena.ScalarImplicatures.instReprWeakStrongDatum.repr : WeakStrongDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instReprWeakStrongDatum : Repr WeakStrongDatum

Equations

• Phenomena.ScalarImplicatures.instReprWeakStrongDatum = { reprPrec := Phenomena.ScalarImplicatures.instReprWeakStrongDatum.repr }

def Phenomena.ScalarImplicatures.someStudents : WeakStrongDatum

Classic "some" example. Source: @cite{horn-1972}, @cite{geurts-2010} Ch. 2.3

Equations

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

def Phenomena.ScalarImplicatures.orWeakStrong : WeakStrongDatum

"Or" example showing weak vs strong. Source: @cite{gazdar-1979}

Equations

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

def Phenomena.ScalarImplicatures.numeralWeakStrong : WeakStrongDatum

Numeral example. Source: @cite{horn-1972}

Equations

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

def Phenomena.ScalarImplicatures.weakStrongExamples : List WeakStrongDatum

All weak/strong examples.

Equations

• Phenomena.ScalarImplicatures.weakStrongExamples = [Phenomena.ScalarImplicatures.someStudents, Phenomena.ScalarImplicatures.orWeakStrong, Phenomena.ScalarImplicatures.numeralWeakStrong]

structure Phenomena.ScalarImplicatures.HornScaleDatum : Type

A Horn scale with its members and example implicatures. Source: @cite{horn-1972}

• name : String

  Name of the scale

• members : List String

  Members from weakest to strongest

• exampleSentence : String

  Example sentence with weakest term

• implicature : String

  Resulting implicature

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instReprHornScaleDatum : Repr HornScaleDatum

Equations

• Phenomena.ScalarImplicatures.instReprHornScaleDatum = { reprPrec := Phenomena.ScalarImplicatures.instReprHornScaleDatum.repr }

def Phenomena.ScalarImplicatures.instReprHornScaleDatum.repr : HornScaleDatum → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.quantifierScale : HornScaleDatum

Quantifier scale. Source: @cite{horn-1972}

Equations

• Phenomena.ScalarImplicatures.quantifierScale = { name := "Quantifiers", members := ["some", "most", "all"], exampleSentence := "Some students passed", implicature := "Not all students passed" }

def Phenomena.ScalarImplicatures.connectiveScale : HornScaleDatum

Connective scale. Source: @cite{horn-1972}

Equations

• Phenomena.ScalarImplicatures.connectiveScale = { name := "Connectives", members := ["or", "and"], exampleSentence := "John sang or danced", implicature := "John didn't both sing and dance" }

def Phenomena.ScalarImplicatures.modalScale : HornScaleDatum

Modal scale. Source: @cite{horn-1972}

Equations

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

def Phenomena.ScalarImplicatures.numeralScale : HornScaleDatum

Numeral scale (with lower-bound semantics). Source: @cite{horn-1972}

Equations

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

def Phenomena.ScalarImplicatures.hornScaleExamples : List HornScaleDatum

All Horn scale examples.

Equations

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

structure Phenomena.ScalarImplicatures.ScaleExample : Type

An example sentence demonstrating a scalar implicature.

• sentence : String

  The sentence

• implicature : String

  The predicted implicature

• arisesInUE : Bool

  Does the implicature arise in upward-entailing context?

def Phenomena.ScalarImplicatures.instReprScaleExample.repr : ScaleExample → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instReprScaleExample : Repr ScaleExample

Equations

• Phenomena.ScalarImplicatures.instReprScaleExample = { reprPrec := Phenomena.ScalarImplicatures.instReprScaleExample.repr }

structure Phenomena.ScalarImplicatures.HornScaleDatumPair : Type

A Horn scale datum with weaker/stronger terms (string-level).

• name : String

  Name of the scale

• weakerTerm : String

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

• strongerTerm : String

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

• exampleSentence : ScaleExample

  Example sentence

def Phenomena.ScalarImplicatures.instReprHornScaleDatumPair.repr : HornScaleDatumPair → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instReprHornScaleDatumPair : Repr HornScaleDatumPair

Equations

• Phenomena.ScalarImplicatures.instReprHornScaleDatumPair = { reprPrec := Phenomena.ScalarImplicatures.instReprHornScaleDatumPair.repr }

def Phenomena.ScalarImplicatures.someAllExample : ScaleExample

Example: "Some students passed"

Equations

• Phenomena.ScalarImplicatures.someAllExample = { sentence := "Some students passed", implicature := "Not all students passed" }

def Phenomena.ScalarImplicatures.someAllDatum : HornScaleDatumPair

The some/all scale datum.

Equations

• Phenomena.ScalarImplicatures.someAllDatum = { name := "Quantifiers (some/all)", weakerTerm := "some", strongerTerm := "all", exampleSentence := Phenomena.ScalarImplicatures.someAllExample }

def Phenomena.ScalarImplicatures.orAndExample : ScaleExample

Example: "John sang or danced"

Equations

• Phenomena.ScalarImplicatures.orAndExample = { sentence := "John sang or danced", implicature := "John didn't both sing and dance" }

def Phenomena.ScalarImplicatures.orAndDatum : HornScaleDatumPair

The or/and scale datum.

Equations

• Phenomena.ScalarImplicatures.orAndDatum = { name := "Connectives (or/and)", weakerTerm := "or", strongerTerm := "and", exampleSentence := Phenomena.ScalarImplicatures.orAndExample }

def Phenomena.ScalarImplicatures.possibleNecessaryExample : ScaleExample

Example: "It's possible it will rain"

Equations

• Phenomena.ScalarImplicatures.possibleNecessaryExample = { sentence := "It's possible that it will rain", implicature := "It's not necessary that it will rain" }

def Phenomena.ScalarImplicatures.possibleNecessaryDatum : HornScaleDatumPair

The possible/necessary scale datum.

Equations

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

def Phenomena.ScalarImplicatures.allScaleExamples : List ScaleExample

All scale examples (string-level).

Equations

• Phenomena.ScalarImplicatures.allScaleExamples = [Phenomena.ScalarImplicatures.someAllExample, Phenomena.ScalarImplicatures.orAndExample, Phenomena.ScalarImplicatures.possibleNecessaryExample]

def Phenomena.ScalarImplicatures.allScalePairs : List HornScaleDatumPair

All Horn scale pair data.

Equations

• Phenomena.ScalarImplicatures.allScalePairs = [Phenomena.ScalarImplicatures.someAllDatum, Phenomena.ScalarImplicatures.orAndDatum, Phenomena.ScalarImplicatures.possibleNecessaryDatum]

theorem Phenomena.ScalarImplicatures.all_arise_in_UE : (allScaleExamples.all fun (x : ScaleExample) => x.arisesInUE) = true

All examples arise in UE contexts.

structure Phenomena.ScalarImplicatures.HurfordDatum : Type

A potential Hurford violation: a disjunction "A or B" where one disjunct entails the other.

• sentence : String

  The disjunction sentence

• disjunctA : String

  First disjunct

• disjunctB : String

  Second disjunct

• entailmentDirection : String

  Which direction is the entailment?

• felicitous : Bool

  Is the sentence felicitous?

• rescueMethod : Option String

  If felicitous, how is it rescued?

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instReprHurfordDatum : Repr HurfordDatum

Equations

• Phenomena.ScalarImplicatures.instReprHurfordDatum = { reprPrec := Phenomena.ScalarImplicatures.instReprHurfordDatum.repr }

def Phenomena.ScalarImplicatures.instReprHurfordDatum.repr : HurfordDatum → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.americanCalifornian : HurfordDatum

Classic Hurford violation: hyponym or hypernym. "#John is American or Californian" — Californian entails American.

Equations

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

def Phenomena.ScalarImplicatures.bachelorUnmarried : HurfordDatum

"#John is a bachelor or unmarried" — bachelor entails unmarried.

Equations

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

def Phenomena.ScalarImplicatures.evenDivisibleBy2 : HurfordDatum

"#The number is even or divisible by 2"

Equations

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

def Phenomena.ScalarImplicatures.someOrAll : HurfordDatum

Rescued by exhaustification: "some or all". exh(some) = "some but not all", which doesn't entail "all".

Equations

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

def Phenomena.ScalarImplicatures.possibleOrNecessary : HurfordDatum

Rescued: "possible or necessary". exh(possible) = "possible but not necessary", doesn't entail "necessary".

Equations

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

def Phenomena.ScalarImplicatures.threeOrAll : HurfordDatum

Rescued: "three or all" (distant entailing disjunction). exh(three) = "exactly three", which doesn't entail "all".

Equations

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

def Phenomena.ScalarImplicatures.hurfordViolations : List HurfordDatum

Infelicitous Hurford violations.

Equations

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

def Phenomena.ScalarImplicatures.hurfordRescuedCases : List HurfordDatum

Felicitous (rescued) cases.

Equations

• Phenomena.ScalarImplicatures.hurfordRescuedCases = [Phenomena.ScalarImplicatures.someOrAll, Phenomena.ScalarImplicatures.possibleOrNecessary, Phenomena.ScalarImplicatures.threeOrAll]

def Phenomena.ScalarImplicatures.allHurfordData : List HurfordDatum

All Hurford data.

Equations

• Phenomena.ScalarImplicatures.allHurfordData = Phenomena.ScalarImplicatures.hurfordViolations ++ Phenomena.ScalarImplicatures.hurfordRescuedCases

theorem Phenomena.ScalarImplicatures.hurford_violations_infelicitous : (hurfordViolations.all fun (x : HurfordDatum) => x.felicitous == false) = true

All violations are infelicitous.

theorem Phenomena.ScalarImplicatures.hurford_rescued_felicitous : (hurfordRescuedCases.all fun (x : HurfordDatum) => x.felicitous == true) = true

All rescued cases are felicitous.

theorem Phenomena.ScalarImplicatures.hurford_rescued_have_method : (hurfordRescuedCases.all fun (x : HurfordDatum) => x.rescueMethod.isSome) = true

All rescued cases have a rescue method.

structure Phenomena.ScalarImplicatures.SinghDatum : Type

A Singh-style disjunction where one disjunct is stronger than the other.

• sentence : String

  The full sentence

• weakerDisjunct : String

  The weaker disjunct (e.g., "A or B")

• strongerDisjunct : String

  The stronger disjunct (e.g., "A and B" / "both")

• weakerFirst : Bool

  Is the weaker mentioned first?

• felicitous : Bool

  Is the sentence felicitous?

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.instReprSinghDatum : Repr SinghDatum

Equations

• Phenomena.ScalarImplicatures.instReprSinghDatum = { reprPrec := Phenomena.ScalarImplicatures.instReprSinghDatum.repr }

def Phenomena.ScalarImplicatures.instReprSinghDatum.repr : SinghDatum → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.orThenBoth : SinghDatum

Classic Singh example: weak-first is OK. "Mary solved problem A or B, or both"

Equations

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

def Phenomena.ScalarImplicatures.cakeOrPieOrBoth : SinghDatum

"John ate cake or pie, or both"

Equations

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

def Phenomena.ScalarImplicatures.singhPossibleOrNecessary : SinghDatum

"It's possible or necessary that it will rain"

Equations

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

def Phenomena.ScalarImplicatures.bothThenOr : SinghDatum

Strong-first is odd: "#both, or A or B"

Equations

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

def Phenomena.ScalarImplicatures.bothThenCakeOrPie : SinghDatum

"#John ate both, or cake or pie"

Equations

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

def Phenomena.ScalarImplicatures.necessaryOrPossible : SinghDatum

"#It's necessary or possible that it will rain" (Strong-first with modals)

Equations

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

def Phenomena.ScalarImplicatures.singhWeakFirstCases : List SinghDatum

Weak-first (felicitous) cases.

Equations

• Phenomena.ScalarImplicatures.singhWeakFirstCases = [Phenomena.ScalarImplicatures.orThenBoth, Phenomena.ScalarImplicatures.cakeOrPieOrBoth, Phenomena.ScalarImplicatures.singhPossibleOrNecessary]

def Phenomena.ScalarImplicatures.singhStrongFirstCases : List SinghDatum

Strong-first (infelicitous) cases.

Equations

• Phenomena.ScalarImplicatures.singhStrongFirstCases = [Phenomena.ScalarImplicatures.bothThenOr, Phenomena.ScalarImplicatures.bothThenCakeOrPie, Phenomena.ScalarImplicatures.necessaryOrPossible]

def Phenomena.ScalarImplicatures.allSinghData : List SinghDatum

All Singh data.

Equations

• Phenomena.ScalarImplicatures.allSinghData = Phenomena.ScalarImplicatures.singhWeakFirstCases ++ Phenomena.ScalarImplicatures.singhStrongFirstCases

theorem Phenomena.ScalarImplicatures.singh_weakFirst_felicitous : (singhWeakFirstCases.all fun (x : SinghDatum) => x.felicitous == true) = true

Weak-first cases are felicitous.

theorem Phenomena.ScalarImplicatures.singh_strongFirst_infelicitous : (singhStrongFirstCases.all fun (x : SinghDatum) => x.felicitous == false) = true

Strong-first cases are infelicitous.

theorem Phenomena.ScalarImplicatures.singh_weakFirst_order : (singhWeakFirstCases.all fun (x : SinghDatum) => x.weakerFirst == true) = true

All weak-first cases have weakerFirst = true.

theorem Phenomena.ScalarImplicatures.singh_strongFirst_order : (singhStrongFirstCases.all fun (x : SinghDatum) => x.weakerFirst == false) = true

All strong-first cases have weakerFirst = false.

theorem Phenomena.ScalarImplicatures.singh_asymmetry : (allSinghData.all fun (d : SinghDatum) => d.felicitous == d.weakerFirst) = true

The Singh asymmetry: felicitous ↔ weakerFirst (at the data level; theory explains why)