Exhaustification Predictions for Semantic Scales

@cite{spector-2016} @cite{fox-2007} @cite{hurford-1974} @cite{singh-2008}

Exhaustification predictions for the semantic scales defined in Alternatives.Lexical: proves that exhIE(weaker) → ¬stronger for each Horn scale, and derives Hurford rescue and Singh asymmetry predictions.

• HurfordSemantic: Disjunction rescue via exhaustification
• SinghSemantic: Asymmetry in disjunction order

structure Exhaustification.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 Exhaustification.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.

Equations

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

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

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

Equations

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

structure Exhaustification.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 Exhaustification.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 = ¬Exhaustification.exhIE s.alts s.weaker ⊆ₚ s.stronger

def Exhaustification.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)

theorem Exhaustification.someAll_implicature (w : Alternatives.SemQuantWorld) : exhIE Alternatives.someAllScale.alts Alternatives.someQ w → ¬Alternatives.allQ w

Prediction: exh(some) → ¬all.

theorem Exhaustification.orAnd_implicature (w : Alternatives.ConnWorld) : exhIE Alternatives.orAndScale.alts Alternatives.orConn w → ¬Alternatives.andConn w

Prediction: exh(or) → ¬and.

theorem Exhaustification.possibleNecessary_implicature (w : Alternatives.ModalWorld) : exhIE Alternatives.possibleNecessaryScale.alts Alternatives.possibleP w → ¬Alternatives.necessaryP w

Prediction: exh(possible) → ¬necessary.

theorem Exhaustification.all_scale_implicatures_derived : (∀ (w : Alternatives.SemQuantWorld), exhIE Alternatives.someAllScale.alts Alternatives.someQ w → ¬Alternatives.allQ w) ∧ (∀ (w : Alternatives.ConnWorld), exhIE Alternatives.orAndScale.alts Alternatives.orConn w → ¬Alternatives.andConn w) ∧ ∀ (w : Alternatives.ModalWorld), exhIE Alternatives.possibleNecessaryScale.alts Alternatives.possibleP w → ¬Alternatives.necessaryP w

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

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

def Exhaustification.someOrAll_semantic : HurfordSemantic Alternatives.SemQuantWorld

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

Equations

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

theorem Exhaustification.someOrAll_is_rescued : someOrAll_semantic.isRescued

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

inductive Exhaustification.HyponymWorld : Type

World type for hyponymy: 3 regions of people

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

instance Exhaustification.instDecidableEqHyponymWorld : DecidableEq HyponymWorld

Equations

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

instance Exhaustification.instReprHyponymWorld : Repr HyponymWorld

Equations

• Exhaustification.instReprHyponymWorld = { reprPrec := Exhaustification.instReprHyponymWorld.repr }

def Exhaustification.instReprHyponymWorld.repr : HyponymWorld → ℕ → Std.Format

Equations

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

def Exhaustification.americanP : Prop' HyponymWorld

"American" predicate

Equations

• Exhaustification.americanP Exhaustification.HyponymWorld.notAmerican = False
• Exhaustification.americanP Exhaustification.HyponymWorld.americanOnly = True
• Exhaustification.americanP Exhaustification.HyponymWorld.californian = True

def Exhaustification.californianP : Prop' HyponymWorld

"Californian" predicate

Equations

• Exhaustification.californianP Exhaustification.HyponymWorld.californian = True
• Exhaustification.californianP w = False

theorem Exhaustification.californian_entails_american : californianP ⊆ₚ americanP

Californian entails American (hyponymy)

def Exhaustification.americanCalifornian_semantic : HurfordSemantic HyponymWorld

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

Equations

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

theorem Exhaustification.exh_californian_entails_american : exhIE americanCalifornian_semantic.alts californianP ⊆ₚ americanP

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

theorem Exhaustification.americanCalifornian_not_rescued : ¬americanCalifornian_semantic.isRescuedFromBA

Prediction: "American or Californian" is not rescued.

def Exhaustification.orThenBoth_semantic : SinghSemantic Alternatives.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 Exhaustification.bothThenOr_semantic : SinghSemantic Alternatives.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 Exhaustification.orAnd_exh_breaks_entailment : ¬exhIE {Alternatives.orConn, Alternatives.andConn} Alternatives.orConn ⊆ₚ Alternatives.andConn

Prediction: exh(or) breaks entailment to and.

theorem Exhaustification.orThenBoth_predicted_felicitous : orThenBoth_semantic.predictedFelicitous

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

theorem Exhaustification.bothThenOr_not_predicted_felicitous : ¬bothThenOr_semantic.predictedFelicitous

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

theorem Exhaustification.singh_asymmetry_derived : orThenBoth_semantic.predictedFelicitous ∧ ¬bothThenOr_semantic.predictedFelicitous

Main Result: Theory correctly predicts Singh asymmetry.