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

@cite{rullmann-1995} @cite{barwise-cooper-1981}

Connects standard quantifier denotations to the polarized individual decomposition from Core.Logic.PolarizedIndividuals, then derives the split-scope reading of negative quantifiers under modals.

Decomposition (§1)

The four corners of the square of opposition arise from entity-polarity pairs via the ConsGQ Boolean algebra:

• some = ⋁_e (e, +) — existential: at least one positive witness
• every = (⋁_e (e, -))ᶜ — universal: no negative witness
• no = (⋁_e (e, +))ᶜ — negative universal: no positive witness
• not_all = ⋁_e (e, -) — negative existential: at least one negative

The key compositional fact is pos_sup_neg: (e,+) ⊔ (e,-) = λR S. R(e), already proved in Core.Logic.PolarizedIndividuals.

Split Scope (§3-§4)

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

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

theorem Phenomena.Quantification.Studies.Elliott2025.some_as_polInd_join {α : Type u_1} (entities : List α) (R S : α → Prop) : (∃ e ∈ entities, R e ∧ S e) ↔ ∃ e ∈ entities, Core.Quantification.PolInd.toGQ (e, true) R S

On a concrete list of entities, some(R,S) = ⋁_e R(e) ∧ S(e), which is the join of positive polarized individuals.

theorem Phenomena.Quantification.Studies.Elliott2025.no_as_polInd_neg {α : Type u_1} (entities : List α) (R S : α → Prop) : (∀ e ∈ entities, ¬R e ∨ ¬S e) ↔ ∀ e ∈ entities, ¬Core.Quantification.PolInd.toGQ (e, true) R S

On a concrete list of entities, no(R,S) = ⋀_e ¬(R(e) ∧ S(e)), which is the meet of complements of positive polarized individuals.

theorem Phenomena.Quantification.Studies.Elliott2025.every_as_polInd_neg {α : Type u_1} (entities : List α) (R S : α → Prop) : (∀ e ∈ entities, ¬R e ∨ S e) ↔ ∀ e ∈ entities, ¬Core.Quantification.PolInd.toGQ (e, false) R S

On a concrete list, every(R,S) = ⋀_e ¬(R(e) ∧ ¬S(e)), which is the meet of complements of negative polarized individuals.

theorem Phenomena.Quantification.Studies.Elliott2025.inner_neg_swaps_polarity {α : Type u_1} (e : α) (R S : α → Prop) : (Core.Quantification.PolInd.toGQ (e, true) R fun (x : α) => ¬S x) ↔ Core.Quantification.PolInd.toGQ (e, false) R S

Inner negation (negating the scope) swaps the polarity of a polarized individual: ⟦(e,+)⟧(R, ¬S) ↔ ⟦(e,-)⟧(R, S).

theorem Phenomena.Quantification.Studies.Elliott2025.inner_neg_pos_list_eq_neg_list {α : Type u_1} (entities : List α) (R S : α → Prop) : (∃ e ∈ entities, Core.Quantification.PolInd.toGQ (e, true) R fun (x : α) => ¬S x) ↔ ∃ e ∈ entities, Core.Quantification.PolInd.toGQ (e, false) R S

Inner negation on a quantifier built from positive PolInds yields the corresponding negative-PolInd quantifier.

theorem Phenomena.Quantification.Studies.Elliott2025.dual_some_eq_every {α : Type u_1} (entities : List α) (R S : α → Prop) : (¬∃ e ∈ entities, R e ∧ ¬S e) ↔ ∀ e ∈ entities, ¬R e ∨ S e

Outer + inner negation = dual. Applied to some, this gives every: ¬some(R, ¬S) ↔ every(R, S).

theorem Phenomena.Quantification.Studies.Elliott2025.outer_neg_some_eq_no {α : Type u_1} (entities : List α) (R S : α → Prop) : (¬∃ e ∈ entities, R e ∧ S e) ↔ ∀ e ∈ entities, ¬R e ∨ ¬S e

Outer negation of some = no.

theorem Phenomena.Quantification.Studies.Elliott2025.split_scope {α : Type u_1} (e : α) : Core.Quantification.PolInd.toConsGQ (e, true) ⊔ Core.Quantification.PolInd.toConsGQ (e, false) = ⟨fun (R x : α → Prop) => R e, ⋯⟩

The split scope reading: (e,+) ⊔ (e,-) = λR S. R(e). Re-exported from Core.Logic.PolarizedIndividuals. The lattice-theoretic content of split scope: scope is "split" between the positive and negative polarities, yielding a quantifier that ignores scope entirely.

theorem Phenomena.Quantification.Studies.Elliott2025.split_scope_restrictor_only {α : Type u_1} (e : α) (R S₁ S₂ : α → Prop) : ↑(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 : α → Prop) : ↑(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 : α → Prop) : (¬∃ e ∈ entities, R e ∧ S e) ↔ ¬∃ e ∈ entities, 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 : α → Prop) : (¬∃ e ∈ entities, Core.Quantification.PolInd.toGQ (e, false) R S) ↔ ∀ e ∈ entities, ¬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.