Determiners via Polarized Individuals @cite{elliott-2025}

@cite{barwise-cooper-1981}

Connects standard quantifier denotations to the polarized individual decomposition from Core.Logic.PolarizedIndividuals.

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 for split scope is pos_sup_neg: (e,+) ⊔ (e,-) = λR S. R(e), already proved in Core.Logic.PolarizedIndividuals.

theorem Semantics.Lexical.Determiner.Polarized.some_as_polInd_join {α : 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

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

theorem Semantics.Lexical.Determiner.Polarized.no_as_polInd_neg {α : Type u_1} (entities : List α) (R S : α → Bool) : (entities.all fun (e : α) => !R e || !S e) = entities.all fun (e : α) => !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 Semantics.Lexical.Determiner.Polarized.every_as_polInd_neg {α : Type u_1} (entities : List α) (R S : α → Bool) : (entities.all fun (e : α) => !R e || S e) = entities.all fun (e : α) => !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 Semantics.Lexical.Determiner.Polarized.inner_neg_swaps_polarity {α : Type u_1} (e : α) (R S : α → Bool) : (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 Semantics.Lexical.Determiner.Polarized.inner_neg_pos_list_eq_neg_list {α : Type u_1} (entities : List α) (R S : α → Bool) : (entities.any fun (e : α) => Core.Quantification.PolInd.toGQ (e, true) R fun (x : α) => !S x) = entities.any fun (e : α) => Core.Quantification.PolInd.toGQ (e, false) R S

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

theorem Semantics.Lexical.Determiner.Polarized.dual_some_eq_every {α : Type u_1} (entities : List α) (R S : α → Bool) : (!entities.any fun (e : α) => R e && !S e) = entities.all fun (e : α) => !R e || S e

theorem Semantics.Lexical.Determiner.Polarized.outer_neg_some_eq_no {α : Type u_1} (entities : List α) (R S : α → Bool) : (!entities.any fun (e : α) => R e && S e) = entities.all fun (e : α) => !R e || !S e

Outer negation of some = no: ¬(∃e. R(e) ∧ S(e)) = ∀e. R(e) → ¬S(e).

theorem Semantics.Lexical.Determiner.Polarized.split_scope {α : Type u_1} (e : α) : Core.Quantification.PolInd.toConsGQ (e, true) ⊔ Core.Quantification.PolInd.toConsGQ (e, false) = ⟨fun (R x : α → Bool) => R e, ⋯⟩

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