Barwise and Cooper 1981: generalized quantifiers and natural language

A noun phrase denotes a quantifier — a family of subsets of the domain — and a determiner assigns to each set A a quantifier that lives on A (the paper's determiner universal, the one condition the logic imposes on non-logical determiners). The classifications of §4 are conditions on such families. A determiner is positive (negative) strong when A always (never) lies in D(A) and weak otherwise; definite when D(A) is a principal filter with a nonempty generator; a quantifier is monotone when closed under supersets or subsets, and outer negation, inner negation and the dual exchange the two directions. Appendix C's propositions are general: a quantifier living on A contains A iff it contains the domain, so a strong determiner's there-sentence is trivial (C1); definite determiners are positive strong (C2, C3); the intersection condition is symmetry, and no proper strong determiner has it (C4–C6); persistent symmetric determiners are increasing (C7); positive strong increasing determiners validate D N that VP, VP (C8); negation reverses monotonicity (C9); an increasing quantifier and its dual overlap (C10); a monotone quantifier is decided by its witness sets (C11). C12 and C13 prove that more than half is definable neither in first-order logic nor from the unrelativized majority quantifier, so most is a determiner, not a quantifier. The fragment's quantity words instantiate Table II, and the paper's own artificial determiners witness that the universals U6–U8 are not logical truths. Under the substrate's proportional reading of few (fewer than half), few N are N is contradictory, so few comes out negative strong — B&C's Table II lists few as weak, a classification their own §4.8 discussion of many and few already marks as unstable. Partial determiners (the n, both, neither) fall outside the total type GQ α and are not treated.

Main results

• livesOn_apply_iff, there_of_positiveStrong, Definite.positiveStrong: C1–C3.
• strong_trivial_of_intersective, scopeUp_of_restrictorUp_symmetric: C6 and C7.
• exists_and_of_scopeUp_dual: C10, with most_selfDual_of_odd_count.
• more_than_half_not_definable, more_than_half_not_Q_definable: C12 and C13, with no_tree_means_most, no tree of first-order constants means most.

References

• [BC81]
• [Mil77]
• [Mos57]

Quantifiers and witness sets

def BarwiseCooper1981.Sieve {α : Type u_1} (Q : Quantifier.NP α) : Prop

A proper quantifier, or sieve, is one that some set passes and some set fails (§4.5).

Equations

• BarwiseCooper1981.Sieve Q = ((∃ (X : α → Prop), Q X) ∧ ∃ (X : α → Prop), ¬Q X)

def BarwiseCooper1981.principalFilter {α : Type u_1} (B : α → Prop) : Quantifier.NP α

The principal filter generated by B consists of the sets containing B (§4.6).

Equations

• BarwiseCooper1981.principalFilter B X = ∀ (x : α), B x → X x

theorem BarwiseCooper1981.livesOn_apply_iff {α : Type u_1} {Q : Quantifier.NP α} {A : α → Prop} (h : Q.LivesOn A) : Q A ↔ Q fun (x : α) => True

A quantifier living on A contains A iff it contains the domain (C1).

theorem BarwiseCooper1981.principalFilter_livesOn_iff {α : Type u_1} {A B : α → Prop} : (principalFilter B).LivesOn A ↔ ∀ (x : α), B x → A x

The principal filter generated by B lives on A iff B ⊆ A (C2).

theorem BarwiseCooper1981.sieve_principalFilter {α : Type u_1} {B : α → Prop} (hB : ∃ (x : α), B x) : Sieve (principalFilter B)

A principal filter with a nonempty generator is a sieve.

theorem BarwiseCooper1981.not_monotone_mixed_conjunction : ¬Monotone (Quantifier.NP.individual true ⊓ Quantifier.GQ.no fun (x : Bool) => x = false) ∧ ¬Antitone (Quantifier.NP.individual true ⊓ Quantifier.GQ.no fun (x : Bool) => x = false)

A mixed conjunction of an increasing and a decreasing quantifier, John and no woman, is neither increasing nor decreasing (§4.10).

Determiners: strength, definiteness, and the intersection condition

def BarwiseCooper1981.Strong {α : Type u_1} (D : Quantifier.GQ α) : Prop

A determiner is strong when it is positive or negative strong (§4.6).

Equations

• BarwiseCooper1981.Strong D = (D.PositiveStrong ∨ D.NegativeStrong)

def BarwiseCooper1981.Weak {α : Type u_1} (D : Quantifier.GQ α) : Prop

A determiner is weak when it is neither positive nor negative strong (§4.6).

Equations

• BarwiseCooper1981.Weak D = ¬BarwiseCooper1981.Strong D

def BarwiseCooper1981.Definite {α : Type u_1} (D : Quantifier.GQ α) : Prop

A determiner is definite when every D(A) is the principal filter of a nonempty generator (§4.6).

Equations

• BarwiseCooper1981.Definite D = ∀ (A : α → Prop), ∃ (B : α → Prop), (∃ (x : α), B x) ∧ ∀ (X : α → Prop), D A X ↔ ∀ (x : α), B x → X x

def BarwiseCooper1981.SelfDual {α : Type u_1} (D : Quantifier.GQ α) : Prop

Self-dual (§4.11).

Equations

• BarwiseCooper1981.SelfDual D = (D.dual = D)

theorem BarwiseCooper1981.there_of_positiveStrong {α : Type u_1} {D : Quantifier.GQ α} (hc : D.Conservative) (h : D.PositiveStrong) (A : α → Prop) : D A fun (x : α) => True

The there-sentence of a positive strong determiner is a tautology (§4.6), since there are D N says the domain lies in D(N), which C1 reduces to N ∈ D(N).

theorem BarwiseCooper1981.not_there_of_negativeStrong {α : Type u_1} {D : Quantifier.GQ α} (hc : D.Conservative) (h : D.NegativeStrong) (A : α → Prop) : ¬D A fun (x : α) => True

The there-sentence of a negative strong determiner is a contradiction (§4.6).

theorem BarwiseCooper1981.Definite.positiveStrong {α : Type u_1} {D : Quantifier.GQ α} (hc : D.Conservative) (hd : Definite D) : D.PositiveStrong

Definite determiners are positive strong (C3).

theorem BarwiseCooper1981.apply_univ_inter_of_intersective {α : Type u_1} {D : Quantifier.GQ α} (h : D.IntersectionCondition) (A B : α → Prop) : D A B ↔ D (fun (x : α) => A x ∧ B x) fun (x : α) => True

Under the intersection condition, B ∈ D(A) iff the domain lies in D(A ∩ B), the there is/are paraphrase of weak determiners (C4).

theorem BarwiseCooper1981.strong_trivial_of_intersective {α : Type u_1} {D : Quantifier.GQ α} (h : D.IntersectionCondition) : (D.PositiveStrong → ∀ (A B : α → Prop), D A B) ∧ (D.NegativeStrong → ∀ (A B : α → Prop), ¬D A B)

A strong determiner satisfying the intersection condition is trivial, since positive strong makes every D(A) everything and negative strong makes it empty; so no proper strong determiner is symmetric (C6).

theorem BarwiseCooper1981.scopeUp_of_restrictorUp_symmetric {α : Type u_1} {D : Quantifier.GQ α} (hp : D.RestrictorMonotone) (hs : Std.Symm D) : D.ScopeMonotone

A persistent symmetric determiner is increasing (C7).

theorem BarwiseCooper1981.apply_inter_of_positiveStrong_scopeUp {α : Type u_1} {D : Quantifier.GQ α} (hps : D.PositiveStrong) (hm : D.ScopeMonotone) (A B : α → Prop) : D (fun (x : α) => A x ∧ B x) B

A positive strong increasing determiner validates D N that VP, VP, since the scope lies in D of the intersected restrictor (C8).

theorem BarwiseCooper1981.scopeMonotone_dual {α : Type u_1} {D : Quantifier.GQ α} (h : D.ScopeMonotone) : D.dual.ScopeMonotone

The dual of an increasing quantifier is increasing (C9 for the dual).

theorem BarwiseCooper1981.exists_and_of_scopeUp_dual {α : Type u_1} {D : Quantifier.GQ α} (hm : D.ScopeMonotone) {R A B : α → Prop} (hA : D R A) (hB : D.dual R B) : ∃ (x : α), A x ∧ B x

An increasing quantifier and its dual overlap, since D(R)(A) and Ď(R)(B) force a common member of A and B (C10).

§4.8's artificial strong-but-not-increasing determiner shows U7 (positive strong determiners are increasing) is not a logical truth.

def BarwiseCooper1981.evenOutside {α : Type u_1} : Quantifier.GQ α

X ∈ D(A) iff X ∖ A is even — positive strong, but not increasing (§4.8).

Equations

• BarwiseCooper1981.evenOutside A X = Even {x : α | X x ∧ ¬A x}.ncard

theorem BarwiseCooper1981.positiveStrong_evenOutside {α : Type u_1} : evenOutside.PositiveStrong

theorem BarwiseCooper1981.not_scopeUp_evenOutside : ¬evenOutside.ScopeMonotone

§4.9's some but not all is persistent but neither increasing nor symmetric, so U8 (persistent determiners are increasing and weak) is not a logical truth either.

def BarwiseCooper1981.someNotAll {α : Type u_1} : Quantifier.GQ α

X ∈ D(A) iff some but not all of A is in X (Appendix C, after C6).

Equations

• BarwiseCooper1981.someNotAll A X = ((∃ (x : α), A x ∧ X x) ∧ ∃ (x : α), A x ∧ ¬X x)

theorem BarwiseCooper1981.restrictorUp_someNotAll {α : Type u_1} : someNotAll.RestrictorMonotone

theorem BarwiseCooper1981.not_scopeUp_someNotAll : ¬someNotAll.ScopeMonotone

theorem BarwiseCooper1981.not_symm_someNotAll : ¬Std.Symm someNotAll

The English quantity words (Table II and §4.7)

theorem BarwiseCooper1981.few_negativeStrong {α : Type u_1} : Quantifier.GQ.few.NegativeStrong

Under the proportional reading (fewer than half), few N are N is contradictory, so few is negative strong, where B&C's Table II lists few as weak.

theorem BarwiseCooper1981.some_weak {α : Type u_1} [Nonempty α] : Weak Quantifier.GQ.some

Some is weak (Table II), since some N is a N is contingent.

theorem BarwiseCooper1981.no_weak {α : Type u_1} [Nonempty α] : Weak Quantifier.GQ.no

No is weak (Table II), since no N is a N is contingent.

theorem BarwiseCooper1981.half_weak : Weak Quantifier.GQ.half

Exactly half, the non-monotone determiner of §4.7, is weak, since half the N are N is contingent, witnessed over Fin 3.

def BarwiseCooper1981.atLeastHalf {α : Type u_1} : Quantifier.GQ α

The lower half of exactly half puts at least half the restrictor in the scope.

Equations

• BarwiseCooper1981.atLeastHalf = (Quantifier.NumberTree.ofSizes fun (x p : ℕ) => p ≤ 2 * x).toGQ

def BarwiseCooper1981.atMostHalf {α : Type u_1} : Quantifier.GQ α

The upper half of exactly half puts at most half the restrictor in the scope.

Equations

• BarwiseCooper1981.atMostHalf = (Quantifier.NumberTree.ofSizes fun (x p : ℕ) => 2 * x ≤ p).toGQ

theorem BarwiseCooper1981.half_eq_meet {α : Type u_1} : Quantifier.GQ.half = atLeastHalf ⊓ atMostHalf

U6 for exactly half, the non-monotone example of §4.8, says that the non-monotone determiner is the conjunction of an increasing and a decreasing one, as the monotonicity constraint requires of simple NPs; exactly n decomposes likewise (Quantifier.GQ.exactly_eq_atLeast_inf_atMost). On the tree the halves are a ≤ b and b ≤ a, and their meet is a = b.

theorem BarwiseCooper1981.atLeastHalf_scopeUp {α : Type u_1} [Fintype α] : atLeastHalf.ScopeMonotone

theorem BarwiseCooper1981.atMostHalf_scopeDown {α : Type u_1} [Fintype α] : atMostHalf.ScopeAntitone

theorem BarwiseCooper1981.all_positiveStrong {α : Type u_1} [Fintype α] {d : Quantifier.GQ.Family} (h : d ∈ Semantics.Denotes.denote English.Determiners.QuantityWord.all) : (d α).PositiveStrong

Every available reading of all is positive strong (Table II).

theorem BarwiseCooper1981.most_apply_self {α : Type u_1} [Fintype α] {d : Quantifier.GQ.Family} (hd : d ∈ Semantics.Denotes.denote English.Determiners.QuantityWord.most) (A : α → Prop) (h : ∃ (x : α), A x) : d α A A

Most is positive strong on nonempty restrictors (Table II; Appendix B's SP1), since most N are N whenever there are Ns. On the empty restrictor the proportional reading fails, as in Barwise and Cooper's Table I column, so most N can denote the empty quantifier.

theorem BarwiseCooper1981.most_selfDual_of_odd_count {α : Type u_1} [Fintype α] {A : α → Prop} (h : Odd {x : α | A x}.ncard) (S : α → Prop) : Quantifier.GQ.most.dual A S ↔ Quantifier.GQ.most A S

On a restrictor of odd size, more than half is self-dual (§4.11).

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.

The proof is the paper's "Fraïssé method" (pp. 213–214): for each m, two models on Fin k — V = [0, 2m), U₁ = [0, m), U₂ = [0, m+1) — disagree on more than half but agree on every sentence with fewer than m quantifiers, their (5). B&C prove (5) by extending a one-one correspondence that respects U and V one step at each quantifier, their (6), since "there is always enough room": below m, every Venn region of the two models is either the same set or large in both. That argument is the Ehrenfeucht–Fraïssé game on monadic models, so (5) is elementarilyEquivalentUpTo_monadicStructure_iff applied to the two models (elementarilyEquivalentUpTo_struc), for quantifier rank, which is at most the number of quantifiers. The language is Language.monadic (Fin 2), with U as pred 0 and V as pred 1.

@[reducible]

def BarwiseCooper1981.struc₁ (m k : ℕ) : (FirstOrder.Language.monadic (Fin 2)).Structure (Fin k)

The structure M₁, in which U is [0, m) and V is [0, 2m), so that exactly half the V's are U's.

Equations

• BarwiseCooper1981.struc₁ m k = FirstOrder.Language.monadicStructure (Fin k) ![fun (x : Fin k) => ↑x < m, fun (x : Fin k) => ↑x < 2 * m]

@[reducible]

def BarwiseCooper1981.struc₂ (m k : ℕ) : (FirstOrder.Language.monadic (Fin 2)).Structure (Fin k)

The structure M₂, in which U is [0, m+1) and V is [0, 2m), so that more than half the V's are U's.

Equations

• BarwiseCooper1981.struc₂ m k = FirstOrder.Language.monadicStructure (Fin k) ![fun (x : Fin k) => ↑x < m + 1, fun (x : Fin k) => ↑x < 2 * m]

theorem BarwiseCooper1981.elementarilyEquivalentUpTo_struc (m k : ℕ) (hm : 0 < m) (hk : 2 * m ≤ k) : (FirstOrder.Language.monadic (Fin 2)).ElementarilyEquivalentUpTo (m - 1) (Fin k) (Fin k)

B&C's (5) says that the two models agree on every sentence with fewer than m quantifiers; for quantifier rank this is (m - 1)-equivalence, since each Venn region of U and V is either the same set in both models or has at least m - 1 elements in both. The region outside V is the same set, so 2m ≤ k suffices where B&C take k ≥ 3m.

The theorem

def BarwiseCooper1981.MostUV {M : Type} (U V : M → Prop) : Prop

"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)

def BarwiseCooper1981.MoreThanHalf (M : Type) (S : (FirstOrder.Language.monadic (Fin 2)).Structure M) : Prop

The more than half truth condition over a structure.

Equations

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

theorem BarwiseCooper1981.more_than_half_not_definable : ¬∃ (φ : (FirstOrder.Language.monadic (Fin 2)).Sentence), ∀ (M : Type) [Fintype M] [Nonempty M] (S : (FirstOrder.Language.monadic (Fin 2)).Structure M), M ⊨ φ ↔ MoreThanHalf M S

C12 of [BC81] (Appendix C p. 213) says that 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 the claim that most is a determiner, not a quantifier.

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 from L(Q) into the first-order language of C12 (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"); the C12 models then agree on φ* by (5), "since φ* is a first-order sentence with c(φ*) < m".

inductive BarwiseCooper1981.QFormula : ℕ → Type

The formulas of Barwise and Cooper's L(Q), the monadic language of C12 with the atoms U, V and equality plus the unrelativized majority quantifier Qx[·], in de Bruijn indices; atoms apply directly to variables, since 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

def BarwiseCooper1981.QFormula.Realize {E : Type} [Fintype E] (U V : E → Prop) {n : ℕ} : QFormula n → (Fin n → E) → Prop

ψ.Realize U V xs is realization over the finite monadic model ⟨E, U, V⟩, where Qx θ holds when more than half of all things satisfy θ.

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)

def BarwiseCooper1981.QFormula.numQ {n : ℕ} : QFormula n → ℕ

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

noncomputable def BarwiseCooper1981.QFormula.star {n : ℕ} : QFormula n → (FirstOrder.Language.monadic (Fin 2)).BoundedFormula Empty n

B&C's Q-elimination ψ* (p. 215) translates L(Q) into the first-order language of C12, sending Qx θ to "every x is in V, equal to a free variable, or satisfies θ*".

Equations

• One or more equations did not get rendered due to their size.
• BarwiseCooper1981.QFormula.falsum.star = ⊥
• (BarwiseCooper1981.QFormula.equal i j).star = ((FirstOrder.Language.var ∘ Sum.inr) i).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) j)
• (BarwiseCooper1981.QFormula.isU i).star = FirstOrder.Language.Relations.boundedFormula₁ (FirstOrder.Language.monadicRel.pred 0) ((FirstOrder.Language.var ∘ Sum.inr) i)
• (BarwiseCooper1981.QFormula.isV i).star = FirstOrder.Language.Relations.boundedFormula₁ (FirstOrder.Language.monadicRel.pred 1) ((FirstOrder.Language.var ∘ Sum.inr) i)
• (f₁.imp f₂).star = f₁.star.imp f₂.star
• f.all.star = f.star.all

theorem BarwiseCooper1981.QFormula.qr_star_le {n : ℕ} (ψ : QFormula n) : ψ.star.qr ≤ ψ.numQ

The translation adds no quantifier nesting beyond ψ's quantifier count, a form of B&C's c(ψ*) = c(ψ) (p. 215).

theorem BarwiseCooper1981.QFormula.realize_equivMap {E : Type} [Fintype E] {U V : E → Prop} (σ : E ≃ E) (hU : ∀ (x : E), U (σ x) ↔ U x) (hV : ∀ (x : E), V (σ x) ↔ V x) {n : ℕ} (f : QFormula n) (xs : Fin n → E) : Realize U V f (⇑σ ∘ xs) ↔ Realize U V f xs

L(Q)-realization is invariant under automorphisms of the monadic model (B&C's "trivial automorphism argument", p. 215).

theorem BarwiseCooper1981.QFormula.realize_star_iff {E : Type} [Fintype E] {U V : E → Prop} (hUV : ∀ (x : E), U x → V x) {n : ℕ} (ψ : QFormula n) : 2 * ({x : E | V x}.ncard + (ψ.numQ + n)) ≤ Fintype.card E → ∀ (xs : Fin n → E), ψ.star.Realize default xs ↔ Realize U V ψ xs

Barwise and Cooper's property (P) (p. 215) says that on models with U ⊆ V whose domain is at least twice |V| plus the complexity of ψ, the Q-elimination star is correct, since the domain "swamps out" U and V.

theorem BarwiseCooper1981.more_than_half_not_Q_definable : ¬∃ (φ : QFormula 0), ∀ (E : Type) [inst : Fintype E] (U V : E → Prop), QFormula.Realize U V φ default ↔ MostUV U V

C13 of [BC81] (Appendix C pp. 214–215) says that even with the unrelativized majority quantifier Qx[·], "more than half of all things", 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, so most must be treated as a determiner, not a quantifier. Barwise and Cooper credit a related unpublished 1965 theorem to David Kaplan.

The truth condition is the codebase's (most : GQ α)

theorem BarwiseCooper1981.mostUV_iff_most_sem {M : Type} [Fintype M] (U V : M → Prop) : MostUV U V ↔ Quantifier.GQ.most V U

The C12/C13 truth condition is most with V as restrictor — the theorems are about the denotation the rest of the codebase attributes to most, not a local re-implementation.

theorem BarwiseCooper1981.most_sem_not_definable : ¬∃ (φ : (FirstOrder.Language.monadic (Fin 2)).Sentence), ∀ (M : Type) [Fintype M] [Nonempty M] (S : (FirstOrder.Language.monadic (Fin 2)).Structure M), M ⊨ φ ↔ Quantifier.GQ.most (fun (x : M) => FirstOrder.Language.Structure.RelMap (FirstOrder.Language.monadicRel.pred 1) ![x]) fun (x : M) => FirstOrder.Language.Structure.RelMap (FirstOrder.Language.monadicRel.pred 0) ![x]

C12 restated through most says that no first-order sentence expresses most over finite models.

The engine-level corollary: no tree means most

theorem BarwiseCooper1981.no_tree_means_most {C X : Type} (words : X → Option ((ty : Montague.Ty) × HeimKratzer.FirstOrderConstant (FirstOrder.Language.monadic (Fin 2)) ty)) : ¬∃ (t : PhraseStructure.Tree C X), ∀ (M : Type) [Fintype M] [Nonempty M] (S : (FirstOrder.Language.monadic (Fin 2)).Structure M) (g : Assignment M), HeimKratzer.Tree.HoldsAt ((HeimKratzer.Model.ofStructure M S).lexicon words ()) g t ↔ Quantifier.GQ.most (fun (x : M) => FirstOrder.Language.Structure.RelMap (FirstOrder.Language.monadicRel.pred 1) ![x]) fun (x : M) => FirstOrder.Language.Structure.RelMap (FirstOrder.Language.monadicRel.pred 0) ![x]

No tree means most. Under any translation of words into the first-order constants of the language of C12, no tree has, across all nonempty finite models and under every assignment, the truth conditions of most. A tree whose logical form has type t reads back to a first-order formula whose universal closure would define most, against C12; any other tree is true in no model, while most is true in the one-element model where both predicates hold.