Generalized Quantifiers #
@cite{barwise-cooper-1981} @cite{keenan-stavi-1986} @cite{peters-westerstahl-2006} @cite{van-de-pol-etal-2023} @cite{mostowski-1957}
Determiners have type (e→t) → ((e→t) → t):
⟦every⟧ = λR.λS. ∀x. R(x) → S(x)⟦some⟧ = λR.λS. ∃x. R(x) ∧ S(x)⟦no⟧ = λR.λS. ¬∃x. R(x) ∧ S(x)
Semantic Universals #
Three properties conjectured to hold of all simple (lexicalized) determiners:
- Conservativity:
Q(A, B) ↔ Q(A, A ∩ B)— only the restrictor matters - Quantity (isomorphism closure): meaning depends only on cardinalities
|A ∩ B|,|A \ B|,|B \ A|,|M \ (A ∪ B)| - Monotonicity: Q is either upward or downward monotone in scope
@cite{van-de-pol-etal-2023} show quantifiers satisfying these universals have shorter minimal description length, suggesting a simplicity bias explains the universals.
Organization #
- Generic GQ properties:
Core.Quantification—Conservative,ScopeUpwardMono,ScopeDownwardMono,outerNeg,innerNeg,dualQ, etc. (model-agnostic) - Concrete denotations:
every_sem,some_sem, etc. — require[Fintype m.Entity]for decidable computation viadecide (∀/∃ x, ...) - Counting quantifiers:
most_sem,few_sem, etc. — useFinset.univ.filterfor cardinality comparisons
ScopeUpwardMono/ScopeDownwardMono are equivalent to Mathlib's
Monotone/Antitone (see Core.Quantification.scopeUpMono_iff_monotone),
connecting to Semantics.Entailment.Polarity.IsUpwardEntailing = Monotone.
Count of elements satisfying a predicate, via Finset.univ.filter.
Equations
Instances For
Equations
Instances For
Partee's A (existential closure) = Barwise & Cooper's ⟦some⟧.
Both compute λR.λS. ∃x. R(x) ∧ S(x) over a finite domain.
A takes the domain explicitly; some_sem uses decide over Fintype.
Equations
Instances For
⟦most⟧(R)(S) = |R ∩ S| > |R \ S|
Equations
- One or more equations did not get rendered due to their size.
Instances For
⟦few⟧(R)(S) = |R ∩ S| < |R \ S| — a minority of Rs are Ss.
Dual of most_sem: few(R,S) ↔ ¬most(R,S) ∧ ¬half(R,S).
Equations
- One or more equations did not get rendered due to their size.
Instances For
⟦half⟧(R)(S) = 2 * |R ∩ S| = |R| — exactly half of Rs are Ss.
Equations
- One or more equations did not get rendered due to their size.
Instances For
⟦at least n⟧(R)(S) = |R ∩ S| ≥ n
Equations
Instances For
⟦at most n⟧(R)(S) = |R ∩ S| ≤ n
Equations
Instances For
⟦exactly n⟧(R)(S) = |R ∩ S| = n
Equations
Instances For
⟦all but n⟧(R)(S) = |R \ S| = n — exactly n R-elements are non-S.
Generalizes "every" (= all but 0). The exceptive counterpart of
exactly_n_sem (which counts |R ∩ S| = n).
Equations
Instances For
⟦between n and k⟧(R)(S) = n ≤ |R ∩ S| ≤ k
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Bridge: toyModel.Entity = ToyEntity is definitional but opaque to instance search.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
∀ x, P x is invariant under bijective substitution.
∃ x, P x is invariant under bijective substitution.
⟦every⟧ is conservative: ∀x. R(x) → S(x) iff ∀x. R(x) → (R(x) ∧ S(x)).
⟦some⟧ is conservative: ∃x. R(x) ∧ S(x) iff ∃x. R(x) ∧ (R(x) ∧ S(x)).
⟦no⟧ is conservative: ∀x. R(x) → ¬S(x) iff ∀x. R(x) → ¬(R(x) ∧ S(x)).
⟦most⟧ is conservative: the R-elements in S are the R-elements in R∩S.
⟦few⟧ is conservative: the R-elements in S are the R-elements in R∩S.
⟦half⟧ is conservative: depends only on R ∩ S within R.
⟦at least n⟧ is conservative: |R ∩ S| = |R ∩ (R ∩ S)|.
⟦at most n⟧ is conservative.
⟦exactly n⟧ is conservative.
⟦every⟧ is upward monotone in scope.
⟦some⟧ is upward monotone in scope.
⟦no⟧ is downward monotone in scope.
⟦few⟧ is downward monotone in scope: if S ⊆ S' and few(R,S'),
then few(R,S). Fewer Ss among Rs means even fewer S-subsets.
⟦most⟧ is upward monotone in scope: if S ⊆ S' and most(R,S),
then most(R,S'). |R∩S'| ≥ |R∩S| > |R\S| ≥ |R\S'|.
⟦some⟧ = ⟦at least 1⟧: existential quantification is "at least one".
outerNeg ⟦some⟧ = ⟦no⟧: negating existence gives universal negation.
⟦at most n⟧ = outerNeg ⟦at least n+1⟧: duality of lower and upper bounds.
This is the counting quantifier instance of the Square of Opposition.
⟦no⟧ = ⟦at most 0⟧. Derived algebraically:
no = outerNeg(some) = outerNeg(at_least 1) = at_most 0.
⟦exactly n⟧ = ⟦at least n⟧ ⊓ ⟦at most n⟧ in the GQ lattice.
"Exactly n" is the meet of a lower bound and an upper bound.
⟦at least n⟧ is Mon↑ in scope: enlarging B cannot decrease |A ∩ B|.
⟦at most n⟧ is Mon↓ in scope. Derived from duality:
outerNeg flips Mon↑ to Mon↓ (Prop 8), and at_most = outerNeg(at_least).
Quantity / Isomorphism closure:
Q(A, B) depends only on the four cardinalities
|A ∩ B|, |A \ B|, |B \ A|, |M \ (A ∪ B)|.
Equivalently: permuting the domain does not change the quantifier's truth value. This is the type ⟨1,1⟩ (binary) generalization of @cite{mostowski-1957}'s permutation invariance for type ⟨1⟩ (unary) quantifiers; the extension to binary determiners is due to @cite{van-benthem-1984} (building on Lindström 1966).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A quantifier satisfies all three Barwise & Cooper universals. @cite{van-de-pol-etal-2023} show these quantifiers have shorter MDL.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Proportional (@cite{peters-westerstahl-2006} §4.3): Q's truth value depends only on the ratio |A ∩ B| / |A| (the proportion of A-elements in B).
Under CONS + QUANT, cardinal quantifiers ("at least 3") depend on absolute cardinalities, while proportional quantifiers ("most", "half") depend only on the proportion of A-elements that are B-elements.
Formally: if the cross-ratio |A₁∩B₁|·|A₂\B₂| = |A₂∩B₂|·|A₁\B₁| (same ratio of successes to failures) and both restrictors are non-empty, the truth values agree.
Proportional ⊂ Quantity: Quantity requires all four cells to match; Proportional requires only the ratio of two cells (hTT, hTF).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Quantity → QuantityInvariant: cardinality-dependence implies bijection-invariance.
Proof: a bijection preserves count (via count_bij_inv),
so all four cell cardinalities match, and Quantity gives the result.
Instances For
QuantityInvariant → Quantity: bijection-invariance implies cardinality-dependence.
On a finite domain, matching cell cardinalities guarantees a cell-preserving
bijection exists (permute elements within each of the four (R,S) cells).
A non-conservative quantifier for contrast: ⟦M⟧(A,B) = |A| > |B|
(van de Pol et al.'s hypothetical counterpart to "most").
Equations
- One or more equations did not get rendered due to their size.
Instances For
M is not conservative: it inspects B outside A. Witness: R = {john, mary}, S = {john, pizza}. m_sem R S = (2 > 2) = false, but m_sem R (R∩S) = (2 > 1) = true.
⟦some⟧ is symmetric: ∃x.R(x)∧S(x) = ∃x.S(x)∧R(x).
⟦no⟧ is symmetric: ¬∃x.R(x)∧S(x) = ¬∃x.S(x)∧R(x).
⟦every⟧ is NOT symmetric. Witness: R=students, S=things (everything).
every(students)(things)=true but every(things)(students)=false.
⟦some⟧ is intersective (follows from CONSERV + SYMM).
⟦no⟧ is intersective.
⟦every⟧ is left anti-additive: every(A∪B, C) = every(A,C) ∧ every(B,C).
⟦no⟧ is left anti-additive: no(A∪B, C) = no(A,C) ∧ no(B,C).
⟦no⟧ is right anti-additive: no(A, B∪C) = no(A,B) ∧ no(A,C).
"Nobody saw A-or-B" ↔ "Nobody saw A and nobody saw B".
This licenses strong NPIs in scope: "Nobody lifted a finger."
@cite{peters-westerstahl-2006} Prop 13: the only non-trivial CONSERV, EXT,
and ISOM quantifiers satisfying LAA are every and no (and A = ∅).
TODO: Full proof requires showing that under ISOM, LAA + CONSERV + non-triviality
forces the quantifier to be one of these three, by number triangle analysis.
Inner negation maps every to no: every...not = no.
∀x. R(x) → ¬S(x) = ¬∃x. R(x) ∧ S(x).
The dual of every is some: Q̌(every) = some.
¬(∀x. R(x) → ¬S(x)) = ∃x. R(x) ∧ S(x).
every_sem satisfies Extension: spectator elements
(outside the restrictor) don't affect truth values.
Proof: !R(e) || S(e) = true when R(e) = false, so all is unchanged.
most_sem satisfies Extension: spectators don't enter
either R∩S or R\S, so the cardinality comparison is unchanged.
every_sem Extension at the denotation level: truth depends only on
R-elements of the domain. Spectators are irrelevant.
every(R,S) = ∀x∈R. S(x).
every_sem is positive strong: every(A,A) = true for all A.
Proof: R(x) = true → R(x) = true for all x.
no_sem is negative strong (@cite{peters-westerstahl-2006} §5.3 fn.9):
no(A,A) = false for all non-empty A.
For the empty restrictor, no(∅,∅) = true (vacuously), so NegativeStrong
(which requires Q(R,R) = false for ALL R) fails when empty R exists.
We prove the non-empty case.
no_sem is NOT positive strong: no(A,A) = false when A is non-empty.
Counterexample: R = {john}.
⟦some⟧ is existential (K&S G3): some(A,B) = some(A∩B, everything).
some is natural in there-sentences: "There are some cats."
⟦no⟧ is existential (K&S G3): no(A,B) = no(A∩B, everything).
no is natural in there-sentences: "There are no cats."
⟦every⟧ is NOT existential (K&S §3.3).
"every" is not natural in there-sentences: *"There is every cat."
Witness: R=students, S=things. every(R,S)=true but every(R∩S, 1)=true trivially,
yet every(thing, student)≠every(thing∩student, 1).
⟦most⟧ is NOT existential (K&S §3.3).
"most" is not natural in there-sentences: *"There are most cats."
Witness: R={john,mary}, S={john,pizza}. |R∩S|=1 vs |R\S|=1, so most(R,S)=false.
But most(R∩S, 1_P): |{john}∩1_P|=1 vs |{john}\1_P|=0, so most(R∩S, 1_P)=true.
⟦every⟧ is transitive: A ⊆ B and B ⊆ C implies A ⊆ C.
⟦every⟧ is antisymmetric: A ⊆ B and B ⊆ A implies A = B.
⟦some⟧ is quasi-reflexive: A∩B ≠ ∅ implies A∩A ≠ ∅ (i.e., A ≠ ∅).
⟦no⟧ is quasi-universal: A∩A = ∅ (i.e., A = ∅) implies A∩B = ∅ for all B.
⟦every⟧ is restrictor-↓ (anti-persistent).
Follows from Zwarts bridge: reflexive + transitive + CONSERV → ↓MON.
⟦some⟧ is restrictor-↑ (persistent): A ⊆ A' and some(A,B) → some(A',B).
⟦no⟧ is restrictor-↓ (anti-persistent): A ⊆ A' and no(A',B) → no(A,B).
⟦every⟧ has double monotonicity ↓MON↑ (@cite{van-benthem-1984} §4.2).
⟦some⟧ has double monotonicity ↑MON↑.
⟦no⟧ has double monotonicity ↓MON↓.
outerNeg ⟦every⟧ (= "not all") has double monotonicity ↑MON↓.
⟦every⟧ is filtrating: every(A,B) ∧ every(A,C) → every(A, B∩C).
Contradiction (A vs O): the A-form and O-form are contradictories.
Contradiction (E vs I): the E-form and I-form are contradictories.
Follows from outerNeg_some_eq_no: negating "some" gives "no".
Contrariety (A ∧ E): the A-form and E-form can't both hold unless the restrictor is empty. If every R is S and no R is S, then nothing satisfies R.
Subalternation (A → I): the A-form entails the I-form when the restrictor is non-empty. This is @cite{belnap-1970}'s assertiveness condition: ∀x(Cx/Bx) presupposes ∃xCx. @cite{strawson-1952} argued "All S are P" presupposes there are Ss — Belnap derives this.
Subalternation (E → O): the E-form entails the O-form when the restrictor is non-empty.
Subcontrariety (I ∨ O): the I-form and O-form can't both fail when the restrictor is non-empty. Either some R is S, or not every R is S (or both).
⟦some⟧ is ↑_SE Mon: adding elements of B to A preserves some(A,B).
⟦some⟧ is ↑_SW Mon: adding elements outside B to A preserves some(A,B).
⟦every⟧ is ↓_NW Mon: removing elements of B from A preserves every(A,B).
⟦every⟧ is ↓_NE Mon: removing elements outside B from A preserves every(A,B).
⟦no⟧ is ↓_NW Mon.
⟦no⟧ is ↓_NE Mon.
⟦some⟧ is ↓_NE Mon (direct proof).
Removing non-S elements from A preserves ∃x.R(x)∧S(x) since the witness is in S.
⟦some⟧ is smooth (↓_NE + ↑_SE).
@cite{peters-westerstahl-2006} §5.6: persistence gives ↑_SE;
the witness argument gives ↓_NE directly.
⟦every⟧ is ↑_SE Mon (direct proof).
Adding B-elements to A preserves ∀x.R(x)→S(x) since the new elements satisfy S.
⟦every⟧ is smooth (↓_NE + ↑_SE). Anti-persistence gives ↓_NE;
adding S-elements to A preserves ∀x.R(x)→S(x) (direct ↑_SE proof).
⟦no⟧ is co-smooth (↓_NW + ↑_SW). Follows from anti-persistence.
⟦most⟧ is ↓_NE Mon (direct proof).
Removing non-S elements from A preserves |A∩S| > |A\S| since |A∩S| stays
the same while |A\S| decreases.
⟦most⟧ is ↑_SE Mon (direct proof).
Adding S-elements to A preserves |A∩S| > |A\S| since |A∩S| grows
while |A\S| stays the same.
⟦most⟧ is smooth. This is a key empirical fact: most natural language
Mon↑ determiners are smooth (@cite{peters-westerstahl-2006} §5.6, (5.28)).
⟦at least n⟧ is persistent (Mon↑ in restrictor), hence ↑_SE and ↑_SW.
⟦at least n⟧ is ↓_NE Mon: removing non-S elements from A preserves
|A ∩ S| ≥ n since the S-witnesses are retained.
⟦at least n⟧ is smooth (↓_NE + ↑_SE).
Persistence gives ↑_SE; the witness-preservation argument gives ↓_NE.
⟦at most n⟧ is anti-persistent (Mon↓ in restrictor). Derived from duality:
outerNeg flips Mon↑_restrictor to Mon↓_restrictor.
⟦at most n⟧ is co-smooth (↓_NW + ↑_SW). Derived from duality:
Smooth(at_least) ↔ CoSmooth(outerNeg(at_least)) = CoSmooth(at_most).
Quantity is closed under outerNeg: if Q depends only on cell cardinalities,
so does ~Q.
Quantity is closed under meet: if Q₁ and Q₂ depend only on cell
cardinalities, so does Q₁ ⊓ Q₂.
⟦at least n⟧ satisfies Quantity: truth depends only on |A ∩ B|.
⟦at most n⟧ satisfies Quantity: truth depends only on |A ∩ B|.
⟦exactly n⟧ satisfies Quantity. Derived from meet closure:
exactly n = (at least n) ⊓ (at most n).
⟦some⟧ satisfies Quantity. Derived: some = at least 1.
⟦no⟧ satisfies Quantity. Derived: no = at most 0.
⟦most⟧ satisfies Quantity: truth depends on |A ∩ B| and |A \ B|.
most(A,B) ↔ |A ∩ B| > |A \ B|.
⟦few⟧ satisfies Quantity: truth depends on |A ∩ B| and |A \ B|.
few(A,B) ↔ |A ∩ B| < |A \ B|.
⟦half⟧ satisfies Quantity: truth depends on |A ∩ B| and |A \ B|.
half(A,B) ↔ 2 * |A ∩ B| = |A|, and |A| = |A ∩ B| + |A \ B|.
⟦some⟧ satisfies all three universals: CONSERV ∧ QUANTITY ∧ Mon↑.
⟦every⟧ satisfies all three universals: CONSERV ∧ QUANTITY ∧ Mon↑.
⟦no⟧ satisfies all three universals: CONSERV ∧ QUANTITY ∧ Mon↓.
⟦most⟧ satisfies all three universals: CONSERV ∧ QUANTITY ∧ Mon↑.
⟦few⟧ satisfies all three universals: CONSERV ∧ QUANTITY ∧ Mon↓.
⟦at least n⟧ satisfies all three universals: CONSERV ∧ QUANTITY ∧ Mon↑.
⟦at most n⟧ satisfies all three universals: CONSERV ∧ QUANTITY ∧ Mon↓.
⟦exactly n⟧ satisfies CONSERV ∧ QUANTITY but is neither Mon↑ nor Mon↓
for n ≥ 1. This is expected: "exactly n" is a non-monotone quantifier.
We prove the first two universals.
⟦all but 0⟧ = ⟦every⟧: zero exceptions means universal.
⟦all but n⟧ is conservative: depends only on R ∩ S within R.
⟦all but n⟧ satisfies Quantity: truth depends only on |A \ B|.
⟦all but n⟧ satisfies CONSERV ∧ QUANTITY (but not MON for n ≥ 1).
⟦between n and k⟧ is conservative (from meet closure).
⟦between n and k⟧ satisfies Quantity (from meet closure).
⟦between n and k⟧ satisfies CONSERV ∧ QUANTITY.
⟦most⟧ is proportional: most(A,B) ↔ |A∩B| > |A\B| depends only on
the ratio |A∩B|/|A\B|. Cross-ratio equality preserves the > comparison.
⟦few⟧ is proportional: few(A,B) ↔ |A∩B| < |A\B|.
⟦at least n⟧ is NOT proportional for n ≥ 2: it depends on absolute count,
not ratio. Counterexample on toyModel: |{john}∩{john}| = 1, |{john}{john}| = 0
vs |{john,mary}∩{john,mary}| = 2, |{john,mary}{john,mary}| = 0.
Same ratio (1/0 = 2/0 in cross-ratio: 10 = 0 = 20) but at_least_2
gives false for the first and true for the second.