inductive Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.Student : Type

Three students in our domain

• alice : Student
• bob : Student
• carol : Student

instance Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instDecidableEqStudent : DecidableEq Student

Equations

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

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instReprStudent.repr : Student → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instReprStudent : Repr Student

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instReprStudent = { reprPrec := Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instReprStudent.repr }

instance Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instBEqStudent : BEq Student

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instBEqStudent = { beq := Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instBEqStudent.beq }

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instBEqStudent.beq : Student → Student → Bool

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instBEqStudent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.studentModel : Semantics.Montague.Model

Model with three students

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.studentModel = { Entity := Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.Student, decEq := inferInstance }

instance Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.instFintypeEntityStudentModel : Fintype studentModel.Entity

Equations

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

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.isStudent : studentModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

All entities are students in this model

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.isStudent x✝ = true

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.passedAt (w : Fin 4) : studentModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

"Passed" predicate indexed by world. World w means exactly w students passed (Alice, then Bob, then Carol).

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.passedAt w s✝ = false
• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.passedAt w Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.Student.alice = true
• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.passedAt w s✝ = false
• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.passedAt w Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.Student.alice = true
• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.passedAt w Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.Student.bob = true
• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.passedAt w Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.Student.carol = false
• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.passedAt w s✝ = true
• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.passedAt w s✝ = false

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.somePassedMontague (w : Fin 4) : Bool

"Some students passed" computed compositionally

Equations

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

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.allPassedMontague (w : Fin 4) : Bool

"All students passed" computed compositionally

Equations

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

@[reducible]

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.boolToProp (b : Bool) : Prop

Convert Bool to Prop

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.boolToProp b = (b = true)

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.somePassed_Prop : Prop' (Fin 4)

"Some students passed" as Prop' (Fin 4)

Equations

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

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.allPassed_Prop : Prop' (Fin 4)

"All students passed" as Prop' (Fin 4)

Equations

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

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.someAllALT_Montague : Set (Prop' (Fin 4))

Alternative set for exhaustivity

Equations

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

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.someStudents_handcrafted : Prop' (Fin 4)

someStudents from Operators.lean

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.someStudents_handcrafted w = (↑w ≥ 1)

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.allStudents_handcrafted : Prop' (Fin 4)

allStudents from Operators.lean

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.allStudents_handcrafted w = (↑w = 3)

theorem Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.somePassed_eq_handcrafted (w : Fin 4) : somePassed_Prop w ↔ someStudents_handcrafted w

Compositional "some" matches hand-crafted definition

theorem Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.allPassed_eq_handcrafted (w : Fin 4) : allPassed_Prop w ↔ allStudents_handcrafted w

Compositional "all" matches hand-crafted definition

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.w1_montague : Fin 4

World 1: one student passed

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.w1_montague = ⟨1, Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.w1_montague._proof_2⟩

def Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.w3_montague : Fin 4

World 3: all students passed

Equations

• Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.w3_montague = ⟨3, Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.w3_montague._proof_2⟩

theorem Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.w1_somePassed : somePassed_Prop w1_montague

At w1, "some passed" holds

theorem Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.w1_not_allPassed : ¬allPassed_Prop w1_montague

At w1, "all passed" does NOT hold

theorem Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.w3_both : somePassed_Prop w3_montague ∧ allPassed_Prop w3_montague

At w3, both "some" and "all" hold

theorem Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.exhMW_somePassed_at_w1 : Exhaustification.exhMW someAllALT_Montague somePassed_Prop w1_montague

Main Result: exhMW(some) holds at w1 (compositionally derived).

This proves the scalar implicature "some but not all" using:

1. Montague compositional semantics
2. @cite{spector-2016} exhaustivity operator

theorem Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.exhMW_somePassed_not_w3 : ¬Exhaustification.exhMW someAllALT_Montague somePassed_Prop w3_montague

Corollary: exhMW(some) does NOT hold at w3.

All-worlds are excluded by exhaustification of "some".

theorem Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.montague_exhMW_entails_exhIE : Exhaustification.exhMW someAllALT_Montague somePassed_Prop ⊆ₚ Exhaustification.exhIE someAllALT_Montague somePassed_Prop

Proposition 6 applies: exhMW ⊆ exhIE for compositional meanings

theorem Phenomena.ScalarImplicatures.Studies.MontagueExhaustivity.exhIE_somePassed_at_w1 : Exhaustification.exhIE someAllALT_Montague somePassed_Prop w1_montague

exhIE also holds at w1 (derived from exhMW via Proposition 6).