Generalized Quantifier Properties — Theorems #

@cite{barwise-cooper-1981} @cite{keenan-stavi-1986} @cite{peters-westerstahl-2006} @cite{van-benthem-1984} @cite{van-benthem-1986} @cite{icard-2012}

Theorems about GQ properties: duality, conservativity/symmetry/strength, left monotonicity and smoothness, Boolean closure, type ⟨1⟩ theorems, van Benthem characterization, and entailment-signature bridge.

source

theorem Core.Quantification.outerNeg_up_to_down {α : Type u_1} (q : GQ α) (h : ScopeUpwardMono q) :

ScopeDownwardMono (outerNeg q)

Outer negation reverses scope monotonicity: mon↑ → mon↓. B&C Theorem C9.

source

theorem Core.Quantification.outerNeg_down_to_up {α : Type u_1} (q : GQ α) (h : ScopeDownwardMono q) :

ScopeUpwardMono (outerNeg q)

Outer negation reverses scope monotonicity: mon↓ → mon↑. B&C Theorem C9.

source

theorem Core.Quantification.innerNeg_up_to_down {α : Type u_1} (q : GQ α) (h : ScopeUpwardMono q) :

ScopeDownwardMono (innerNeg q)

Inner negation reverses scope monotonicity: mon↑ → mon↓ (B&C §4.11).

source

theorem Core.Quantification.innerNeg_down_to_up {α : Type u_1} (q : GQ α) (h : ScopeDownwardMono q) :

ScopeUpwardMono (innerNeg q)

Inner negation reverses scope monotonicity: mon↓ → mon↑ (B&C §4.11). Mirrors innerNeg_up_to_down. Proof: contrapose S⊆S' to ¬S'⊆¬S.

source

theorem Core.Quantification.outerNeg_restrictorUp_to_down {α : Type u_1} (q : GQ α) (h : RestrictorUpwardMono q) :

RestrictorDownwardMono (outerNeg q)

Outer negation reverses restrictor monotonicity: mon↑ → mon↓.

source

theorem Core.Quantification.outerNeg_restrictorDown_to_up {α : Type u_1} (q : GQ α) (h : RestrictorDownwardMono q) :

RestrictorUpwardMono (outerNeg q)

Outer negation reverses restrictor monotonicity: mon↓ → mon↑.

source

theorem Core.Quantification.outerNeg_involution {α : Type u_1} (q : GQ α) :

outerNeg (outerNeg q) = q

Outer negation is involutive: ~~Q = Q.

source

theorem Core.Quantification.innerNeg_involution {α : Type u_1} (q : GQ α) :

innerNeg (innerNeg q) = q

Inner negation is involutive: Q~~ = Q.

source

theorem Core.Quantification.dualQ_involution {α : Type u_1} (q : GQ α) :

dualQ (dualQ q) = q

Dual is involutive: Q̌̌ = Q.

source

theorem Core.Quantification.quantityInvariant_outerNeg {α : Type u_1} (q : GQ α) (h : QuantityInvariant q) :

QuantityInvariant (outerNeg q)

Outer negation preserves QuantityInvariant: if Q is bijection-invariant, so is ~Q.

source

theorem Core.Quantification.quantityInvariant_innerNeg {α : Type u_1} (q : GQ α) (h : QuantityInvariant q) :

QuantityInvariant (innerNeg q)

Inner negation preserves QuantityInvariant: if Q is bijection-invariant, so is Q~.

source

theorem Core.Quantification.quantityInvariant_dualQ {α : Type u_1} (q : GQ α) (h : QuantityInvariant q) :

QuantityInvariant (dualQ q)

Dual preserves QuantityInvariant.

source

theorem Core.Quantification.quantityInvariant_gqMeet {α : Type u_1} (f g : GQ α) (hf : QuantityInvariant f) (hg : QuantityInvariant g) :

QuantityInvariant (gqMeet f g)

Meet preserves QuantityInvariant.

source

theorem Core.Quantification.intersection_conservative_symmetric {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hInt : IntersectionCondition q) :

QSymmetric q

Conservative + intersection condition → symmetric (B&C Theorem C5). Proof: by conservativity Q(A,B) = Q(A, A∩B) and Q(B,A) = Q(B, B∩A); both have the same restrictor∩scope = A∩B, so intersection condition equates them.

source

theorem Core.Quantification.co_property_mono {α : Type u_1} (q : GQ α) :

ScopeDownwardMono q ↔ ScopeUpwardMono (innerNeg q)

Scope-downward monotonicity is equivalent to scope-upward monotonicity of the inner negation (co-property characterization, P&W §3.2.4).

source

theorem Core.Quantification.conserv_symm_iff_int {α : Type u_1} (q : GQ α) (hCons : Conservative q) :

QSymmetric q ↔ IntersectionCondition q

Under conservativity, symmetric ↔ intersective (P&W Ch.6 Fact 1). This is the single most important bridge theorem — it explains why weak determiners allow there-insertion.

source

theorem Core.Quantification.symm_not_positive_strong {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hSym : QSymmetric q) (hNontrivF : ∃ (R : α → Bool) (S : α → Bool), q R S = false) :

¬PositiveStrong q

Non-trivial symmetric quantifiers are not positive strong (P&W Ch.6 Fact 7).

source

theorem Core.Quantification.conservative_iff_livesOn {α : Type u_1} (q : GQ α) :

Conservative q ↔ ∀ (A : α → Bool), LivesOn (restrict q A) A

Conservativity of a GQ is equivalent to its restricted quantifiers living on their restrictors (P&W §3.2.2).

source

theorem Core.Quantification.extension_trivial {α : Type u_1} (q : GQ α) :

Extension q

Every GQ α satisfies Extension: the representation is universe-free.

source

theorem Core.Quantification.vanBenthem_cons_ext {α : Type u_1} (q : GQ α) :

Extension q → (Conservative q ↔ ∀ (A : α → Bool), LivesOn (restrict q A) A)

@cite{van-benthem-1984}: Under Extension (free for GQ α), Conservativity is equivalent to LivesOn — the restricted quantifier depends only on elements of its restrictor. This is the CONS + EXT ↔ Rel(⟨1⟩) characterization of "well-behaved" type ⟨1,1⟩ quantifiers.

Our conservative_iff_livesOn doesn't need an EXT hypothesis because GQ α already bakes it.

source

theorem Core.Quantification.restrictorUpMono_to_upSE {α : Type u_1} (q : GQ α) (h : RestrictorUpwardMono q) :

UpSEMon q

Persistence → ↑_SE Mon (trivial: ↑_SE conditions are a special case of A⊆A').

source

theorem Core.Quantification.restrictorUpMono_to_upSW {α : Type u_1} (q : GQ α) (h : RestrictorUpwardMono q) :

UpSWMon q

Persistence → ↑_SW Mon (trivial: ↑_SW conditions are a special case of A⊆A').

source

theorem Core.Quantification.upSW_upSE_to_restrictorUpMono {α : Type u_1} (q : GQ α) (hSW : UpSWMon q) (hSE : UpSEMon q) :

RestrictorUpwardMono q

↑_SW Mon ∧ ↑_SE Mon → Persistence (@cite{peters-westerstahl-2006} Prop 6).

Proof: extend A to A' in two steps via A'' = A ∪ (A'\B). Step 1: A⊆A'' with A∩B = A''∩B (new elements are outside B) — apply ↑_SW. Step 2: A''⊆A' with A''\B = A'\B (same elements outside B) — apply ↑_SE.

source

theorem Core.Quantification.persistent_iff_upSW_and_upSE {α : Type u_1} (q : GQ α) :

RestrictorUpwardMono q ↔ UpSWMon q ∧ UpSEMon q

Persistence ↔ ↑_SW Mon ∧ ↑_SE Mon (@cite{peters-westerstahl-2006} Prop 6).

source

theorem Core.Quantification.restrictorDownMono_to_downNW {α : Type u_1} (q : GQ α) (h : RestrictorDownwardMono q) :

DownNWMon q

Anti-persistence → ↓_NW Mon.

source

theorem Core.Quantification.restrictorDownMono_to_downNE {α : Type u_1} (q : GQ α) (h : RestrictorDownwardMono q) :

DownNEMon q

Anti-persistence → ↓_NE Mon.

source

theorem Core.Quantification.downNW_downNE_to_restrictorDownMono {α : Type u_1} (q : GQ α) (hNW : DownNWMon q) (hNE : DownNEMon q) :

RestrictorDownwardMono q

↓_NW Mon ∧ ↓_NE Mon → Anti-persistence.

Proof: shrink A to A' in two steps via A'' = A' ∪ (A∩B) ∩ something. More precisely, A'' = A ∩ (A' ∪ B). Then A' ⊆ A'' ⊆ A, A∩B = A''∩B (removing complement-of-(A'∪B) doesn't touch B-elements), and A'\B = A''\B (A'' outside B = A ∩ A' outside B = A' outside B). Step 1: ↓_NE from A to A''. Step 2: ↓_NW from A'' to A'.

source

theorem Core.Quantification.anti_persistent_iff_downNW_and_downNE {α : Type u_1} (q : GQ α) :

RestrictorDownwardMono q ↔ DownNWMon q ∧ DownNEMon q

Anti-persistence ↔ ↓_NW Mon ∧ ↓_NE Mon.

source

theorem Core.Quantification.outerNeg_upSE_to_downNW {α : Type u_1} (q : GQ α) (h : UpSEMon q) :

DownNWMon (outerNeg q)

Outer negation reverses ↑_SE to ↓_NW (@cite{peters-westerstahl-2006} Prop 8a). Contrapositive: if Q(R',S)→Q(R,S) under ↑_SE conditions, then ¬Q(R,S)→¬Q(R',S), which is ↓_NW for ~Q.

source

theorem Core.Quantification.outerNeg_downNW_to_upSE {α : Type u_1} (q : GQ α) (h : DownNWMon q) :

UpSEMon (outerNeg q)

Outer negation reverses ↓_NW to ↑_SE.

source

theorem Core.Quantification.outerNeg_upSW_to_downNE {α : Type u_1} (q : GQ α) (h : UpSWMon q) :

DownNEMon (outerNeg q)

Outer negation reverses ↑_SW to ↓_NE.

source

theorem Core.Quantification.outerNeg_downNE_to_upSW {α : Type u_1} (q : GQ α) (h : DownNEMon q) :

UpSWMon (outerNeg q)

Outer negation reverses ↓_NE to ↑_SW.

source

theorem Core.Quantification.innerNeg_downNE_to_downNW {α : Type u_1} (q : GQ α) (h : DownNEMon q) :

DownNWMon (innerNeg q)

Inner negation switches ↓_NE ↔ ↓_NW (@cite{peters-westerstahl-2006} Prop 8b).

Proof: if Q is ↓_NE Mon, then Q¬(A,B) = Q(A,¬B), A'⊆A, and A\B = A'\B means A∩(¬B) = A'∩(¬B), so ↓_NE Mon on Q gives Q(A',¬B) = Q¬(A',B). This is the ↓_NW condition for Q¬.

source

theorem Core.Quantification.innerNeg_downNW_to_downNE {α : Type u_1} (q : GQ α) (h : DownNWMon q) :

DownNEMon (innerNeg q)

Inner negation switches ↓_NW ↔ ↓_NE.

source

theorem Core.Quantification.innerNeg_upSE_to_upSW {α : Type u_1} (q : GQ α) (h : UpSEMon q) :

UpSWMon (innerNeg q)

Inner negation switches ↑_SE ↔ ↑_SW.

source

theorem Core.Quantification.innerNeg_upSW_to_upSE {α : Type u_1} (q : GQ α) (h : UpSWMon q) :

UpSEMon (innerNeg q)

Inner negation switches ↑_SW ↔ ↑_SE.

source

theorem Core.Quantification.smooth_iff_outerNeg_coSmooth {α : Type u_1} (q : GQ α) :

Smooth q ↔ CoSmooth (outerNeg q)

Smooth ↔ outer negation is co-smooth (@cite{peters-westerstahl-2006} Prop 8a).

source

theorem Core.Quantification.smooth_iff_innerNeg_coSmooth {α : Type u_1} (q : GQ α) :

Smooth q ↔ CoSmooth (innerNeg q)

Smooth ↔ inner negation is co-smooth (@cite{peters-westerstahl-2006} Prop 8b).

source

theorem Core.Quantification.smooth_conservative_scopeUpMono {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hSmooth : Smooth q) :

ScopeUpwardMono q

CONSERV ∧ Smooth → Mon↑ (@cite{peters-westerstahl-2006} Prop 9).

Proof: Given Q(A,B) and B ⊆ B'. Let A' = A \ (B'\B). Then:

A'⊆A and A∩B=A'∩B (removing B'\B doesn't touch B since B∩(B'\B)=∅) → ↓_NE gives Q(A',B)
A'∩B = A'∩B' (any x∈A'∩B' must be in B, since elements of B'\B were removed) → CONSERV: Q(A',B) = Q(A',B')
A'⊆A and A'\B'=A\B' (A'\B' = A(B'\B)\B' = A\B') → ↑_SE gives Q(A,B')

source

theorem Core.Quantification.symmetric_to_upSW_downNE {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hSym : QSymmetric q) :

UpSWMon q ∧ DownNEMon q

CONSERV ∧ QSymmetric → ↑_SW Mon ∧ ↓_NE Mon (@cite{peters-westerstahl-2006} Prop 7).

Under CONSERV, symmetry is equivalent to Q(A,B) ↔ Q(A∩B, A∩B). Both ↑_SW and ↓_NE preserve A∩B, so the truth value is unchanged.

source

theorem Core.Quantification.upSW_downNE_to_symmetric {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hUpSW : UpSWMon q) (hDownNE : DownNEMon q) :

QSymmetric q

↑_SW Mon ∧ ↓_NE Mon → QSymmetric (under CONSERV). Converse of symmetric_to_upSW_downNE. Together they give @cite{peters-westerstahl-2006} Prop 7: a CONSERV quantifier is symmetric iff it satisfies ↑_SW Mon and ↓_NE Mon.

Proof sketch: Given Q(A,B), extend A to A∪B via ↑_SW (intersection preserved), then shrink A∪B to B via ↓_NE (intersection preserved), yielding Q(B, A∩B). By CONSERV, Q(B, A∩B) = Q(B, B∩(A∩B)) = Q(B, A∩B). Symmetrically from Q(B,A) → Q(A,B).

source

theorem Core.Quantification.symmetric_iff_upSW_downNE {α : Type u_1} (q : GQ α) (hCons : Conservative q) :

QSymmetric q ↔ UpSWMon q ∧ DownNEMon q

@cite{peters-westerstahl-2006} Prop 7: a CONSERV type ⟨1,1⟩ quantifier is symmetric iff it satisfies ↑_SW Mon and ↓_NE Mon.

source

theorem Core.Quantification.conservative_outerNeg {α : Type u_1} (q : GQ α) (h : Conservative q) :

Conservative (outerNeg q)

Conservativity is closed under complement (K&S §2.3, negation). If Q is conservative, then ~Q is conservative.

source

theorem Core.Quantification.conservative_gqMeet {α : Type u_1} (f g : GQ α) (hf : Conservative f) (hg : Conservative g) :

Conservative (gqMeet f g)

Conservativity is closed under meet (K&S §2.3, conjunction). If Q₁ and Q₂ are conservative, then Q₁ ∧ Q₂ is conservative.

source

theorem Core.Quantification.conservative_gqJoin {α : Type u_1} (f g : GQ α) (hf : Conservative f) (hg : Conservative g) :

Conservative (gqJoin f g)

Conservativity is closed under join (K&S §2.3, disjunction). If Q₁ and Q₂ are conservative, then Q₁ ∨ Q₂ is conservative.

source

theorem Core.Quantification.outerNeg_gqJoin {α : Type u_1} (f g : GQ α) :

outerNeg (gqJoin f g) = gqMeet (outerNeg f) (outerNeg g)

K&S (26): complement distributes over join via de Morgan. ~(f ∨ g) = ~f ∧ ~g. "neither...nor" = complement of "either...or".

source

theorem Core.Quantification.outerNeg_gqMeet {α : Type u_1} (f g : GQ α) :

outerNeg (gqMeet f g) = gqJoin (outerNeg f) (outerNeg g)

K&S (26): complement distributes over meet via de Morgan. ~(f ∧ g) = ~f ∨ ~g.

source

theorem Core.Quantification.scopeUpMono_gqMeet {α : Type u_1} (f g : GQ α) (hf : ScopeUpwardMono f) (hg : ScopeUpwardMono g) :

ScopeUpwardMono (gqMeet f g)

K&S PROP 6: Meet (join) of scope-↑ functions is scope-↑.

source

theorem Core.Quantification.scopeDownMono_gqMeet {α : Type u_1} (f g : GQ α) (hf : ScopeDownwardMono f) (hg : ScopeDownwardMono g) :

ScopeDownwardMono (gqMeet f g)

K&S PROP 6: Meet (join) of scope-↓ functions is scope-↓.

source

theorem Core.Quantification.scopeUpMono_gqJoin {α : Type u_1} (f g : GQ α) (hf : ScopeUpwardMono f) (hg : ScopeUpwardMono g) :

ScopeUpwardMono (gqJoin f g)

K&S PROP 6: Join of scope-↑ functions is scope-↑.

source

theorem Core.Quantification.conservative_adjRestrict {α : Type u_1} (q : GQ α) (adj : α → Bool) (h : Conservative q) :

Conservative (adjRestrict q adj)

K&S PROP 3: Conservativity is preserved under adjectival restriction.

source

theorem Core.Quantification.scopeUpMono_adjRestrict {α : Type u_1} (q : GQ α) (adj : α → Bool) (h : ScopeUpwardMono q) :

ScopeUpwardMono (adjRestrict q adj)

K&S PROP 5: Scope-upward monotonicity is preserved under adjectival restriction. If det is increasing, (det + AP) is increasing.

source

theorem Core.Quantification.scopeDownMono_adjRestrict {α : Type u_1} (q : GQ α) (adj : α → Bool) (h : ScopeDownwardMono q) :

ScopeDownwardMono (adjRestrict q adj)

K&S PROP 5: Scope-downward monotonicity is preserved under adjectival restriction. If det is decreasing, (det + AP) is decreasing — NPIs still licensed.

source

theorem Core.Quantification.individual_upward_closed {α : Type u_1} (a : α) (P P' : α → Bool) (h : ∀ (x : α), P x = true → P' x = true) :

individual a P = true → individual a P' = true

Montagovian individuals are upward closed (ultrafilter property): if P ⊆ P' and a ∈ P, then a ∈ P'.

source

theorem Core.Quantification.individual_meet_closed {α : Type u_1} (a : α) (P Q : α → Bool) :

individual a P = true → individual a Q = true → (individual a fun (x : α) => P x && Q x) = true

Montagovian individuals are closed under intersection: if a ∈ P and a ∈ Q, then a ∈ P ∩ Q.

source

theorem Core.Quantification.vanBenthem_refl_antisym_is_inclusion {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hRefl : PositiveStrong q) (hAnti : QAntisymmetric q) (A B : α → Bool) :

q A B = true ↔ ∀ (x : α), A x = true → B x = true

@cite{van-benthem-1984} Theorem 3.1.1: Under conservativity, inclusion (⊆) is the only reflexive antisymmetric quantifier.

This is the "Aristotle reversed" cornerstone: the inferential properties (reflexivity + antisymmetry) uniquely determine the quantifier "all".

Proof: (→) By CONSERV, Q(A,B) = Q(A, A∩B). Reflexivity gives Q(A∩B, A∩B). CONSERV again gives Q(A∩B, A) = Q(A∩B, A∩B). Antisymmetry on Q(A, A∩B) and Q(A∩B, A) yields A = A∩B, i.e., A ⊆ B. (←) If A ⊆ B then A∩B = A, so Q(A,B) = Q(A,A) by CONSERV + reflexivity.

source

theorem Core.Quantification.zwarts_refl_trans_scopeUp {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hRefl : PositiveStrong q) (hTrans : QTransitive q) :

ScopeUpwardMono q

@cite{van-benthem-1984} Thm 4.1.1 (Zwarts): reflexive + transitive → MON↑. Under CONSERV, if Q is reflexive and transitive, Q is scope-upward-monotone.

Proof: QAB and B ⊆ B' gives QBB' (CONSERV + reflexivity), then QAB' by transitivity.

source

theorem Core.Quantification.zwarts_refl_trans_restrictorDown {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hRefl : PositiveStrong q) (hTrans : QTransitive q) :

RestrictorDownwardMono q

@cite{van-benthem-1984} Thm 4.1.1 (Zwarts): reflexive + transitive → ↓MON. Under CONSERV, if Q is reflexive and transitive, Q is restrictor-downward-monotone (anti-persistent).

Proof: QR'S and R ⊆ R' gives QRR' (CONSERV + reflexivity), then QRS by transitivity.

source

theorem Core.Quantification.zwarts_sym_scopeUp_quasiRefl {α : Type u_1} (q : GQ α) (hCons : Conservative q) (_hSym : QSymmetric q) (hUp : ScopeUpwardMono q) :

QuasiReflexive q

@cite{van-benthem-1984} Thm 4.1.3 (Zwarts): for symmetric quantifiers, scope-↑ implies quasi-reflexive, under CONSERV.

source

theorem Core.Quantification.zwarts_sym_scopeDown_quasiUniv {α : Type u_1} (q : GQ α) (hCons : Conservative q) (_hSym : QSymmetric q) (hDown : ScopeDownwardMono q) :

QuasiUniversal q

@cite{van-benthem-1984} Thm 4.1.3 (Zwarts): for symmetric quantifiers, scope-↓ implies quasi-universal, under CONSERV.

source

theorem Core.Quantification.scopeUpMono_rightContinuous {α : Type u_1} (q : GQ α) (h : ScopeUpwardMono q) :

RightContinuous q

Right-monotone quantifiers are right-continuous (@cite{van-benthem-1984} §4.3).

source

theorem Core.Quantification.irrefl_almostConn_scopeDown {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hIrrefl : NegativeStrong q) (hAC : AlmostConnected q) :

ScopeDownwardMono q

@cite{van-benthem-1984} Thm 4.1.2: irreflexive + almost-connected → MON↓. Proof by duality: Q irreflexive ↔ ¬Q reflexive, Q almost-connected ↔ ¬Q transitive. By Zwarts (4.1.1), ¬Q has MON↑. Outer negation reverses scope monotonicity: MON↑ of ¬Q gives MON↓ of Q.

source

theorem Core.Quantification.irrefl_almostConn_restrictorUp {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hIrrefl : NegativeStrong q) (hAC : AlmostConnected q) :

RestrictorUpwardMono q

@cite{van-benthem-1984} Thm 4.1.2: irreflexive + almost-connected → ↑MON. Proof: ¬Q has ↓MON (Zwarts). Contrapositive gives ↑MON for Q: ↓MON(¬Q) = (A⊆A' → ¬Q(A',B) → ¬Q(A,B)) = (A⊆A' → Q(A,B) → Q(A',B)) = ↑MON(Q).

source

theorem Core.Quantification.vanBenthem_symm_quasiRefl_is_overlap {α : Type u_1} [Fintype α] [DecidableEq α] (q : GQ α) (hCons : Conservative q) (hSym : QSymmetric q) (hQR : QuasiReflexive q) (hWitT : ∃ (x : α), (q (fun (y : α) => y == x) fun (y : α) => y == x) = true) (hWitF : ∃ (A : α → Bool), q A A = false) (hIso : QuantityInvariant q) (A B : α → Bool) :

q A B = true ↔ ∃ (x : α), A x = true ∧ B x = true

@cite{van-benthem-1984} Cor 3.3.2: Under conservativity, the ONLY symmetric quasi-reflexive quantifier is overlap (= "some").

Proof: CONSERV + symmetric → intersective (conserv_symm_iff_int). So q(A,B) = q(A∩B, A∩B) =: f(A∩B). Quasi-reflexivity gives: f(C) → f(D) when C ⊆ D (set A=D, B=C; then q(D,C) = f(D∩C) = f(C), and QR gives q(D,D) = f(D)). VAR gives f(∅) = false (otherwise f ≡ true) and ∃C, f(C) = true. So f is an upward-closed non-trivial predicate on sets.

(→) If q(A,B) = true, then f(A∩B) = true, so A∩B is non-empty. (←) If A∩B is non-empty, pick a ∈ A∩B. Then f({a}) must be true (otherwise f(C) = false for all singletons, and upward closure + A∩B ⊇ {a} gives f(A∩B) = true only if f({a}) = true — contradiction). that works across models of arbitrary size, ensuring q is non-trivial on singletons. Because GQ α is fixed-domain, we explicitly require a singleton witness (hWitT) and isomorphism invariance (hIso) to ensure all singletons behave identically.

source