Spector (2016): Worked examples of exhaustivity operators

[Spe16] "Comparing Exhaustivity Operators." Semantics and Pragmatics 9(11): 1–33.

Concrete derivations of exhMW, exhIE, and their coincidence (Theorem 9) on the two classic Horn scales:

1. some/all scale: "Some students passed" → "Not all students passed"
2. or/and scale: "John sang or danced" → exclusive reading

The abstract Spector framework lives in Semantics/Exhaustification/Operators/Basic.lean. This file holds the empirical exemplars — small finite worlds, scale-specific alternative sets, and the per-scale exhMW ≡ exhIE corollaries — kept out of the theory file in line with the project's theory/Studies split.

It also collects the [Chi13] Maximize Strength worked examples (matrix-clause SI computed, DE-context SI suppressed) as a small table of MaximizeStrengthExample records.

Results

• exhMW_some_at_w1, exhMW_some_not_w3 — exhMW(some) excludes "all"
• exhMW_or_at_wSang, exhMW_or_not_wBoth — exhMW(or) excludes "both"
• someAll_exhMW_iff_exhIE, orAnd_exhMW_iff_exhIE — Theorem 9 instances
• maximizeStrengthExamples — Maximize Strength contexts table

"Some students passed"

• φ = "some students passed" (literal meaning: at least one)
• ALT = {some, all}
• Expected: exhMW(some) = "some but not all"

World model: Fin 4 represents how many students passed (0–3 of 3).

@[reducible, inline]

abbrev Spector2016.SomeAllWorld : Type

Worlds for some/all example: number of students who passed (0 to 3).

Equations

• Spector2016.SomeAllWorld = Fin 4

def Spector2016.someStudents : Set SomeAllWorld

"Some students passed" (at least one).

Equations

• Spector2016.someStudents w = (↑w ≥ 1)

def Spector2016.allStudents : Set SomeAllWorld

"All students passed" (all three).

Equations

• Spector2016.allStudents w = (↑w = 3)

def Spector2016.someAllALT : Set (Set SomeAllWorld)

Alternative set: {some, all}.

Equations

• Spector2016.someAllALT = {Spector2016.someStudents, Spector2016.allStudents}

def Spector2016.w1 : SomeAllWorld

World where exactly 1 student passed.

Equations

• Spector2016.w1 = ⟨1, Spector2016.w1._proof_2⟩

def Spector2016.w3 : SomeAllWorld

World where all 3 students passed.

Equations

• Spector2016.w3 = ⟨3, Spector2016.w3._proof_2⟩

theorem Spector2016.w1_satisfies_some : someStudents w1

theorem Spector2016.w1_not_all : ¬allStudents w1

theorem Spector2016.w3_satisfies_both : someStudents w3 ∧ allStudents w3

theorem Spector2016.w1_leALT_w3 : w1 ≤[someAllALT] w3

theorem Spector2016.w3_not_leALT_w1 : ¬w3 ≤[someAllALT] w1

theorem Spector2016.w1_ltALT_w3 : w1 <[someAllALT] w3

theorem Spector2016.w1_minimal_some : Exhaustification.IsMinimal someAllALT someStudents w1

theorem Spector2016.w3_not_minimal_some : ¬Exhaustification.IsMinimal someAllALT someStudents w3

theorem Spector2016.exhMW_some_at_w1 : Exhaustification.exhMW someAllALT someStudents w1

exhMW(some) holds at w=1 — the scalar implicature "some but not all".

theorem Spector2016.exhMW_some_not_w3 : ¬Exhaustification.exhMW someAllALT someStudents w3

exhMW(some) excludes the "all" world.

"John sang or danced"

• World = four possibilities: neither, only sang, only danced, both
• φ = "sang or danced" (inclusive)
• ALT = {or, and}
• Expected: exhMW(or) = "or but not both" (exclusive reading)

inductive Spector2016.OrAndWorld : Type

Four worlds for or/and example.

• neither : OrAndWorld
• onlySang : OrAndWorld
• onlyDanced : OrAndWorld
• both : OrAndWorld

@[implicit_reducible]

instance Spector2016.instDecidableEqOrAndWorld : DecidableEq OrAndWorld

Equations

• Spector2016.instDecidableEqOrAndWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Spector2016.instReprOrAndWorld : Repr OrAndWorld

Equations

• Spector2016.instReprOrAndWorld = { reprPrec := Spector2016.instReprOrAndWorld.repr }

def Spector2016.instReprOrAndWorld.repr : OrAndWorld → ℕ → Std.Format

Equations

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

def Spector2016.sang : Set OrAndWorld

Equations

• Spector2016.sang Spector2016.OrAndWorld.neither = False
• Spector2016.sang Spector2016.OrAndWorld.onlySang = True
• Spector2016.sang Spector2016.OrAndWorld.onlyDanced = False
• Spector2016.sang Spector2016.OrAndWorld.both = True

def Spector2016.danced : Set OrAndWorld

Equations

• Spector2016.danced Spector2016.OrAndWorld.neither = False
• Spector2016.danced Spector2016.OrAndWorld.onlySang = False
• Spector2016.danced Spector2016.OrAndWorld.onlyDanced = True
• Spector2016.danced Spector2016.OrAndWorld.both = True

def Spector2016.sangOrDanced : Set OrAndWorld

Equations

• Spector2016.sangOrDanced w = (Spector2016.sang w ∨ Spector2016.danced w)

def Spector2016.sangAndDanced : Set OrAndWorld

Equations

• Spector2016.sangAndDanced w = (Spector2016.sang w ∧ Spector2016.danced w)

def Spector2016.orAndALT : Set (Set OrAndWorld)

Equations

• Spector2016.orAndALT = {Spector2016.sangOrDanced, Spector2016.sangAndDanced}

def Spector2016.wSang : OrAndWorld

Equations

• Spector2016.wSang = Spector2016.OrAndWorld.onlySang

def Spector2016.wBoth : OrAndWorld

Equations

• Spector2016.wBoth = Spector2016.OrAndWorld.both

theorem Spector2016.wSang_satisfies_or : sangOrDanced wSang

theorem Spector2016.wSang_not_and : ¬sangAndDanced wSang

theorem Spector2016.wBoth_satisfies_both : sangOrDanced wBoth ∧ sangAndDanced wBoth

theorem Spector2016.wSang_leALT_wBoth : wSang ≤[orAndALT] wBoth

theorem Spector2016.wBoth_not_leALT_wSang : ¬wBoth ≤[orAndALT] wSang

theorem Spector2016.wSang_ltALT_wBoth : wSang <[orAndALT] wBoth

theorem Spector2016.wSang_minimal : Exhaustification.IsMinimal orAndALT sangOrDanced wSang

theorem Spector2016.exhMW_or_at_wSang : Exhaustification.exhMW orAndALT sangOrDanced wSang

exhMW(or) at wSang: exclusive reading.

theorem Spector2016.exhMW_or_not_wBoth : ¬Exhaustification.exhMW orAndALT sangOrDanced wBoth

exhMW(or) excludes the "both" world.

For a two-element Horn scale {weak, strong} where strong ⊆ weak, exhMW ≡ exhIE without invoking the full closure-under-conjunction hypothesis: at any exhIE world, the stronger alternative is false, which makes the world minimal.

theorem Spector2016.allStudents_entails_someStudents : allStudents ⊆ someStudents

theorem Spector2016.someAll_exhMW_iff_exhIE : Exhaustification.exhMW someAllALT someStudents = Exhaustification.exhIE someAllALT someStudents

Per-scale Theorem 9 instance: some/all.

theorem Spector2016.sangAndDanced_entails_sangOrDanced : sangAndDanced ⊆ sangOrDanced

theorem Spector2016.orAnd_exhMW_iff_exhIE : Exhaustification.exhMW orAndALT sangOrDanced = Exhaustification.exhIE orAndALT sangOrDanced

Per-scale Theorem 9 instance: or/and.

theorem Spector2016.exhIE_some_at_w1 : Exhaustification.exhIE someAllALT someStudents w1

theorem Spector2016.exhIE_some_not_w3 : ¬Exhaustification.exhIE someAllALT someStudents w3

theorem Spector2016.exhIE_or_at_wSang : Exhaustification.exhIE orAndALT sangOrDanced wSang

theorem Spector2016.exhIE_or_not_wBoth : ¬Exhaustification.exhIE orAndALT sangOrDanced wBoth

A small descriptive table of contexts illustrating [Chi13]'s Maximize Strength predictions. The principle itself (maximizeStrength, exh_in_ue_strengthens, etc.) lives in Operators.lean.

Context	Polarity	SI computed?
Matrix clause	UE	yes
Negation scope	DE	no
Conditional antecedent	DE	no
Universal restrictor	DE	no

structure Spector2016.MaximizeStrengthExample : Type

• description : String
• contextType : NaturalLogic.ContextPolarity
• siComputed : Bool
• explanation : String

@[implicit_reducible]

instance Spector2016.instReprMaximizeStrengthExample : Repr MaximizeStrengthExample

Equations

• Spector2016.instReprMaximizeStrengthExample = { reprPrec := Spector2016.instReprMaximizeStrengthExample.repr }

def Spector2016.instReprMaximizeStrengthExample.repr : MaximizeStrengthExample → ℕ → Std.Format

Equations

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

def Spector2016.ms_matrix_clause : MaximizeStrengthExample

Equations

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

def Spector2016.ms_negation : MaximizeStrengthExample

Equations

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

def Spector2016.ms_antecedent : MaximizeStrengthExample

Equations

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

def Spector2016.ms_universal_restrictor : MaximizeStrengthExample

Equations

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

def Spector2016.maximizeStrengthExamples : List MaximizeStrengthExample

Equations

• Spector2016.maximizeStrengthExamples = [Spector2016.ms_matrix_clause, Spector2016.ms_negation, Spector2016.ms_antecedent, Spector2016.ms_universal_restrictor]