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?

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

Equations

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

instance Phenomena.ScalarImplicatures.instReprDEBlockingDatum : Repr DEBlockingDatum

Equations

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

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?

instance Phenomena.ScalarImplicatures.instReprWeakStrongDatum : Repr WeakStrongDatum

Equations

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

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

Equations

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

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

instance Phenomena.ScalarImplicatures.instReprHornScaleDatum : Repr HornScaleDatum

Equations

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

def Phenomena.ScalarImplicatures.instReprHornScaleDatum.repr : HornScaleDatum → Nat → 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?

instance Phenomena.ScalarImplicatures.instReprScaleExample : Repr ScaleExample

Equations

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

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

Equations

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

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

instance Phenomena.ScalarImplicatures.instReprHornScaleDatumPair : Repr HornScaleDatumPair

Equations

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

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

Equations

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

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?

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

Equations

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

instance Phenomena.ScalarImplicatures.instReprHurfordDatum : Repr HurfordDatum

Equations

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

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?

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

Equations

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

instance Phenomena.ScalarImplicatures.instReprSinghDatum : Repr SinghDatum

Equations

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

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)