inductive MontagueExhaustivity.Student : Type

Three students in our domain

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

@[implicit_reducible]

instance MontagueExhaustivity.instDecidableEqStudent : DecidableEq Student

Equations

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

def MontagueExhaustivity.instReprStudent.repr : Student → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MontagueExhaustivity.instReprStudent : Repr Student

Equations

• MontagueExhaustivity.instReprStudent = { reprPrec := MontagueExhaustivity.instReprStudent.repr }

def MontagueExhaustivity.studentModel : Core.Logic.Intensional.Frame

Model with three students

Equations

• MontagueExhaustivity.studentModel = { Entity := MontagueExhaustivity.Student, Index := Unit }

@[implicit_reducible]

instance MontagueExhaustivity.instFintypeEntityStudentModel : Fintype studentModel.Entity

Equations

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

def MontagueExhaustivity.isStudent : studentModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

All entities are students in this model

Equations

• MontagueExhaustivity.isStudent x✝ = True

def MontagueExhaustivity.passedAt (w : Fin 4) : studentModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

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

Equations

• MontagueExhaustivity.passedAt w s✝ = False
• MontagueExhaustivity.passedAt w MontagueExhaustivity.Student.alice = True
• MontagueExhaustivity.passedAt w s✝ = False
• MontagueExhaustivity.passedAt w MontagueExhaustivity.Student.alice = True
• MontagueExhaustivity.passedAt w MontagueExhaustivity.Student.bob = True
• MontagueExhaustivity.passedAt w MontagueExhaustivity.Student.carol = False
• MontagueExhaustivity.passedAt w s✝ = True
• MontagueExhaustivity.passedAt w s✝ = False

def MontagueExhaustivity.somePassedMontague (w : Fin 4) : Prop

"Some students passed" computed compositionally

Equations

• MontagueExhaustivity.somePassedMontague w = Semantics.Quantification.Quantifier.some_sem MontagueExhaustivity.studentModel MontagueExhaustivity.isStudent (MontagueExhaustivity.passedAt w)

def MontagueExhaustivity.allPassedMontague (w : Fin 4) : Prop

"All students passed" computed compositionally

Equations

• MontagueExhaustivity.allPassedMontague w = Semantics.Quantification.Quantifier.every_sem MontagueExhaustivity.studentModel MontagueExhaustivity.isStudent (MontagueExhaustivity.passedAt w)

def MontagueExhaustivity.somePassed_Prop : Set (Fin 4)

"Some students passed" as Set (Fin 4)

Equations

• MontagueExhaustivity.somePassed_Prop = MontagueExhaustivity.somePassedMontague

def MontagueExhaustivity.allPassed_Prop : Set (Fin 4)

"All students passed" as Set (Fin 4)

Equations

• MontagueExhaustivity.allPassed_Prop = MontagueExhaustivity.allPassedMontague

def MontagueExhaustivity.someAllALT_Montague : Set (Set (Fin 4))

Alternative set for exhaustivity

Equations

• MontagueExhaustivity.someAllALT_Montague = {MontagueExhaustivity.somePassed_Prop, MontagueExhaustivity.allPassed_Prop}

def MontagueExhaustivity.someStudents_handcrafted : Set (Fin 4)

someStudents from Operators.lean

Equations

• MontagueExhaustivity.someStudents_handcrafted w = (↑w ≥ 1)

def MontagueExhaustivity.allStudents_handcrafted : Set (Fin 4)

allStudents from Operators.lean

Equations

• MontagueExhaustivity.allStudents_handcrafted w = (↑w = 3)

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

Compositional "some" matches hand-crafted definition

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

Compositional "all" matches hand-crafted definition

def MontagueExhaustivity.w1_montague : Fin 4

World 1: one student passed

Equations

• MontagueExhaustivity.w1_montague = ⟨1, MontagueExhaustivity.w1_montague._proof_2⟩

def MontagueExhaustivity.w3_montague : Fin 4

World 3: all students passed

Equations

• MontagueExhaustivity.w3_montague = ⟨3, MontagueExhaustivity.w3_montague._proof_2⟩

theorem MontagueExhaustivity.w1_somePassed : somePassed_Prop w1_montague

At w1, "some passed" holds

theorem MontagueExhaustivity.w1_not_allPassed : ¬allPassed_Prop w1_montague

At w1, "all passed" does NOT hold

theorem MontagueExhaustivity.w3_both : somePassed_Prop w3_montague ∧ allPassed_Prop w3_montague

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

theorem 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 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 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 MontagueExhaustivity.exhIE_somePassed_at_w1 : Exhaustification.exhIE someAllALT_Montague somePassed_Prop w1_montague

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