@cite{charlow-2021}: Empirical Data

@cite{charlow-2021}

Finite witnessing models for the cumulative reading puzzle.

Sentence: "Exactly three boys saw exactly five movies."

Scenario A (Figure 1): 3 boys, 5 movies. Each boy saw some movies; collectively all 5 movies were seen by some boy. Both cumulative and pseudo-cumulative readings are true.

Scenario B: 4 boys, 6 movies. Four boys collectively saw 6 movies, but a 3-boy subgroup saw exactly 5.

• Cumulative reading (= global counting): FALSE (4 boys total participated, not 3; 6 movies total, not 5)
• Pseudo-cumulative reading (= ∃ subset): TRUE ({b1,b2,b3} saw 5 movies)

The key empirical observation: native speakers judge the sentence FALSE in Scenario B, matching the cumulative reading.

inductive Phenomena.Plurals.Studies.Charlow2021.Data.Boy3 : Type

• b1 : Boy3
• b2 : Boy3
• b3 : Boy3

instance Phenomena.Plurals.Studies.Charlow2021.Data.instDecidableEqBoy3 : DecidableEq Boy3

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instDecidableEqBoy3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Plurals.Studies.Charlow2021.Data.instReprBoy3.repr : Boy3 → ℕ → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Charlow2021.Data.instReprBoy3 : Repr Boy3

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instReprBoy3 = { reprPrec := Phenomena.Plurals.Studies.Charlow2021.Data.instReprBoy3.repr }

instance Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy3 : BEq Boy3

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy3 = { beq := Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy3.beq }

def Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy3.beq : Boy3 → Boy3 → Bool

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy3.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Plurals.Studies.Charlow2021.Data.instFintypeBoy3 : Fintype Boy3

Equations

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

inductive Phenomena.Plurals.Studies.Charlow2021.Data.Movie5 : Type

• m1 : Movie5
• m2 : Movie5
• m3 : Movie5
• m4 : Movie5
• m5 : Movie5

instance Phenomena.Plurals.Studies.Charlow2021.Data.instDecidableEqMovie5 : DecidableEq Movie5

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instDecidableEqMovie5 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Plurals.Studies.Charlow2021.Data.instReprMovie5 : Repr Movie5

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instReprMovie5 = { reprPrec := Phenomena.Plurals.Studies.Charlow2021.Data.instReprMovie5.repr }

def Phenomena.Plurals.Studies.Charlow2021.Data.instReprMovie5.repr : Movie5 → ℕ → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie5 : BEq Movie5

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie5 = { beq := Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie5.beq }

def Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie5.beq : Movie5 → Movie5 → Bool

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie5.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Plurals.Studies.Charlow2021.Data.instFintypeMovie5 : Fintype Movie5

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Data.scenarioA_saw : Boy3 → Movie5 → Bool

Scenario A seeing relation (bipartite graph): b1 saw m1, m2; b2 saw m3, m4; b3 saw m5. Collectively: 3 boys saw 5 movies.

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioA_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy3.b1 Phenomena.Plurals.Studies.Charlow2021.Data.Movie5.m1 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioA_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy3.b1 Phenomena.Plurals.Studies.Charlow2021.Data.Movie5.m2 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioA_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy3.b2 Phenomena.Plurals.Studies.Charlow2021.Data.Movie5.m3 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioA_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy3.b2 Phenomena.Plurals.Studies.Charlow2021.Data.Movie5.m4 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioA_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy3.b3 Phenomena.Plurals.Studies.Charlow2021.Data.Movie5.m5 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioA_saw x✝¹ x✝ = false

inductive Phenomena.Plurals.Studies.Charlow2021.Data.Boy4 : Type

• b1 : Boy4
• b2 : Boy4
• b3 : Boy4
• b4 : Boy4

instance Phenomena.Plurals.Studies.Charlow2021.Data.instDecidableEqBoy4 : DecidableEq Boy4

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instDecidableEqBoy4 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Plurals.Studies.Charlow2021.Data.instReprBoy4 : Repr Boy4

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instReprBoy4 = { reprPrec := Phenomena.Plurals.Studies.Charlow2021.Data.instReprBoy4.repr }

def Phenomena.Plurals.Studies.Charlow2021.Data.instReprBoy4.repr : Boy4 → ℕ → Std.Format

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy4.beq : Boy4 → Boy4 → Bool

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy4.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy4 : BEq Boy4

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy4 = { beq := Phenomena.Plurals.Studies.Charlow2021.Data.instBEqBoy4.beq }

instance Phenomena.Plurals.Studies.Charlow2021.Data.instFintypeBoy4 : Fintype Boy4

Equations

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

inductive Phenomena.Plurals.Studies.Charlow2021.Data.Movie6 : Type

• m1 : Movie6
• m2 : Movie6
• m3 : Movie6
• m4 : Movie6
• m5 : Movie6
• m6 : Movie6

instance Phenomena.Plurals.Studies.Charlow2021.Data.instDecidableEqMovie6 : DecidableEq Movie6

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instDecidableEqMovie6 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Plurals.Studies.Charlow2021.Data.instReprMovie6 : Repr Movie6

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instReprMovie6 = { reprPrec := Phenomena.Plurals.Studies.Charlow2021.Data.instReprMovie6.repr }

def Phenomena.Plurals.Studies.Charlow2021.Data.instReprMovie6.repr : Movie6 → ℕ → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie6 : BEq Movie6

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie6 = { beq := Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie6.beq }

def Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie6.beq : Movie6 → Movie6 → Bool

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.instBEqMovie6.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Plurals.Studies.Charlow2021.Data.instFintypeMovie6 : Fintype Movie6

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_saw : Boy4 → Movie6 → Bool

Scenario B seeing relation: b1 saw m1, m2; b2 saw m3, m4; b3 saw m5; b4 saw m6. Four boys participated, seeing 6 distinct movies total.

Equations

• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy4.b1 Phenomena.Plurals.Studies.Charlow2021.Data.Movie6.m1 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy4.b1 Phenomena.Plurals.Studies.Charlow2021.Data.Movie6.m2 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy4.b2 Phenomena.Plurals.Studies.Charlow2021.Data.Movie6.m3 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy4.b2 Phenomena.Plurals.Studies.Charlow2021.Data.Movie6.m4 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy4.b3 Phenomena.Plurals.Studies.Charlow2021.Data.Movie6.m5 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_saw Phenomena.Plurals.Studies.Charlow2021.Data.Boy4.b4 Phenomena.Plurals.Studies.Charlow2021.Data.Movie6.m6 = true
• Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_saw x✝¹ x✝ = false

def Phenomena.Plurals.Studies.Charlow2021.Data.cumulativeReading {B : Type u_1} {M : Type u_2} [BEq B] [BEq M] (saw : B → M → Bool) (allBoys : List B) (allMovies : List M) (n_boys n_movies : ℕ) : Bool

Cumulative reading: the total number of boys who saw any movie = n_boys, AND the total number of movies seen by any boy = n_movies. This is the "global count" interpretation.

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Data.pseudoCumulativeReading {B : Type u_1} {M : Type u_2} [BEq M] (saw : B → M → Bool) (allBoys : List B) (allMovies : List M) (n_boys n_movies : ℕ) : Bool

Pseudo-cumulative reading: ∃ a subset of n_boys boys such that the movies they collectively saw number exactly n_movies. (Does NOT require the subset to be the maximal group.)

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Data.allBoys3 : List Boy3

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Data.allMovies5 : List Movie5

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Data.allBoys4 : List Boy4

Equations

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

def Phenomena.Plurals.Studies.Charlow2021.Data.allMovies6 : List Movie6

Equations

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

theorem Phenomena.Plurals.Studies.Charlow2021.Data.scenarioA_cumulative_true : cumulativeReading scenarioA_saw allBoys3 allMovies5 3 5 = true

Scenario A: cumulative reading is TRUE. 3 boys participated in seeing, and 5 movies were seen.

theorem Phenomena.Plurals.Studies.Charlow2021.Data.scenarioA_pseudo_true : pseudoCumulativeReading scenarioA_saw allBoys3 allMovies5 3 5 = true

Scenario A: pseudo-cumulative reading is also TRUE.

theorem Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_cumulative_false : cumulativeReading scenarioB_saw allBoys4 allMovies6 3 5 = false

Scenario B: cumulative reading is FALSE. 4 boys participated (not 3), and 6 movies were seen (not 5).

theorem Phenomena.Plurals.Studies.Charlow2021.Data.scenarioB_pseudo_true : pseudoCumulativeReading scenarioB_saw allBoys4 allMovies6 3 5 = true

Scenario B: pseudo-cumulative reading is TRUE (the overgeneration). {b1,b2,b3} is a 3-element subset that collectively saw 5 movies.