Quantifier Universals Bridge #
@cite{barwise-cooper-1981} @cite{mostowski-1957} @cite{peters-westerstahl-2006} @cite{van-benthem-1984} @cite{van-de-pol-etal-2023}
Bridges the English determiner fragment (Fragments.English.Determiners.QuantityWord)
to the GQ property predicates in Core.Quantification and
Theories.Semantics.Lexical.Determiner.Quantifier.
Empirical phenomena verified #
- Conservativity (@cite{barwise-cooper-1981}, conservativity conjecture): all six English quantity words satisfy CONSERV.
- Quantity/isomorphism closure (@cite{mostowski-1957}): all six satisfy QUANT.
- Table II per-entry verification (@cite{barwise-cooper-1981} Table II): each quantity word's strength and monotonicity direction match the paper's classification. Changing a fragment field breaks exactly one theorem.
- Monotonicity–strength correlation (@cite{barwise-cooper-1981} U7): strong English determiners are scope-↑MON (increasing).
- Weak ↔ there-insertion (@cite{barwise-cooper-1981} §4.6): weak determiners allow there-insertion; strong determiners don't.
- Symmetry ↔ weak (@cite{peters-westerstahl-2006}, symmetric ↔ there-insertion): weak = symmetric, strong = not symmetric.
- Positive-strong → scope-↑ (@cite{peters-westerstahl-2006}, positive-strong determiners are scope-upward-monotone).
- Duality (@cite{barwise-cooper-1981} §4.11): outer/inner negation and dual operations connect every ↔ some ↔ no via the Square of Opposition, bridged to fragment entries.
- Domain restriction (@cite{ritchie-schiller-2024}): conservativity enables domain restriction for all six quantity words.
Data structures #
MonotonicitySimplicity,ConservativitySimplicity,QuantitySimplicity: @cite{van-de-pol-etal-2023} LZ complexity effect sizes.
Thread map #
- Formal definitions:
Core.Quantification—Conservative,ScopeUpwardMono,ScopeDownwardMono,QuantityInvariant,PositiveStrong,QSymmetric,outerNeg,innerNeg,dualQ - Concrete denotations:
Semantics.Lexical.Determiner.Quantifier—every_sem,some_sem,no_sem,most_sem,few_sem,half_sem - Fragment entries:
Fragments.English.Determiners.QuantityWord.gqDenotation - Domain restriction:
Semantics.Lexical.Determiner.DomainRestriction—DomainRestrictor,DDRP,conservative_domain_restricted - Impossibility theorems:
Core.Quantification.NumberTreeGQ—no_asymmetric,no_strict_partial_order,no_euclidean - Counting formula:
Core.Quantification.conservativeQuantifierCount
Conservativity holds for all simple (lexicalized) English determiners.
@cite{barwise-cooper-1981} conjecture this is a universal of natural
language. Proved individually for each quantity word via
every_conservative, some_conservative, etc.
All simple determiners satisfy quantity/isomorphism closure:
their truth value depends only on cardinalities |A∩B|, |A\B|, etc.
All/any-based quantifiers (every, some, no) use all_bij_inv/any_bij_inv;
cardinality-based quantifiers (most, few, half) use filter_length_bij_inv.
every/all: strong, scope-↑MON (increasing).
most: strong, scope-↑MON (increasing).
some: weak, scope-↑MON (increasing).
no: weak, scope-↓MON (decreasing).
few: weak, scope-↓MON (decreasing).
half: weak, non-monotone. Not in @cite{barwise-cooper-1981} Table II; classification follows @cite{van-de-pol-etal-2023}.
All English quantity words except "half" are monotone. "Half" is the lone non-monotone simple determiner (@cite{van-de-pol-etal-2023} classify it as non-monotone).
"Half" is the sole non-monotone quantity word.
The ⟨some, all⟩ scale is upward monotone (both members increasing).
@cite{barwise-cooper-1981} U7 (monotonicity–strength correlation): strong determiners are scope-↑MON (increasing). The full universal distinguishes positive-strong (→ ↑MON) from negative-strong (→ ↓MON); since both English strong determiners (most, every) are positive, the universal reduces to: strong → increasing.
Strictly stronger than the previous strong_implies_monotone (which
only checked != .nonMonotone without verifying direction).
Weak determiners allow there-insertion (@cite{barwise-cooper-1981} §4.6). "There are some/a/few/no cats" vs *"There is every/each cat".
Strong determiners block there-insertion (@cite{barwise-cooper-1981} Table II).
Weak English determiners are symmetric (@cite{peters-westerstahl-2006},
symmetric ↔ there-insertion ↔ weak).
Cross-references: some_symmetric, no_symmetric in Quantifier.lean.
Strong English determiners are not symmetric (@cite{peters-westerstahl-2006}).
Witness: every_not_symmetric in Quantifier.lean.
The dual of ⟦every⟧ is ⟦some⟧: Q̌(every) = some (@cite{barwise-cooper-1981} §4.11).
¬(∀x. R(x) → ¬S(x)) = ∃x. R(x) ∧ S(x).
Bridges dualQ_every_eq_some from Quantifier.lean to fragment entries.
Inner negation maps ⟦every⟧ to ⟦no⟧: every~ = no (@cite{barwise-cooper-1981} §4.11).
∀x. R(x) → ¬S(x) = ¬∃x. R(x) ∧ S(x).
Bridges innerNeg_every_eq_no to fragment entries.
Outer negation maps ⟦some⟧ to ⟦no⟧: ~some = no (@cite{barwise-cooper-1981} §4.11).
¬(∃x. R(x) ∧ S(x)) = ∀x. R(x) → ¬S(x).
Bridges outerNeg_some_eq_no to fragment entries.
Positive-strong determiners are scope-upward-monotone
(@cite{peters-westerstahl-2006}).
Only all (= every_sem) is genuinely positive-strong; for the rest,
PositiveStrong is vacuously false (contradicted by R = λ _ => false
or R = λ _ => true), making the implication trivially true.
Monotone quantifiers have strictly lower LZ complexity than non-monotone ones. This is the strongest of the three effects. (@cite{van-de-pol-etal-2023})
- monotone_mean_lz : ℚ
Mean LZ complexity of monotone quantifiers (universe size 4)
- non_monotone_mean_lz : ℚ
Mean LZ complexity of non-monotone quantifiers
Monotone is simpler
Instances For
Conservative quantifiers have lower LZ complexity than non-conservative ones.
Instances For
Quantity-satisfying quantifiers have lower LZ complexity, but the effect is weaker than monotonicity.
Instances For
The three universals combined: quantifiers satisfying all three have the lowest complexity. Monotonicity is the strongest single predictor, quantity the weakest.
- monotonicity_effect : MonotonicitySimplicity
- conservativity_effect : ConservativitySimplicity
- quantity_effect : QuantitySimplicity
Instances For
Conservativity universally enables domain restriction: all 6 English quantity words remain conservative under any domain restrictor C.
This connects @cite{barwise-cooper-1981}'s conservativity conjecture (all simple determiners are conservative) to @cite{ritchie-schiller-2024}'s DDRPs. Domain restriction via C-intersection is well-defined for the entire English determiner system because every lexicalized determiner is conservative.
Cross-references:
conservative_domain_restricted(general GQ theorem)DDRPstructure (nested spatial regions → candidate restrictors)RitchieSchiller2024.lean(full RSA model with DDRPs)