@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 Data.Boy3 : Type

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

@[implicit_reducible]

instance Data.instDecidableEqBoy3 : DecidableEq Boy3

Equations

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

@[implicit_reducible]

instance Data.instReprBoy3 : Repr Boy3

Equations

• Data.instReprBoy3 = { reprPrec := Data.instReprBoy3.repr }

def Data.instReprBoy3.repr : Boy3 → ℕ → Std.Format

Equations

• Data.instReprBoy3.repr Data.Boy3.b1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Boy3.b1")).group prec✝
• Data.instReprBoy3.repr Data.Boy3.b2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Boy3.b2")).group prec✝
• Data.instReprBoy3.repr Data.Boy3.b3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Boy3.b3")).group prec✝

@[implicit_reducible]

instance Data.instFintypeBoy3 : Fintype Boy3

Equations

• Data.instFintypeBoy3 = { elems := {Data.Boy3.b1, Data.Boy3.b2, Data.Boy3.b3}, complete := Data.instFintypeBoy3._proof_1 }

inductive Data.Movie5 : Type

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

@[implicit_reducible]

instance Data.instDecidableEqMovie5 : DecidableEq Movie5

Equations

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

def Data.instReprMovie5.repr : Movie5 → ℕ → Std.Format

Equations

• Data.instReprMovie5.repr Data.Movie5.m1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie5.m1")).group prec✝
• Data.instReprMovie5.repr Data.Movie5.m2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie5.m2")).group prec✝
• Data.instReprMovie5.repr Data.Movie5.m3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie5.m3")).group prec✝
• Data.instReprMovie5.repr Data.Movie5.m4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie5.m4")).group prec✝
• Data.instReprMovie5.repr Data.Movie5.m5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie5.m5")).group prec✝

@[implicit_reducible]

instance Data.instReprMovie5 : Repr Movie5

Equations

• Data.instReprMovie5 = { reprPrec := Data.instReprMovie5.repr }

@[implicit_reducible]

instance Data.instFintypeMovie5 : Fintype Movie5

Equations

• Data.instFintypeMovie5 = { elems := {Data.Movie5.m1, Data.Movie5.m2, Data.Movie5.m3, Data.Movie5.m4, Data.Movie5.m5}, complete := Data.instFintypeMovie5._proof_1 }

def 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

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

inductive Data.Boy4 : Type

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

@[implicit_reducible]

instance Data.instDecidableEqBoy4 : DecidableEq Boy4

Equations

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

def Data.instReprBoy4.repr : Boy4 → ℕ → Std.Format

Equations

• Data.instReprBoy4.repr Data.Boy4.b1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Boy4.b1")).group prec✝
• Data.instReprBoy4.repr Data.Boy4.b2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Boy4.b2")).group prec✝
• Data.instReprBoy4.repr Data.Boy4.b3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Boy4.b3")).group prec✝
• Data.instReprBoy4.repr Data.Boy4.b4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Boy4.b4")).group prec✝

@[implicit_reducible]

instance Data.instReprBoy4 : Repr Boy4

Equations

• Data.instReprBoy4 = { reprPrec := Data.instReprBoy4.repr }

@[implicit_reducible]

instance Data.instFintypeBoy4 : Fintype Boy4

Equations

• Data.instFintypeBoy4 = { elems := {Data.Boy4.b1, Data.Boy4.b2, Data.Boy4.b3, Data.Boy4.b4}, complete := Data.instFintypeBoy4._proof_1 }

inductive Data.Movie6 : Type

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

@[implicit_reducible]

instance Data.instDecidableEqMovie6 : DecidableEq Movie6

Equations

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

def Data.instReprMovie6.repr : Movie6 → ℕ → Std.Format

Equations

• Data.instReprMovie6.repr Data.Movie6.m1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie6.m1")).group prec✝
• Data.instReprMovie6.repr Data.Movie6.m2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie6.m2")).group prec✝
• Data.instReprMovie6.repr Data.Movie6.m3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie6.m3")).group prec✝
• Data.instReprMovie6.repr Data.Movie6.m4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie6.m4")).group prec✝
• Data.instReprMovie6.repr Data.Movie6.m5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie6.m5")).group prec✝
• Data.instReprMovie6.repr Data.Movie6.m6 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Movie6.m6")).group prec✝

@[implicit_reducible]

instance Data.instReprMovie6 : Repr Movie6

Equations

• Data.instReprMovie6 = { reprPrec := Data.instReprMovie6.repr }

@[implicit_reducible]

instance Data.instFintypeMovie6 : Fintype Movie6

Equations

• Data.instFintypeMovie6 = { elems := {Data.Movie6.m1, Data.Movie6.m2, Data.Movie6.m3, Data.Movie6.m4, Data.Movie6.m5, Data.Movie6.m6}, complete := Data.instFintypeMovie6._proof_1 }

def 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

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

def 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 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 Data.allBoys3 : List Boy3

Equations

• Data.allBoys3 = [Data.Boy3.b1, Data.Boy3.b2, Data.Boy3.b3]

def Data.allMovies5 : List Movie5

Equations

• Data.allMovies5 = [Data.Movie5.m1, Data.Movie5.m2, Data.Movie5.m3, Data.Movie5.m4, Data.Movie5.m5]

def Data.allBoys4 : List Boy4

Equations

• Data.allBoys4 = [Data.Boy4.b1, Data.Boy4.b2, Data.Boy4.b3, Data.Boy4.b4]

def Data.allMovies6 : List Movie6

Equations

• Data.allMovies6 = [Data.Movie6.m1, Data.Movie6.m2, Data.Movie6.m3, Data.Movie6.m4, Data.Movie6.m5, Data.Movie6.m6]

theorem 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 Data.scenarioA_pseudo_true : pseudoCumulativeReading scenarioA_saw allBoys3 allMovies5 3 5 = true

Scenario A: pseudo-cumulative reading is also TRUE.

theorem 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 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.