Counting generalized quantifiers

[BC81] [KS86] [PW06] [Mos57]

[Fintype α]-gated specializations: counting quantifiers (most_sem, few_sem, half_sem, the at_*_n_sem family, the exceptive all_but_n_sem, between_n_m_sem, and the non-conservative counterexample m_sem), plus the cardinality-based Quantity and Proportional predicates and the bridge to model-agnostic QuantityInvariant.

Main declarations

• count — (Finset.univ.filter P).card over a Fintype carrier.
• Counting GQs (most_sem, few_sem, half_sem, both_sem, neither_sem, at_least_n_sem, at_most_n_sem, exactly_n_sem, all_but_n_sem, between_n_m_sem, m_sem).
• Quantity — cardinality-based isomorphism closure.
• Proportional — truth-value depends only on the ratio |A∩B|/|A\B|.

Relativized counting (the maximal-generality primitive)

countOn counts over an explicit Finset domain — decidable with no Fintype on the carrier. The whole-carrier count is its Finset.univ specialization (count := countOn Finset.univ). The threshold/prevalence operators (the cross-multiplied Nat predicate thresholdGtOn and its demoted ℚ view prevalenceOn, the analogue of Rel.edgeDensity) build on countOn.

def Quantification.countOn {α : Type u_1} (s : Finset α) (P : α → Prop) [DecidablePred P] : ℕ

Count of elements of s satisfying P. The Fintype-free counting primitive.

Equations

• Quantification.countOn s P = (Finset.filter P s).card

def Quantification.mostOn {α : Type u_1} (s : Finset α) (R S : α → Prop) [DecidablePred R] [DecidablePred S] : Prop

"most" over s: strictly more R∧S than R∧¬S in s. Division-free. mostOn Finset.univ = most_sem (mostOn_univ).

Equations

• Quantification.mostOn s R S = ((Quantification.countOn s fun (x : α) => R x ∧ S x) > Quantification.countOn s fun (x : α) => R x ∧ ¬S x)

def Quantification.thresholdOn {α : Type u_1} (s : Finset α) (R S : α → Prop) (num denom : ℕ) [DecidablePred R] [DecidablePred S] : Prop

Threshold (≥): at least num/denom of the R's in s are S. Cross-multiplied.

Equations

• Quantification.thresholdOn s R S num denom = ((denom * Quantification.countOn s fun (x : α) => R x ∧ S x) ≥ num * Quantification.countOn s R)

def Quantification.thresholdGtOn {α : Type u_1} (s : Finset α) (R S : α → Prop) (num denom : ℕ) [DecidablePred R] [DecidablePred S] : Prop

Threshold (>): more than num/denom of the R's in s are S. Cross-multiplied.

Equations

• Quantification.thresholdGtOn s R S num denom = ((denom * Quantification.countOn s fun (x : α) => R x ∧ S x) > num * Quantification.countOn s R)

def Quantification.prevalenceOn {α : Type u_1} (s : Finset α) (R S : α → Prop) [DecidablePred R] [DecidablePred S] : ℚ

The ℚ prevalence view (analogue of Rel.edgeDensity): proportion of R-in-s that are S. The derived numeric value; related to thresholdGtOn by thresholdGtOn_iff_prevalenceOn.

Equations

• Quantification.prevalenceOn s R S = if Quantification.countOn s R = 0 then 0 else ↑(Quantification.countOn s fun (x : α) => R x ∧ S x) / ↑(Quantification.countOn s R)

@[implicit_reducible]

instance Quantification.mostOn.decidable {α : Type u_1} (s : Finset α) (R S : α → Prop) [DecidablePred R] [DecidablePred S] : Decidable (mostOn s R S)

Equations

• Quantification.mostOn.decidable s R S = id inferInstance

@[implicit_reducible]

instance Quantification.thresholdOn.decidable {α : Type u_1} (s : Finset α) (R S : α → Prop) (num denom : ℕ) [DecidablePred R] [DecidablePred S] : Decidable (thresholdOn s R S num denom)

Equations

• Quantification.thresholdOn.decidable s R S num denom = id inferInstance

@[implicit_reducible]

instance Quantification.thresholdGtOn.decidable {α : Type u_1} (s : Finset α) (R S : α → Prop) (num denom : ℕ) [DecidablePred R] [DecidablePred S] : Decidable (thresholdGtOn s R S num denom)

Equations

• Quantification.thresholdGtOn.decidable s R S num denom = id inferInstance

theorem Quantification.countOn_decompose {α : Type u_1} (s : Finset α) (R S : α → Prop) [DecidablePred R] [DecidablePred S] : countOn s R = (countOn s fun (x : α) => R x ∧ S x) + countOn s fun (x : α) => R x ∧ ¬S x

|s∩R| = |s∩R∩S| + |s∩R\S|.

theorem Quantification.thresholdGtOn_iff_prevalenceOn {α : Type u_1} (s : Finset α) (R S : α → Prop) [DecidablePred R] [DecidablePred S] (num denom : ℕ) (hdenom : 0 < denom) (hR : 0 < countOn s R) : thresholdGtOn s R S num denom ↔ prevalenceOn s R S > ↑num / ↑denom

The division-free thresholdGtOn agrees with "prevalenceOn exceeds num/denom", justifying the demotion of the ℚ ratio to a derived view.

theorem Quantification.thresholdGtOn_one_two_iff_mostOn {α : Type u_1} (s : Finset α) (R S : α → Prop) [DecidablePred R] [DecidablePred S] : thresholdGtOn s R S 1 2 ↔ mostOn s R S

"More than half" is exactly "most": thresholdGtOn s R S 1 2 (more than 1/2 of the R's in s are S) coincides with mostOn s R S (strictly more R∧S than R∧¬S). Both are division-free Nat comparisons; the bridge is countOn_decompose. The threshold 1/2 is special because it is the cutpoint at the 1 : 1 cell ratio.

The relativized ∀/∃ companions of Basic's whole-carrier every_sem/ some_sem/no_sem: bounded over an explicit Finset, hence decidable with no Fintype (Finset.decidableDforallFinset). They are not duplicates of the _sem denotations — every_sem ranges over the whole (possibly infinite) carrier for the general GQ theory, whereas everyOn s ranges over s; the two meet at s = Finset.univ (everyOn_univ).

def Quantification.everyOn {α : Type u_1} (s : Finset α) (R S : α → Prop) : Prop

s-relativized restricted universal: every R in s is S.

Equations

• Quantification.everyOn s R S = ∀ x ∈ s, R x → S x

def Quantification.someOn {α : Type u_1} (s : Finset α) (R S : α → Prop) : Prop

s-relativized existential.

Equations

• Quantification.someOn s R S = ∃ x ∈ s, R x ∧ S x

def Quantification.noOn {α : Type u_1} (s : Finset α) (R S : α → Prop) : Prop

s-relativized no.

Equations

• Quantification.noOn s R S = ∀ x ∈ s, R x → ¬S x

@[implicit_reducible]

instance Quantification.everyOn.decidable {α : Type u_1} (s : Finset α) (R S : α → Prop) [DecidablePred R] [DecidablePred S] : Decidable (everyOn s R S)

Equations

• Quantification.everyOn.decidable s R S = id inferInstance

@[implicit_reducible]

instance Quantification.someOn.decidable {α : Type u_1} (s : Finset α) (R S : α → Prop) [DecidablePred R] [DecidablePred S] : Decidable (someOn s R S)

Equations

• Quantification.someOn.decidable s R S = id inferInstance

@[implicit_reducible]

instance Quantification.noOn.decidable {α : Type u_1} (s : Finset α) (R S : α → Prop) [DecidablePred R] [DecidablePred S] : Decidable (noOn s R S)

Equations

• Quantification.noOn.decidable s R S = id inferInstance

def Quantification.count {α : Type u_1} [Fintype α] (P : α → Prop) [DecidablePred P] : ℕ

Count of elements satisfying a predicate, via Finset.univ.filter. The Finset.univ specialization of countOn.

Equations

• Quantification.count P = Quantification.countOn Finset.univ P

Whole-carrier recovery (s = Finset.univ)

The relativized ∀/∃ operators reduce to Basic's whole-carrier denotations at s = univ, exhibiting them as the general layer's finite specialization.

@[simp]

theorem Quantification.everyOn_univ {α : Type u_1} [Fintype α] (R S : α → Prop) : everyOn Finset.univ R S ↔ every_sem R S

@[simp]

theorem Quantification.someOn_univ {α : Type u_1} [Fintype α] (R S : α → Prop) : someOn Finset.univ R S ↔ some_sem R S

@[simp]

theorem Quantification.noOn_univ {α : Type u_1} [Fintype α] (R S : α → Prop) : noOn Finset.univ R S ↔ no_sem R S

Counting denotations

noncomputable def Quantification.most_sem {α : Type u_1} [Fintype α] : GQ α

⟦most⟧(R)(S) = |R ∩ S| > |R \ S|.

Equations

• Quantification.most_sem R S = ((Quantification.count fun (x : α) => R x ∧ S x) > Quantification.count fun (x : α) => R x ∧ ¬S x)

noncomputable def Quantification.few_sem {α : Type u_1} [Fintype α] : GQ α

⟦few⟧(R)(S) = |R ∩ S| < |R \ S|. Dual of most_sem.

Equations

• Quantification.few_sem R S = ((Quantification.count fun (x : α) => R x ∧ S x) < Quantification.count fun (x : α) => R x ∧ ¬S x)

noncomputable def Quantification.half_sem {α : Type u_1} [Fintype α] : GQ α

⟦half⟧(R)(S) = 2 * |R ∩ S| = |R|.

Equations

• Quantification.half_sem R S = ((2 * Quantification.count fun (x : α) => R x ∧ S x) = Quantification.count fun (x : α) => R x)

noncomputable def Quantification.both_sem {α : Type u_1} [Fintype α] : GQ α

⟦both⟧(R)(S) = ⟦every⟧(R)(S) ∧ |R| ≥ 2. K&S §2.3.

Equations

• Quantification.both_sem R S = (Quantification.every_sem R S ∧ {x : α | R x}.card ≥ 2)

noncomputable def Quantification.neither_sem {α : Type u_1} [Fintype α] : GQ α

⟦neither⟧ = gqMeet ⟦no⟧ (|R| ≥ 2). K&S (83b).

Equations

• Quantification.neither_sem = Quantification.gqMeet Quantification.no_sem fun (R x : α → Prop) => {x : α | R x}.card ≥ 2

noncomputable def Quantification.at_least_n_sem {α : Type u_1} [Fintype α] (n : ℕ) : GQ α

⟦at least n⟧(R)(S) = |R ∩ S| ≥ n.

Equations

• Quantification.at_least_n_sem n R S = ((Quantification.count fun (x : α) => R x ∧ S x) ≥ n)

noncomputable def Quantification.at_most_n_sem {α : Type u_1} [Fintype α] (n : ℕ) : GQ α

⟦at most n⟧(R)(S) = |R ∩ S| ≤ n.

Equations

• Quantification.at_most_n_sem n R S = ((Quantification.count fun (x : α) => R x ∧ S x) ≤ n)

noncomputable def Quantification.exactly_n_sem {α : Type u_1} [Fintype α] (n : ℕ) : GQ α

⟦exactly n⟧(R)(S) = |R ∩ S| = n.

Equations

• Quantification.exactly_n_sem n R S = ((Quantification.count fun (x : α) => R x ∧ S x) = n)

noncomputable def Quantification.all_but_n_sem {α : Type u_1} [Fintype α] (n : ℕ) : GQ α

⟦all but n⟧(R)(S) = |R \ S| = n. The exceptive counterpart of exactly_n_sem; generalizes "every" (= all but 0).

Equations

• Quantification.all_but_n_sem n R S = ((Quantification.count fun (x : α) => R x ∧ ¬S x) = n)

noncomputable def Quantification.between_n_m_sem {α : Type u_1} [Fintype α] (n k : ℕ) : GQ α

⟦between n and k⟧(R)(S) = n ≤ |R ∩ S| ≤ k.

Equations

• Quantification.between_n_m_sem n k = Quantification.gqMeet (Quantification.at_least_n_sem n) (Quantification.at_most_n_sem k)

noncomputable def Quantification.m_sem {α : Type u_1} [Fintype α] : GQ α

A non-conservative quantifier for contrast: ⟦M⟧(A,B) = |A| > |B| (van de Pol et al.'s hypothetical counterpart to "most").

Equations

• Quantification.m_sem R S = ((Quantification.count fun (x : α) => R x) > Quantification.count fun (x : α) => S x)

count helpers

theorem Quantification.count_bij_inv {α : Type u_1} [Fintype α] (f : α → α) (hBij : Function.Bijective f) {P : α → Prop} [DecidablePred P] : count P = count (P ∘ f)

count P = count (P ∘ f) when f is a bijection.

theorem Quantification.count_congr_iff {α : Type u_1} [Fintype α] {P Q : α → Prop} [DecidablePred P] [DecidablePred Q] (h : ∀ (x : α), P x ↔ Q x) : count P = count Q

Equivalent predicates produce equal counts.

theorem Quantification.count_and_idem_any {α : Type u_1} [Fintype α] (R S : α → Prop) (inst1 : DecidablePred fun (x : α) => R x ∧ S x) (inst2 : DecidablePred fun (x : α) => R x ∧ R x ∧ S x) : (count fun (x : α) => R x ∧ S x) = count fun (x : α) => R x ∧ R x ∧ S x

Instance-polymorphic: count(R∧S) = count(R∧(R∧S)) for any DecidablePred instances.

theorem Quantification.count_neg_idem_any {α : Type u_1} [Fintype α] (R S : α → Prop) (inst1 : DecidablePred fun (x : α) => R x ∧ ¬S x) (inst2 : DecidablePred fun (x : α) => R x ∧ ¬(R x ∧ S x)) : (count fun (x : α) => R x ∧ ¬S x) = count fun (x : α) => R x ∧ ¬(R x ∧ S x)

Instance-polymorphic: count(R∧¬S) = count(R∧¬(R∧S)) for any DecidablePred instances.

theorem Quantification.count_le_of_imp {α : Type u_1} [Fintype α] {P Q : α → Prop} [DecidablePred P] [DecidablePred Q] (h : ∀ (x : α), P x → Q x) : count P ≤ count Q

If P implies Q pointwise, then |filter P| ≤ |filter Q|.

theorem Quantification.count_decompose {α : Type u_1} [Fintype α] (R S : α → Prop) [DecidablePred R] [DecidablePred S] : (count fun (x : α) => R x) = (count fun (x : α) => R x ∧ S x) + count fun (x : α) => R x ∧ ¬S x

|R| = |R∩S| + |R\S|.

Conservativity of counting GQs

theorem Quantification.most_conservative {α : Type u_1} [Fintype α] : Conservative most_sem

theorem Quantification.few_conservative {α : Type u_1} [Fintype α] : Conservative few_sem

theorem Quantification.half_conservative {α : Type u_1} [Fintype α] : Conservative half_sem

theorem Quantification.both_conservative {α : Type u_1} [Fintype α] : Conservative both_sem

theorem Quantification.neither_conservative {α : Type u_1} [Fintype α] : Conservative neither_sem

theorem Quantification.at_least_n_conservative {α : Type u_1} [Fintype α] (n : ℕ) : Conservative (at_least_n_sem n)

theorem Quantification.at_most_n_conservative {α : Type u_1} [Fintype α] (n : ℕ) : Conservative (at_most_n_sem n)

theorem Quantification.exactly_n_conservative {α : Type u_1} [Fintype α] (n : ℕ) : Conservative (exactly_n_sem n)

theorem Quantification.all_but_n_conservative {α : Type u_1} [Fintype α] (n : ℕ) : Conservative (all_but_n_sem n)

theorem Quantification.between_n_m_conservative {α : Type u_1} [Fintype α] (n k : ℕ) : Conservative (between_n_m_sem n k)

Counting quantifier identities ([PW06] §4.3)

theorem Quantification.some_eq_at_least_1 {α : Type u_1} [Fintype α] : some_sem = at_least_n_sem 1

⟦some⟧ = ⟦at least 1⟧.

theorem Quantification.at_most_eq_outerNeg_at_least_succ {α : Type u_1} [Fintype α] (n : ℕ) : at_most_n_sem n = outerNeg (at_least_n_sem (n + 1))

⟦at most n⟧ = outerNeg ⟦at least n+1⟧.

theorem Quantification.no_eq_at_most_0 {α : Type u_1} [Fintype α] : no_sem = at_most_n_sem 0

⟦no⟧ = ⟦at most 0⟧.

theorem Quantification.exactly_eq_meet_at_least_at_most {α : Type u_1} [Fintype α] (n : ℕ) : exactly_n_sem n = gqMeet (at_least_n_sem n) (at_most_n_sem n)

⟦exactly n⟧ = ⟦at least n⟧ ⊓ ⟦at most n⟧.

theorem Quantification.all_but_0_eq_every {α : Type u_1} [Fintype α] : all_but_n_sem 0 = every_sem

⟦all but 0⟧ = ⟦every⟧.

Scope monotonicity of counting GQs

theorem Quantification.few_scope_down {α : Type u_1} [Fintype α] : ScopeDownwardMono few_sem

theorem Quantification.most_scope_up {α : Type u_1} [Fintype α] : ScopeUpwardMono most_sem

theorem Quantification.at_least_n_scope_up {α : Type u_1} [Fintype α] (n : ℕ) : ScopeUpwardMono (at_least_n_sem n)

theorem Quantification.at_most_n_scope_down {α : Type u_1} [Fintype α] (n : ℕ) : ScopeDownwardMono (at_most_n_sem n)

Smoothness

theorem Quantification.most_downNE {α : Type u_1} [Fintype α] : DownNEMon most_sem

theorem Quantification.most_upSE {α : Type u_1} [Fintype α] : UpSEMon most_sem

theorem Quantification.most_smooth {α : Type u_1} [Fintype α] : Smooth most_sem

theorem Quantification.at_least_n_restrictor_up {α : Type u_1} [Fintype α] (n : ℕ) : RestrictorUpwardMono (at_least_n_sem n)

theorem Quantification.at_least_n_downNE {α : Type u_1} [Fintype α] (n : ℕ) : DownNEMon (at_least_n_sem n)

theorem Quantification.at_least_n_smooth {α : Type u_1} [Fintype α] (n : ℕ) : Smooth (at_least_n_sem n)

theorem Quantification.at_most_n_restrictor_down {α : Type u_1} [Fintype α] (n : ℕ) : RestrictorDownwardMono (at_most_n_sem n)

theorem Quantification.at_most_n_coSmooth {α : Type u_1} [Fintype α] (n : ℕ) : CoSmooth (at_most_n_sem n)

Quantity / isomorphism closure ([Mos57])

Cardinality-based, Fintype-gated. quantityInvariant_of_quantity and quantity_of_quantityInvariant bridge to the model-agnostic QuantityInvariant (in Defs.lean): the four Venn cells are the fibers of the Bool × Bool code x ↦ (decide (R x), decide (S x)), and equal cell cardinalities glue (Equiv.ofFiberEquiv) into a domain bijection.

def Quantification.Quantity {α : Type u_1} [Fintype α] (q : GQ α) : Prop

Quantity / isomorphism closure: Q(A, B) depends only on the four cardinalities |A ∩ B|, |A \ B|, |B \ A|, |M \ (A ∪ B)|. Type-⟨1,1⟩ generalization of [Mos57]'s permutation invariance for type-⟨1⟩ quantifiers, due to [vB84].

Equations

• One or more equations did not get rendered due to their size.

theorem Quantification.quantityInvariant_of_quantity {α : Type u_1} [Fintype α] (q : GQ α) (hQ : Quantity q) : QuantityInvariant q

Quantity → QuantityInvariant: cardinality-dependence implies bijection-invariance. Each cell count of (A', B') equals the corresponding cell count of (A, B): the bijection f maps the (A', B')-cell into the (A, B)-cell (membership transported by the A ∘ f ↔ A', B ∘ f ↔ B' hypotheses), so the filters have equal card.

theorem Quantification.quantity_of_quantityInvariant {α : Type u_1} [Fintype α] [DecidableEq α] (q : GQ α) (hQ : QuantityInvariant q) : Quantity q

QuantityInvariant → Quantity: bijection-invariance implies cardinality-dependence. Equal cell cardinalities give, cell by cell, an equivalence of cellCode fibers (Fintype.equivOfCardEq); gluing the four over the partition of α (Equiv.ofFiberEquiv) yields a bijection f with R₁ ∘ f ↔ R₂ and S₁ ∘ f ↔ S₂, to which hQ applies.

Quantity closure

theorem Quantification.quantity_outerNeg {α : Type u_1} [Fintype α] [DecidableEq α] (q : GQ α) (h : Quantity q) : Quantity (outerNeg q)

theorem Quantification.quantity_gqMeet {α : Type u_1} [Fintype α] [DecidableEq α] (q₁ q₂ : GQ α) (h₁ : Quantity q₁) (h₂ : Quantity q₂) : Quantity (gqMeet q₁ q₂)

Quantity of concrete GQs

theorem Quantification.at_least_n_quantity {α : Type u_1} [Fintype α] [DecidableEq α] (n : ℕ) : Quantity (at_least_n_sem n)

theorem Quantification.at_most_n_quantity {α : Type u_1} [Fintype α] [DecidableEq α] (n : ℕ) : Quantity (at_most_n_sem n)

theorem Quantification.exactly_n_quantity {α : Type u_1} [Fintype α] [DecidableEq α] (n : ℕ) : Quantity (exactly_n_sem n)

theorem Quantification.some_quantity {α : Type u_1} [Fintype α] [DecidableEq α] : Quantity some_sem

theorem Quantification.no_quantity {α : Type u_1} [Fintype α] [DecidableEq α] : Quantity no_sem

theorem Quantification.every_quantity {α : Type u_1} [Fintype α] [DecidableEq α] : Quantity every_sem

theorem Quantification.most_quantity {α : Type u_1} [Fintype α] [DecidableEq α] : Quantity most_sem

theorem Quantification.few_quantity {α : Type u_1} [Fintype α] [DecidableEq α] : Quantity few_sem

theorem Quantification.half_quantity {α : Type u_1} [Fintype α] [DecidableEq α] : Quantity half_sem

theorem Quantification.all_but_n_quantity {α : Type u_1} [Fintype α] [DecidableEq α] (n : ℕ) : Quantity (all_but_n_sem n)

theorem Quantification.between_n_m_quantity {α : Type u_1} [Fintype α] [DecidableEq α] (n k : ℕ) : Quantity (between_n_m_sem n k)

Satisfies universals (counting)

theorem Quantification.most_satisfiesUniversals {α : Type u_1} [Fintype α] [DecidableEq α] : SatisfiesUniversals most_sem

theorem Quantification.few_satisfiesUniversals {α : Type u_1} [Fintype α] [DecidableEq α] : SatisfiesUniversals few_sem

theorem Quantification.at_least_n_satisfiesUniversals {α : Type u_1} [Fintype α] [DecidableEq α] (n : ℕ) : SatisfiesUniversals (at_least_n_sem n)

theorem Quantification.at_most_n_satisfiesUniversals {α : Type u_1} [Fintype α] [DecidableEq α] (n : ℕ) : SatisfiesUniversals (at_most_n_sem n)

Proportional quantifiers ([PW06] §4.3)

def Quantification.Proportional {α : Type u_1} [Fintype α] (q : GQ α) : Prop

Proportional: q's truth value depends only on the ratio |A∩B|/|A\B|.

Equations

• One or more equations did not get rendered due to their size.

theorem Quantification.most_proportional {α : Type u_1} [Fintype α] [DecidableEq α] : Proportional most_sem

theorem Quantification.few_proportional {α : Type u_1} [Fintype α] [DecidableEq α] : Proportional few_sem

theorem Quantification.half_proportional {α : Type u_1} [Fintype α] [DecidableEq α] : Proportional half_sem

Proportional ⇒ not intersective / not monotone (witnessed counterexamples)

The proportional determiners most, few, half are not intersective: they fail the Existential property (felicity in there-sentences), even though B&C's Table II labels few/half "weak". Existential q (q R S ↔ q (R∩S) ⊤) is false for them because the truth value depends on |R∖S|, not just on |R∩S|. Refuting it needs a domain with |α| ≥ 3 (over Fin 1/Fin 2 most is vacuously Existential), so the witnessed statements pin α := Fin 3. half is moreover non-monotone in scope (goes true→false as the scope grows), and most is not symmetric.

theorem Quantification.count_eq_decidable {α : Type u_1} [Fintype α] [DecidableEq α] (P : α → Prop) (inst' : DecidablePred P) [DecidablePred P] : count P = count P

count is independent of the chosen DecidablePred instance: any instance equals the canonical synthesized one. Lets the classical-DecidablePred count frozen into the counting denotations be evaluated by decide.

theorem Quantification.not_existential_most_sem : ¬Existential most_sem

most is proportional, not intersective: it fails Existential. Witness over Fin 3: R = ⊤, S = {0} gives |R∩S| = 1, |R∖S| = 2, so most R S is false (1 > 2 fails) while most (R∩S) ⊤ is true (|R∩S| = 1 > 0).

theorem Quantification.not_existential_few_sem : ¬Existential few_sem

few is proportional, not intersective: it fails Existential, despite B&C's "weak" label. Witness over Fin 3: R = ⊤, S = {0} gives |R∩S| = 1 < |R∖S| = 2, so few R S is true while few (R∩S) ⊤ is false (|R∩S| < |∅| = 0 is impossible).

theorem Quantification.not_existential_half_sem : ¬Existential half_sem

half is proportional, not intersective: it fails Existential, despite B&C's "weak" label. Witness over Fin 3: R = {0,1}, S = {0} gives half R S true (2·|R∩S| = 2 = |R|) while half (R∩S) ⊤ requires |R∩S| = 0, false.

theorem Quantification.half_not_scopeUp : ¬ScopeUpwardMono half_sem

half is not scope-upward-monotone. Witness over Fin 3: R = {0,1}, S = {0} ⊆ S' = {0,1}; half R S is true (2·1 = 2 = |R|) but half R S' is false (2·2 = 4 ≠ 2) — growing the scope flips it true→false.

theorem Quantification.half_not_scopeDown : ¬ScopeDownwardMono half_sem

half is not scope-downward-monotone. Witness over Fin 3: R = {0,1}, S = ∅ ⊆ S' = {0}; half R S' is true (2·1 = 2 = |R|) but half R S is false (2·0 = 0 ≠ 2) — shrinking the scope flips it true→false.

theorem Quantification.half_not_monotone : ¬ScopeUpwardMono half_sem ∧ ¬ScopeDownwardMono half_sem

half is non-monotone in scope: neither scope-upward nor scope-downward monotone ([vdPLvM+23]).

theorem Quantification.not_qsymmetric_most_sem : ¬QSymmetric most_sem

most is not symmetric: most R S ↔ most S R fails. Witness over Fin 3: R = {0}, S = {0,1}; most R S is true (|R∩S| = 1 > |R∖S| = 0) but most S R is false (|S∩R| = 1 > |S∖R| = 1 fails).

Whole-carrier recovery for mostOn and inherited proportionality

mostOn Finset.univ is the s = Finset.univ fibre of the relativized most, matching the whole-carrier most_sem (modulo the DecidablePred-instance bridge Finset.filter_congr_decidable). The Proportional theorem proved for most_sem therefore transfers to it by inheritance, not re-proof.

@[simp]

theorem Quantification.mostOn_univ {α : Type u_1} [Fintype α] (R S : α → Prop) [DecidablePred R] [DecidablePred S] : mostOn Finset.univ R S ↔ most_sem R S

theorem Quantification.mostOn_univ_proportional {α : Type u_1} [Fintype α] : Proportional fun (R S : α → Prop) => mostOn Finset.univ R S

mostOn at the whole carrier is proportional — inherited from most_proportional, not re-proved: at s = Finset.univ the relativized mostOn IS most_sem.