structure Phenomena.Negation.NegationInference : Type

A negation inference test case.

• premise : String

  The premise sentence

• conclusion : String

  The conclusion sentence

• setRelation : String

  The set relation licensing the inference

• direction : String

  Direction of inference (up = subset→superset, down = superset→subset)

• judgedValid : Bool

  Do speakers judge this as valid?

• notes : String

  Notes on the judgment

instance Phenomena.Negation.instReprNegationInference : Repr NegationInference

Equations

• Phenomena.Negation.instReprNegationInference = { reprPrec := Phenomena.Negation.instReprNegationInference.repr }

def Phenomena.Negation.instReprNegationInference.repr : NegationInference → Nat → Std.Format

Equations

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

def Phenomena.Negation.negation_de_valid : NegationInference

Negation is DE: "didn't see animal" → "didn't see dog" (downward valid).

Given: dogs ⊆ animals If John didn't see any animal, he didn't see any dog.

Equations

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

def Phenomena.Negation.negation_not_ue : NegationInference

Negation is NOT UE: "didn't see dog" ↛ "didn't see animal" (upward invalid).

Given: dogs ⊆ animals John could have not seen a dog but seen a cat (which is an animal).

Equations

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

def Phenomena.Negation.double_negation_ue : NegationInference

Double negation restores UE: "didn't not see dog" → "didn't not see animal".

DE ∘ DE = UE (proven in Core.Proposition and Entailment.Polarity)

Equations

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

structure Phenomena.Negation.SIBlockingDatum : Type

DE blocks scalar implicature: "didn't eat some" ≠ "didn't eat some but not all".

In UE contexts: "ate some" → "ate some but not all" (SI) In DE contexts: this implicature is blocked.

• sentence : String

  The sentence in a DE context

• siDerived : Bool

  Is the scalar implicature derived?

• literalMeaning : String

  Expected meaning without SI

• siMeaning : String

  Expected meaning with SI (if derived)

• notes : String

  Notes

instance Phenomena.Negation.instReprSIBlockingDatum : Repr SIBlockingDatum

Equations

• Phenomena.Negation.instReprSIBlockingDatum = { reprPrec := Phenomena.Negation.instReprSIBlockingDatum.repr }

def Phenomena.Negation.instReprSIBlockingDatum.repr : SIBlockingDatum → Nat → Std.Format

Equations

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

def Phenomena.Negation.negation_blocks_si : SIBlockingDatum

Equations

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

def Phenomena.Negation.positive_derives_si : SIBlockingDatum

Equations

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

structure Phenomena.Negation.NPIDatum : Type

Negative Polarity Item licensing datum.

• sentence : String

  The sentence with the NPI

• acceptable : Bool

  Is it grammatical/acceptable?

• npi : String

  The NPI being tested

• licensor : String

  The licensing environment

def Phenomena.Negation.instReprNPIDatum.repr : NPIDatum → Nat → Std.Format

Equations

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

instance Phenomena.Negation.instReprNPIDatum : Repr NPIDatum

Equations

• Phenomena.Negation.instReprNPIDatum = { reprPrec := Phenomena.Negation.instReprNPIDatum.repr }

def Phenomena.Negation.negation_licenses_anyone : NPIDatum

Equations

• Phenomena.Negation.negation_licenses_anyone = { sentence := "John didn't see anyone", acceptable := true, npi := "anyone", licensor := "negation (didn't)" }

def Phenomena.Negation.no_licensor_anyone : NPIDatum

Equations

• Phenomena.Negation.no_licensor_anyone = { sentence := "*John saw anyone", acceptable := false, npi := "anyone", licensor := "none" }

def Phenomena.Negation.negation_licenses_ever : NPIDatum

Equations

• Phenomena.Negation.negation_licenses_ever = { sentence := "John hasn't ever been to Paris", acceptable := true, npi := "ever", licensor := "negation (hasn't)" }

def Phenomena.Negation.no_licensor_ever : NPIDatum

Equations

• Phenomena.Negation.no_licensor_ever = { sentence := "*John has ever been to Paris", acceptable := false, npi := "ever", licensor := "none" }

def Phenomena.Negation.allNegationInferences : List NegationInference

Equations

• Phenomena.Negation.allNegationInferences = [Phenomena.Negation.negation_de_valid, Phenomena.Negation.negation_not_ue, Phenomena.Negation.double_negation_ue]

def Phenomena.Negation.allSIBlockingData : List SIBlockingDatum

Equations

• Phenomena.Negation.allSIBlockingData = [Phenomena.Negation.negation_blocks_si, Phenomena.Negation.positive_derives_si]

def Phenomena.Negation.allNPIData : List NPIDatum

Equations

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

theorem Phenomena.Negation.negation_is_de_not_ue : negation_de_valid.judgedValid = true ∧ negation_not_ue.judgedValid = false

Negation should be DE but not UE

theorem Phenomena.Negation.double_negation_restores_ue : double_negation_ue.judgedValid = true

Double negation should restore UE

theorem Phenomena.Negation.negation_blocks_scalar_implicature : negation_blocks_si.siDerived = false ∧ positive_derives_si.siDerived = true

Negation should block SI

theorem Phenomena.Negation.negation_licenses_npis : negation_licenses_anyone.acceptable = true ∧ negation_licenses_ever.acceptable = true

Negation should license NPIs