Split Scope via Polarized Individuals @cite{elliott-2025}

@cite{rullmann-1995}

Connecting the polarized individual decomposition of determiners (Theories/Semantics/Lexical/Determiner/PolarizedIndividuals) to the empirical phenomenon of split scope.

Split Scope

Split scope arises when a quantifier's restrictor and scope are interpreted at different positions in the semantic derivation. The classic case is negative quantifiers under modals:

(1) You need to read no book. a. Surface: ¬∃x[book(x) ∧ need(read(x))] — "no" takes wide scope b. Split: need(¬∃x[book(x) ∧ read(x)]) — neg above, ∃ below

Reading (b) is the "split" reading: negation scopes above the modal while the existential restrictor scopes below it.

Lattice-Theoretic Analysis

@cite{elliott-2025} derives split scope from the polarized individual decomposition: no = (⋁_e (e,+))ᶜ. Since complement distributes over scope position changes, the negative and existential components can end up at different heights.

The key algebraic fact is pos_sup_neg: (e,+) ⊔ (e,-) = λR S. R(e) — the join of complementary polarities yields a quantifier that ignores scope entirely (it only checks the restrictor).

theorem Phenomena.Quantification.Studies.Elliott2025.split_scope_restrictor_only {α : Type u_1} (e : α) (R S₁ S₂ : α → Bool) : ↑(Core.Quantification.PolInd.toConsGQ (e, true) ⊔ Core.Quantification.PolInd.toConsGQ (e, false)) R S₁ = ↑(Core.Quantification.PolInd.toConsGQ (e, true) ⊔ Core.Quantification.PolInd.toConsGQ (e, false)) R S₂

The fundamental split-scope fact: joining complementary polarities yields a GQ that depends only on the restrictor, not the scope. This means scope position is irrelevant — the quantifier "splits".

theorem Phenomena.Quantification.Studies.Elliott2025.split_scope_eq_restrictor {α : Type u_1} (e : α) (R S : α → Bool) : ↑(Core.Quantification.PolInd.toConsGQ (e, true) ⊔ Core.Quantification.PolInd.toConsGQ (e, false)) R S = R e

Corollary: split scope means the result equals R(e) regardless of what scope predicate is supplied.

theorem Phenomena.Quantification.Studies.Elliott2025.no_from_complement_of_some {α : Type u_1} (entities : List α) (R S : α → Bool) : (!entities.any fun (e : α) => R e && S e) = !entities.any fun (e : α) => Core.Quantification.PolInd.toGQ (e, true) R S

A negative quantifier no(R,S) = ¬∃e. R(e) ∧ S(e) decomposes as the complement of the join of positive polarized individuals. When scope splits, the complement applies at one position while the existential restrictor applies at another.

theorem Phenomena.Quantification.Studies.Elliott2025.every_from_neg_polInd {α : Type u_1} (entities : List α) (R S : α → Bool) : (!entities.any fun (e : α) => Core.Quantification.PolInd.toGQ (e, false) R S) = entities.all fun (e : α) => !R e || S e

every arises from the dual of some: outer + inner negation. With polarized individuals: every(R,S) = ¬(⋁_e (e,-))(R,S), i.e., the complement of the join of negative polarized individuals. This decomposition parallels no but with reversed polarity.