Three-Way Comparison: Cumulative Readings

@cite{charlow-2021}

Compares three approaches to deriving cumulative readings of modified numerals:

Approach	Mechanism	Cumulative?	Extra machinery
Higher-order GQs	Continuations (Barker & Shan)	Yes	Cont monad, LOWER
Post-suppositions	Writer monad (Brasoveanu)	Yes	PostSupp type, reify
Update semantics	Non-distributive M_v	Yes	None beyond StateCCP

All three derive cumulative readings for Scenario A, but update semantics does so with the least additional stipulation — non-distributivity of M_v is a consequence of the update-theoretic architecture, not an add-on.

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

All three approaches derive the cumulative reading for Scenario A.

theorem Phenomena.Plurals.Compare.subtype_blocks_pseudo : ¬Semantics.Dynamic.DynamicGQ.SubtypePolymorphism.subtypeOf Semantics.Dynamic.DynamicGQ.SubtypePolymorphism.CardTest_type Semantics.Dynamic.DynamicGQ.SubtypePolymorphism.Mvar_type

The subtype polymorphism approach blocks pseudo-cumulative readings: CardTest_type (T) is NOT a subtype of Mvar_type (t).

theorem Phenomena.Plurals.Compare.dependent_indefinites_need_extra {W : Type u_1} {E : Type u_2} [Nonempty W] [Nonempty E] : ¬∀ (depIndef : Semantics.Dynamic.Core.StateCCP W E), Semantics.Dynamic.Core.IsDistributive depIndef

Dependent indefinites (Charlow §7.2) need something beyond update semantics alone — either higher-order GQs or post-suppositions are needed. Specifically, dependent indefinites cannot be typed as StateCCP.

Proof: the constant CCP fun _ => Set.univ is not distributive — it maps ∅ to Set.univ, but per-element processing of ∅ yields ∅.