Quantifier Universals Bridge #
[BC81] [Mos57] [PW06] [vB84] [vdPLvM+23]
Bridges the English determiner fragment (English.Determiners.QuantityWord)
to the GQ property predicates in Quantification and
Quantification.Quantifier.
Empirical phenomena verified #
- Conservativity ([BC81], conservativity conjecture): all six English quantity words satisfy CONSERV.
- Quantity/isomorphism closure ([Mos57]): all six satisfy QUANT.
- Table II per-entry verification ([BC81] 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 ([BC81] U7): strong English determiners are scope-↑MON (increasing).
- Weak ↔ there-insertion ([BC81] §4.6): weak determiners allow there-insertion; strong determiners don't.
- Symmetry ↔ weak ([PW06], symmetric ↔ there-insertion): weak = symmetric, strong = not symmetric.
- Positive-strong → scope-↑ ([PW06], positive-strong determiners are scope-upward-monotone).
- Duality ([BC81] §4.11): outer/inner negation and dual operations connect every ↔ some ↔ no via the Square of Opposition, bridged to fragment entries.
- Domain restriction ([RS24a]): conservativity enables domain restriction for all six quantity words.
Data structures #
MonotonicitySimplicity,ConservativitySimplicity,QuantitySimplicity: [vdPLvM+23] LZ complexity effect sizes.
Conservativity holds for all simple (lexicalized) English determiners.
[BC81] 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.
TODO: Rewrite proof for cardinality-based quantifiers (most, few, half)
which need count_bij_inv adapted to Prop predicates.
Extension: domain independence #
EXT (Q(A,B) depends only on A and B, not on an ambient universe)
holds trivially for GQ α since the representation is universe-free —
no axiom needed. EXT + CONS together yield the [vB84]
characterization: determiners can be represented as type ⟨1⟩ quantifiers
that "live on" their restrictor; see conservative_iff_livesOn.
[BC81] Table II: per-entry verification #
Each theorem takes one quantity word's QuantityWord.entry typological
label (the textbook-consensus B&C Table II strength/monotonicity classification)
as a hypothesis and proves the corresponding genuine GQ property of the
denotation QuantityWord.gqDenotation:
strength = .weak⟹Existential ⟦d⟧(intersective: passes there-insertion)strength = .strong⟹¬ Existential ⟦d⟧monotonicity = .increasing⟹ScopeUpwardMono ⟦d⟧monotonicity = .decreasing⟹ScopeDownwardMono ⟦d⟧
So changing a QuantityWord.entry field still breaks exactly one theorem
(the label is a hypothesis), but the theorem now earns its content from the
denotation rather than self-reporting the stored field. Where the substrate
lacks the backing lemma the conclusion is left sorry with a TODO.
B&C's Table II classifies every/all (strong, ↑MON), some (weak, ↑MON), no (weak, ↓MON), most (strong, ↑MON), many (weak, ↑MON), few (weak, ↓MON); our scale omits "many" and adds proportional "half" (van-de-pol et al.).
Caveat — "weak" ≠ Existential for proportional determiners. B&C's "weak"
tracks felicity in there-sentences; for the intersective words (some, no)
it coincides with the GQ Existential property. But the table also labels the
proportional words few and half .weak (they do pass there-insertion:
"there are few cats"), and Existential fails for them — few_sem/half_sem
are not intersective. So the weak ⟹ Existential bridge is stated and proved
only for the intersective words; for few/half the genuine GQ fact is the
negation (¬ Existential), recorded below as a substrate gap.
some: weak ⟹ Existential, and increasing ⟹ ScopeUpwardMono.
no: weak ⟹ Existential, and decreasing ⟹ ScopeDownwardMono.
every/all: strong ⟹ ¬ Existential (over a nonempty domain), and
increasing ⟹ ScopeUpwardMono. The nonemptiness hypothesis is essential:
over the empty domain every GQ is vacuously Existential.
most: increasing ⟹ ScopeUpwardMono (polymorphic, most_scope_up). The
strength ⟹ ¬ Existential half is witnessed separately at Fin 3
(table_II_most_not_existential): most is proportional, not intersective,
so refuting Existential needs a |α| ≥ 3 witness, not mere nonemptiness.
most: strong ⟹ ¬ Existential, witnessed at Fin 3. most is proportional,
not intersective, so it blocks there-insertion ([BC81] Table II).
Refuting Existential needs |α| ≥ 3 (1 elem in R∩S, 2 in R∖S): over Fin 1/
Fin 2 every GQ is vacuously Existential. Earned from not_existential_most_sem.
few: decreasing ⟹ ScopeDownwardMono (few_scope_down). The table labels
few .weak, but few_sem is proportional, not intersective, so the
genuine GQ fact is ¬ Existential ⟦few⟧ (a substrate gap), not Existential.
few: strong/weak ⟹ existential status, witnessed at Fin 3. The table's
.weak label tracks there-insertion; the genuine GQ property is
¬ Existential because few_sem is proportional, not intersective
(|R∩S| < |R∖S| is not determined by |R∩S| alone). Earned from
not_existential_few_sem.
half: non-monotone, so the increasing/decreasing bridges are vacuously true (the label hypothesis is unsatisfiable for half).
half: the table labels half .weak, but half_sem is proportional, so the
genuine GQ property is ¬ Existential ⟦half⟧, witnessed at Fin 3.
Existential half_sem (2|R∩S| = |R| ↔ 2|R∩S| = |R∩S|) is false; refuting it
needs a witness with R∖S non-empty. Earned from not_existential_half_sem.
All English quantity words except "half" are monotone in scope (each is
ScopeUpwardMono or ScopeDownwardMono); "half" is the lone non-monotone
simple determiner ([vdPLvM+23]). Stated as a real disjunction of
GQ monotonicity properties, witnessed per word from the substrate lemmas.
"Half" is non-monotone: it is neither scope-upward nor scope-downward
monotone ([vdPLvM+23]), witnessed at Fin 3 (a 2-element restrictor
on which half flips true→false under scope growth/shrinkage). Earned from
half_not_monotone.
[BC81] U7 (monotonicity–strength correlation): the strong
English determiners (every, most) are scope-↑MON. Both are positive-strong,
so the universal reduces to: strong → increasing, here proved as the genuine
ScopeUpwardMono property of each denotation.
Weak intersective determiners allow there-insertion, formalized as the
Existential property ([BC81] §4.6; [PW06]
existential ↔ there-insertion). "There are some/no cats."
Strong determiners block there-insertion: ¬ Existential over a nonempty
domain ([BC81] Table II). The most case is witnessed at
Fin 3 in table_II_most_not_existential (proportional most needs |α| ≥ 3).
Weak (intersective) English determiners are symmetric
([PW06], symmetric ↔ there-insertion ↔ weak), proved as
the genuine QSymmetric property of the denotation.
Strong English determiners are not symmetric ([PW06]).
The genuine ¬ QSymmetric property for all (= every_sem) is proved as
strong_all_not_symmetric below, over the ToyEntity witness it requires; for
most it is strong_most_not_symmetric, witnessed at Fin 3.
Strong most is not symmetric, as a property of its denotation over the
Fin 3 witness ([PW06]). most R S ↔ most S R fails for
R = {0}, S = {0,1}: most R S holds (|R∩S| = 1 > |R∖S| = 0) but
most S R does not (|S∩R| = 1 > |S∖R| = 1 is false). Earned from
not_qsymmetric_most_sem.
Toy-witnessed counterexamples #
Counterexamples to non-properties of specific determiners need a concrete
witness type; the witness is the toy fragment's ToyEntity.
⟦every⟧ is NOT symmetric. Witness: R=students, S=things; every(students,
things)=true but every(things,students)=false.
⟦no⟧ is NOT positive strong: no(A,A) = false when A is non-empty.
Strong all (= every_sem) is not symmetric, as a property of its
denotation QuantityWord.all.gqDenotation over the ToyEntity witness
([PW06]). The genuine §7 strong-not-symmetric fact,
earned from the denotation rather than the typological .strength label.
The dual of ⟦every⟧ is ⟦some⟧: Q̌(every) = some ([BC81] §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 ([BC81] §4.11).
∀x. R(x) → ¬S(x) = ¬∃x. R(x) ∧ S(x).
Bridges pinnerNeg_every_eq_no to fragment entries.
Outer negation maps ⟦some⟧ to ⟦no⟧: ~some = no ([BC81] §4.11).
¬(∃x. R(x) ∧ S(x)) = ∀x. R(x) → ¬S(x).
Bridges pouterNeg_some_eq_no to fragment entries.
Positive-strong determiners are scope-upward-monotone
([PW06]).
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. ([vdPLvM+23])
- 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.
- conservative_mean_lz : ℚ
- non_conservative_mean_lz : ℚ
Instances For
Quantity-satisfying quantifiers have lower LZ complexity, but the effect is weaker than monotonicity.
- quantity_mean_lz : ℚ
- non_quantity_mean_lz : ℚ
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 [BC81]'s conservativity conjecture (all simple determiners are conservative) to [RS24a]'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)
Appendix C: more than half is not first-order definable #
[BC81] Appendix C (C12, p. 213): over a first-order language
with equality and two unary predicate symbols U, V, no sentence is
true in exactly the finite models where more than half the V's are U's
(2·|U∩V| > |V|). B&C treat most via more than half "to avoid problems
of vagueness"; the theorem is the formal core of their claim that most
must be a determiner, not a quantifier (their C13, deferred).
The proof is the paper's own (pp. 213–214), a hand-rolled Fraïssé argument:
for each m, two structures on Fin (3m+1) — V = [0,2m), U₁ = [0,m),
U₂ = [0,m+1) — disagree on more than half but agree on every formula
with fewer than m quantifiers-plus-free-variables (their condition (6)),
because a region-respecting correspondence can always be extended:
"there is always enough room".
Relation symbols: two unary predicates.
Instances For
Equations
- BarwiseCooper1981.instDecidableEqUvRel.decEq BarwiseCooper1981.uvRel.U BarwiseCooper1981.uvRel.U = isTrue BarwiseCooper1981.instDecidableEqUvRel.decEq._proof_1
- BarwiseCooper1981.instDecidableEqUvRel.decEq BarwiseCooper1981.uvRel.U BarwiseCooper1981.uvRel.V = isFalse BarwiseCooper1981.instDecidableEqUvRel.decEq._proof_2
- BarwiseCooper1981.instDecidableEqUvRel.decEq BarwiseCooper1981.uvRel.V BarwiseCooper1981.uvRel.U = isFalse BarwiseCooper1981.instDecidableEqUvRel.decEq._proof_3
- BarwiseCooper1981.instDecidableEqUvRel.decEq BarwiseCooper1981.uvRel.V BarwiseCooper1981.uvRel.V = isTrue BarwiseCooper1981.instDecidableEqUvRel.decEq._proof_4
Instances For
The monadic language of C12 (equality is built into the formula type).
Equations
- BarwiseCooper1981.L_UV = { Functions := fun (x : ℕ) => Empty, Relations := BarwiseCooper1981.uvRel }
Instances For
Equations
Instances For
Equations
Instances For
Quantifier count of a formula (c(φ) minus the free-variable count in
B&C's notation).
Equations
- BarwiseCooper1981.numQuant FirstOrder.Language.BoundedFormula.falsum = 0
- BarwiseCooper1981.numQuant (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = 0
- BarwiseCooper1981.numQuant (FirstOrder.Language.BoundedFormula.rel R ts) = 0
- BarwiseCooper1981.numQuant (f₁.imp f₂) = BarwiseCooper1981.numQuant f₁ + BarwiseCooper1981.numQuant f₂
- BarwiseCooper1981.numQuant f.all = BarwiseCooper1981.numQuant f + 1
Instances For
Realization in M₁ (structures are term-level, so instances are pinned
explicitly).
Equations
- BarwiseCooper1981.Realize₁ m k φ xs = φ.Realize default xs
Instances For
Realization in M₂.
Equations
- BarwiseCooper1981.Realize₂ m k φ xs = φ.Realize default xs
Instances For
B&C's condition (6) (p. 214): a formula whose quantifier count plus
free-variable count is below m cannot distinguish region-matched tuples
across M₁/M₂. Structural induction; at each quantifier "there is always
enough room to extend the one-one correspondence one more step".
The theorem #
"More than half the V's are U's" over bare predicates
(Card(U ∩ V) > ½ Card(V), B&C p. 213).
Equations
- BarwiseCooper1981.MostUV U V = (2 * {x : M | U x ∧ V x}.ncard > {x : M | V x}.ncard)
Instances For
The more than half truth condition over a structure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
C12 ([BC81], Appendix C p. 213): no first-order sentence over two unary predicates is true in exactly the finite models where more than half the V's are U's. The formal core of B&C's claim that most is a determiner, not a quantifier.
The same result via the general Ehrenfeucht–Fraïssé apparatus #
The proof above is B&C's hand-rolled Fraïssé argument. The same conclusion follows
from the project's general finite-rank EF engine
(Core.Logic.FirstOrder.EhrenfeuchtFraisseGame): build, for each rank k, a pair of
L_UV-structures that are rank-k back-and-forth equivalent yet separated by more
than half, then feed nEquiv_of_backForth into not_foDefinable_of_nEquiv. This
section is a demonstration of that apparatus on a known result — the colored-set
back-and-forth of Libkin, Elements of Finite Model Theory §3 (Cor 3.10 and the two-
unary-predicate "colored sets" example) — alongside, not in place of, B&C's own proof.
The rank-k witnesses are exactly B&C's struc₁/struc₂ instantiated at m = k + 1
on the domain Fin (3·(k+1)+1): the colour classes U∩V, V \ U, and ¬V then each
have matching size or both have size ≥ k + 1, which is the "enough room" condition the
RegionMatch-extension lemmas (extend₁₂/extend₂₁) already discharge.
MoreThanHalf as a property of bundled L_UV-structures, for the EF inexpressibility
corollary not_foDefinable_of_nEquiv.
Equations
- BarwiseCooper1981.MoreThanHalfPred M = BarwiseCooper1981.MoreThanHalf (↑M) M.str
Instances For
Rank-k witness A: U = [0, k+1), V = [0, 2k+2) on Fin (3k+4) — exactly half
the V's are U's, so ¬ MoreThanHalf.
Equations
- BarwiseCooper1981.efWitnessA k = { α := Fin (3 * (k + 1) + 1), str := BarwiseCooper1981.struc₁ (k + 1) (3 * (k + 1) + 1) }
Instances For
Rank-k witness B: U = [0, k+2), V = [0, 2k+2) on Fin (3k+4) — more than half
the V's are U's, so MoreThanHalf.
Equations
- BarwiseCooper1981.efWitnessB k = { α := Fin (3 * (k + 1) + 1), str := BarwiseCooper1981.struc₂ (k + 1) (3 * (k + 1) + 1) }
Instances For
C12 via the general EF apparatus ([BC81] Appendix C, reproved
through Core.Logic.FirstOrder.EhrenfeuchtFraisseGame). More than half the V's are U's
is not first-order definable: for each rank k the structures efWitnessA k and
efWitnessB k are k-equivalent (a colored-set back-and-forth) yet disagree on the
property, so not_foDefinable_of_nEquiv applies. Cf. more_than_half_not_definable, which
proves the same via B&C's own hand-rolled Fraïssé argument; Libkin, Elements of Finite
Model Theory §3 (Cor 3.10 + colored sets).
Appendix C: C13 — most is a determiner, not a quantifier #
[BC81] C13 (pp. 214–215): extend the monadic language with a
quantifier symbol Q, where Qx[φ(x)] means "more than half of all things
satisfy φ". Even in this language, no sentence is true in exactly the finite
models where more than half the V's are U's: the relativized quantifier is
not definable from the unrelativized one. So most cannot be a unary
sentence operator over the domain — it must be a determiner (a footnote
credits a related unpublished 1965 theorem to David Kaplan).
The proof is B&C's: a translation star eliminating Q (Qx θ becomes
"every x outside V and the free variables satisfies θ*"), correct on
models where the domain swamps V (property (P), via "a trivial
automorphism argument"), reducing to C12's models.
Formulas of B&C's L(Q): the monadic language of C12 (atoms U, V,
equality) plus the unrelativized majority quantifier Qx[·]. De Bruijn
indices; atoms apply directly to variables (the language has no function
symbols).
- falsum {n : ℕ} : QFormula n
- equal {n : ℕ} (i j : Fin n) : QFormula n
- isU {n : ℕ} (i : Fin n) : QFormula n
- isV {n : ℕ} (i : Fin n) : QFormula n
- imp {n : ℕ} (f₁ f₂ : QFormula n) : QFormula n
- all {n : ℕ} (f : QFormula (n + 1)) : QFormula n
- qx {n : ℕ} (f : QFormula (n + 1)) : QFormula n
Instances For
Realization over a finite monadic model ⟨E, U, V⟩. The Q clause is
B&C's: more than half of all things satisfy the body.
Equations
- BarwiseCooper1981.QFormula.Realize U V BarwiseCooper1981.QFormula.falsum x✝ = False
- BarwiseCooper1981.QFormula.Realize U V (BarwiseCooper1981.QFormula.equal i j) x✝ = (x✝ i = x✝ j)
- BarwiseCooper1981.QFormula.Realize U V (BarwiseCooper1981.QFormula.isU i) x✝ = U (x✝ i)
- BarwiseCooper1981.QFormula.Realize U V (BarwiseCooper1981.QFormula.isV i) x✝ = V (x✝ i)
- BarwiseCooper1981.QFormula.Realize U V (f₁.imp f₂) x✝ = (BarwiseCooper1981.QFormula.Realize U V f₁ x✝ → BarwiseCooper1981.QFormula.Realize U V f₂ x✝)
- BarwiseCooper1981.QFormula.Realize U V f.all x✝ = ∀ (x : E), BarwiseCooper1981.QFormula.Realize U V f (Fin.snoc x✝ x)
- BarwiseCooper1981.QFormula.Realize U V f.qx x✝ = (2 * {a : E | BarwiseCooper1981.QFormula.Realize U V f (Fin.snoc x✝ a)}.ncard > Fintype.card E)
Instances For
Quantifier count (all and qx both count).
Equations
- BarwiseCooper1981.QFormula.falsum.numQ = 0
- (BarwiseCooper1981.QFormula.equal i j).numQ = 0
- (BarwiseCooper1981.QFormula.isU i).numQ = 0
- (BarwiseCooper1981.QFormula.isV i).numQ = 0
- (f₁.imp f₂).numQ = f₁.numQ + f₂.numQ
- f.all.numQ = f.numQ + 1
- f.qx.numQ = f.numQ + 1
Instances For
Q-freeness: the first-order fragment of L(Q).
Equations
- BarwiseCooper1981.QFormula.falsum.QFree = True
- (BarwiseCooper1981.QFormula.equal i j).QFree = True
- (BarwiseCooper1981.QFormula.isU i).QFree = True
- (BarwiseCooper1981.QFormula.isV i).QFree = True
- (f₁.imp f₂).QFree = (f₁.QFree ∧ f₂.QFree)
- f.all.QFree = f.QFree
- f.qx.QFree = False
Instances For
Negation.
Equations
Instances For
Finite disjunction.
Equations
Instances For
"The last variable equals one of the first n."
Equations
- BarwiseCooper1981.QFormula.eqAny n = BarwiseCooper1981.QFormula.orList (List.map (fun (i : Fin n) => BarwiseCooper1981.QFormula.equal (Fin.last n) i.castSucc) (List.finRange n))
Instances For
B&C's Q-elimination (ψ*, p. 215): Qx θ becomes "every x that is
outside V and distinct from the free variables satisfies θ*".
Equations
- BarwiseCooper1981.QFormula.falsum.star = BarwiseCooper1981.QFormula.falsum
- (BarwiseCooper1981.QFormula.equal i j).star = BarwiseCooper1981.QFormula.equal i j
- (BarwiseCooper1981.QFormula.isU i).star = BarwiseCooper1981.QFormula.isU i
- (BarwiseCooper1981.QFormula.isV i).star = BarwiseCooper1981.QFormula.isV i
- (f₁.imp f₂).star = f₁.star.imp f₂.star
- f.all.star = f.star.all
- f.qx.star = ((BarwiseCooper1981.QFormula.isV (Fin.last x✝)).or ((BarwiseCooper1981.QFormula.eqAny x✝).or f.star)).all
Instances For
L(Q)-realization is invariant under automorphisms of the monadic model
(B&C's "trivial automorphism argument", p. 215).
The Q-free condition (6): the C12 argument for the L(Q) fragment
over the C12 model pair.
B&C's property (P) (p. 215): on models with U ⊆ V whose domain is at
least twice |V| plus the complexity of ψ, the Q-elimination star is
correct — the domain "swamps out" U and V.
C13 ([BC81], Appendix C pp. 214–215): even with the
unrelativized majority quantifier Qx[·] ("more than half of all things")
available, no sentence of L(Q) is true in exactly the finite models where
more than half the V's are U's. The relativized quantifier is not definable
from the unrelativized one: most must be treated as a determiner, not a
quantifier. (B&C credit a related unpublished 1965 theorem to David Kaplan.)
The truth condition is the codebase's ⟦most⟧ #
The C12/C13 truth condition is most_sem with V as restrictor — the
theorems are about the denotation the rest of the codebase attributes to
most, not a local re-implementation.
C12 restated through most_sem: no first-order sentence expresses
the codebase's ⟦most⟧ over finite models.
The engine-level corollary: no fragment tree means most #
No tree of the compiled fragment means most: for any logical
vocabulary and disjoint naming maps over L_UV, no closed tree of the FO
fragment has, across all nonempty finite models, exactly ⟦most⟧'s truth
conditions — C12 stated about Tree.interp itself, via the agreement
theorem holdsAt_iff_realize. The fragment's partiality at most is a
theorem, not a design choice.