Elliott (2025): Determiners as predicates

Elliott proposes that a determiner denotes a predicate of groups of polarized individuals rather than a relation between sets. Every individual x has a positive version x⁺ and a negative version x⁻, no group contains both, and a noun denotes its maximal groups: its extension divided in every possible way into positive and negative individuals. Exactly two holds of the groups with two positive individuals, and a sentence says that some group of the noun satisfies the determiner while the scope holds of its positive and fails of its negative individuals. A group records which members of the restrictor are outside the scope, so these truth conditions are those of generalized quantifier theory, and the determiners expressible this way are exactly the conservative ones.

Main statements

• classical_lessThan_iff_some, classical_zero_false: on plain pluralities, less than three boys sneezed says only that some boy sneezed, and zero boys sneezed is false.
• partsOrderIso: groups ordered by parthood are the sets of polarized individuals that never contain both versions of one individual, ordered by inclusion.
• setOf_noun, delta_iff_le: the groups of a noun are its extension polarized in every possible way, and the ∆-operator for a predicate holds of the parts of the group polarized by it.
• sentence_iff: a sentence holds when the determiner holds of the noun's extension polarized by the scope.
• lessThan_three_matches_judgments: unlike the classical entry, less than three gets the judgments about upper bounds and existential entailment right.
• toGQ_exactly, toGQ_lessThan, toGQ_all, toGQ_most: the predicted truth conditions are those of the generalized quantifiers.
• toGQ_ofGQ_eq_iff, conservative_toGQ, consGQOrderIso: a generalized quantifier survives the round trip through predicates exactly when it is conservative, and the predicates are order isomorphic to the conservative quantifiers, whose atoms are the groups (ofGQ_atom).
• card_predicates, eqOn_ofGQ_iff: on n individuals there are 2 ^ (3 ^ n - 1) predicates of nonempty groups, and they determine a conservative quantifier up to its value at the empty restrictor.
• all_scopeless, exactly_two_not_individual: existential raising of all N is a Montague individual and so scopeless, while that of exactly two N is not.
• not_some_singular_collective: some boy gathered is false of a collective predicate.
• whichDeRe_eq_ker, relevant_of_conservative: the answers to which N did B? correspond to the groups of the noun, so every conservative determiner is relevant to the question.

Implementation notes

A group is a function into Flat Bool, the paper's trivalent presentation: ⊥ for an absent individual and ↑true, ↑false for the two polarities. Parthood is the pointwise flat order, so no group contains both versions of an individual. Nouns, like determiners, are predicates of groups, and the paper's covert existential determiner is GQ.some at groups. The paper's domain has no empty group; PolarGroup α has one, ⊥, with which predicates match the conservative quantifiers exactly and all N and no N are singletons even for an empty noun. Restricting to X ≠ ⊥ recovers the paper's count and its correspondence up to the empty restrictor. The classical theory's pluralities are nonempty Finsets, and a collective predicate is one true of no atom.

TODO

• The paper says that the ∆-operator of a collective predicate is true of no group of a singular noun, but it is true of the wholly negative group (delta_collective_iff); some boy gathered is false all the same, since some requires a positive atom.
• The plural numerals of the last section, which count the atoms inside a positive atom.

References

• [Ell25]
• [BC81]
• [KS86]
• [Lin83]
• [Lin87b]
• [Rot17b]
• [vB86]
• [BN18]
• [Sch02]
• [GS84]

The classical predicative theory

def Elliott2025.classicalSentence {α : Type u_1} (D : Finset α → Prop) (N vp : α → Prop) : Prop

On the classical predicative theory a determiner D is a predicate of pluralities, here nonempty finite sets, and a sentence says that some plurality satisfying D consists of N-individuals that each satisfy the scope vp.

Equations

• Elliott2025.classicalSentence D N vp = ∃ (X : Finset α), X.Nonempty ∧ D X ∧ (∀ x ∈ X, N x) ∧ ∀ x ∈ X, vp x

theorem Elliott2025.classical_lessThan_iff_some {α : Type u_1} {N vp : α → Prop} {n : ℕ} (hn : 1 < n) : classicalSentence (fun (x : Finset α) => x.card < n) N vp ↔ Quantifier.GQ.some N vp

Van Benthem's problem is that every part of a plurality that satisfies the scope satisfies it too, so less than n N vp says only that some N satisfies vp.

theorem Elliott2025.classical_zero_false {α : Type u_1} {N vp : α → Prop} : ¬classicalSentence (fun (x : Finset α) => x.card = 0) N vp

The problem of zero is that every plurality has an atom, so zero is never satisfied.

Groups of polarized individuals

@[reducible, inline]

abbrev Elliott2025.PolarGroup (α : Type u_2) : Type u_2

A group of polarized individuals sends an individual x to ↑true when x⁺ is a part of it, to ↑false when x⁻ is, and to ⊥ when neither is; parthood is the pointwise order.

Equations

• Elliott2025.PolarGroup α = (α → Flat Bool)

def Elliott2025.PolarGroup.posAtoms {α : Type u_1} (X : PolarGroup α) : Set α

The positive atoms of a group are the individuals it contains positively.

Equations

• X.posAtoms = {x : α | X x = ↑true}

def Elliott2025.PolarGroup.negAtoms {α : Type u_1} (X : PolarGroup α) : Set α

The negative atoms of a group are the individuals it contains negatively.

Equations

• X.negAtoms = {x : α | X x = ↑false}

def Elliott2025.PolarGroup.atoms {α : Type u_1} (X : PolarGroup α) : Set α

The atoms of a group are the individuals it contains with either polarity.

Equations

• X.atoms = {x : α | X x ≠ ⊥}

def Elliott2025.PolarGroup.parts {α : Type u_1} (X : PolarGroup α) : Set (α × Bool)

The atomic parts of a group are polarized individuals, (x, true) for x⁺ and (x, false) for x⁻.

Equations

• X.parts = {p : α × Bool | X p.1 = ↑p.2}

def Elliott2025.PolarGroup.delta {α : Type u_1} (X : PolarGroup α) (f : α → Prop) : Prop

The ∆-operator predicates f of a group distributively, requiring that f hold of x for each atomic part x⁺ and fail of x for each atomic part x⁻.

Equations

• X.delta f = ∀ p ∈ X.parts, f p.1 ↔ p.2 = true

theorem Elliott2025.PolarGroup.le_iff_parts_subset {α : Type u_1} {X Y : PolarGroup α} : X ≤ Y ↔ X.parts ⊆ Y.parts

Parthood is inclusion of atomic parts.

theorem Elliott2025.PolarGroup.posAtoms_subset_atoms {α : Type u_1} {X : PolarGroup α} : X.posAtoms ⊆ X.atoms

theorem Elliott2025.PolarGroup.atoms_diff_posAtoms {α : Type u_1} {X : PolarGroup α} : X.atoms \ X.posAtoms = X.negAtoms

@[simp]

theorem Elliott2025.PolarGroup.atoms_eq_empty_iff {α : Type u_1} {X : PolarGroup α} : X.atoms = ∅ ↔ X = ⊥

def Elliott2025.Coherent {α : Type u_1} (A : Set (α × Bool)) : Prop

A set of polarized individuals is coherent when it contains no individual with both polarities.

Equations

• Elliott2025.Coherent A = ∀ (x : α), ¬((x, true) ∈ A ∧ (x, false) ∈ A)

noncomputable def Elliott2025.partsOrderIso {α : Type u_1} : PolarGroup α ≃o { A : Set (α × Bool) // Coherent A }

Groups ordered by parthood are the coherent sets of polarized individuals ordered by inclusion, the empty group corresponding to the empty set.

Equations

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

noncomputable def Elliott2025.polarize {α : Type u_1} (N vp : α → Prop) : PolarGroup α

polarize N vp is the group of the N-individuals, each positive if it satisfies vp and negative otherwise.

Equations

• Elliott2025.polarize N vp x = if N x then ↑(decide (vp x)) else ⊥

@[simp]

theorem Elliott2025.atoms_polarize {α : Type u_1} {N vp : α → Prop} : (polarize N vp).atoms = {x : α | N x}

@[simp]

theorem Elliott2025.posAtoms_polarize {α : Type u_1} {N vp : α → Prop} : (polarize N vp).posAtoms = {x : α | N x ∧ vp x}

@[simp]

theorem Elliott2025.negAtoms_polarize {α : Type u_1} {N vp : α → Prop} : (polarize N vp).negAtoms = {x : α | N x ∧ ¬vp x}

theorem Elliott2025.polarize_eq_polarize_iff {α : Type u_1} {N vp vp' : α → Prop} : polarize N vp = polarize N vp' ↔ ∀ (x : α), N x → (vp x ↔ vp' x)

Two polarizations of N agree exactly when their scopes agree on N.

theorem Elliott2025.polarize_ne_bot_iff {α : Type u_1} {N vp : α → Prop} : polarize N vp ≠ ⊥ ↔ ∃ (x : α), N x

theorem Elliott2025.polarize_atoms_posAtoms {α : Type u_1} (X : PolarGroup α) : (polarize (fun (x : α) => x ∈ X.atoms) fun (x : α) => x ∈ X.posAtoms) = X

A group is its atoms polarized by its positive atoms.

theorem Elliott2025.delta_polarize_iff {α : Type u_1} {N vp vp' : α → Prop} : (polarize N vp).delta vp' ↔ ∀ (x : α), N x → (vp' x ↔ vp x)

theorem Elliott2025.delta_iff_le {α : Type u_1} {vp : α → Prop} {X : PolarGroup α} : X.delta vp ↔ X ≤ polarize ⊤ vp

The ∆-operator for f holds exactly of the parts of the group that polarizes every individual by f.

def Elliott2025.noun {α : Type u_1} (N : α → Prop) : PolarGroup α → Prop

A noun holds of the maximal groups whose atoms all fall under it.

Equations

• Elliott2025.noun N = Maximal fun (X : Elliott2025.PolarGroup α) => ∀ x ∈ X.atoms, N x

theorem Elliott2025.noun_iff {α : Type u_1} {N : α → Prop} {X : PolarGroup α} : noun N X ↔ X.atoms = {x : α | N x}

The groups of a noun are those whose atoms are exactly its extension.

theorem Elliott2025.noun_polarize {α : Type u_1} (N vp : α → Prop) : noun N (polarize N vp)

theorem Elliott2025.setOf_noun {α : Type u_1} {N : α → Prop} : {X : PolarGroup α | noun N X} = Set.range (polarize N)

The groups of a noun are its extension polarized by every possible scope, one for each division of the extension into positive and negative atoms.

theorem Elliott2025.noun_iff_exists {α : Type u_1} {N : α → Prop} {X : PolarGroup α} : noun N X ↔ ∃ (S : α → Prop), polarize N S = X

theorem Elliott2025.delta_iff_eq_polarize {α : Type u_1} {N vp : α → Prop} {X : PolarGroup α} (hX : noun N X) : X.delta vp ↔ X = polarize N vp

On the groups of a noun, the ∆-operator for vp holds only of the noun's extension polarized by vp.

Determiners as predicates

@[reducible, inline]

abbrev Elliott2025.Det (α : Type u_2) : Type u_2

A determiner denotes a predicate of groups.

Equations

• Elliott2025.Det α = (Elliott2025.PolarGroup α → Prop)

def Elliott2025.Det.atLeast {α : Type u_1} (n : ℕ) : Det α

A bare numeral has an at-least meaning, so two holds of groups with at least two positive atoms.

Equations

• Elliott2025.Det.atLeast n X = (n ≤ X.posAtoms.ncard)

def Elliott2025.Det.exactly {α : Type u_1} (n : ℕ) : Det α

Exactly n holds of groups with n positive atoms; zero is exactly 0.

Equations

• Elliott2025.Det.exactly n X = (X.posAtoms.ncard = n)

def Elliott2025.Det.lessThan {α : Type u_1} (n : ℕ) : Det α

Less than n holds of groups with fewer than n positive atoms.

Equations

• Elliott2025.Det.lessThan n X = (X.posAtoms.ncard < n)

def Elliott2025.Det.all {α : Type u_1} : Det α

All holds of groups without negative atoms.

Equations

• Elliott2025.Det.all X = (X.negAtoms = ∅)

def Elliott2025.Det.some {α : Type u_1} : Det α

Some holds of groups with a positive atom.

Equations

• Elliott2025.Det.some X = (X.posAtoms ≠ ∅)

def Elliott2025.Det.notAll {α : Type u_1} : Det α

Not all is the negation of all.

Equations

• Elliott2025.Det.notAll = Elliott2025.Det.allᶜ

def Elliott2025.Det.none {α : Type u_1} : Det α

None is the negation of some.

Equations

• Elliott2025.Det.none = Elliott2025.Det.someᶜ

def Elliott2025.Det.most {α : Type u_1} : Det α

Most holds of groups with more positive than negative atoms.

Equations

• Elliott2025.Det.most X = (X.negAtoms.ncard < X.posAtoms.ncard)

def Elliott2025.Det.ofGQ {α : Type u_1} (Q : Quantifier.GQ α) : Det α

A generalized quantifier yields a predicate by applying it to the atoms and the positive atoms of a group.

Equations

• Elliott2025.Det.ofGQ Q X = Q (fun (x : α) => x ∈ X.atoms) fun (x : α) => x ∈ X.posAtoms

def Elliott2025.sentence {α : Type u_1} (D : Det α) (N vp : α → Prop) : Prop

In a simple distributive sentence the determiner modifies the noun intersectively, and the covert existential determiner GQ.some relates the resulting predicate to the ∆-operator applied to the scope.

Equations

• Elliott2025.sentence D N vp = Quantifier.GQ.some (D ⊓ Elliott2025.noun N) fun (x : Elliott2025.PolarGroup α) => x.delta vp

def Elliott2025.Det.toGQ {α : Type u_1} (D : Det α) : Quantifier.GQ α

A determiner yields a generalized quantifier through the truth conditions of its sentences.

Equations

• D.toGQ = Elliott2025.sentence D

theorem Elliott2025.sentence_iff {α : Type u_1} (D : Det α) (N vp : α → Prop) : sentence D N vp ↔ D (polarize N vp)

A sentence holds when its determiner holds of the noun's extension polarized by the scope.

Upper bounds, existential entailment and zero

theorem Elliott2025.lessThan_three_matches_judgments : (List.lookup "true in the context" Examples.ex_10.readings = some Judgment.acceptable ↔ sentence (Det.lessThan 3) ⊤ ⊤) ∧ (List.lookup "true in the context" Examples.ex_12.readings = some Judgment.acceptable ↔ sentence (Det.lessThan 3) ⊤ ⊥)

With three boys, less than three boys sneezed is false if they all sneezed and true if none did, as judged.

theorem Elliott2025.classical_lessThan_three_misses_judgments : ¬(List.lookup "true in the context" Examples.ex_10.readings = some Judgment.acceptable ↔ classicalSentence (fun (x : Finset (Fin 3)) => x.card < 3) ⊤ ⊤) ∧ ¬(List.lookup "true in the context" Examples.ex_12.readings = some Judgment.acceptable ↔ classicalSentence (fun (x : Finset (Fin 3)) => x.card < 3) ⊤ ⊥)

The classical entry gets both judgments wrong.

theorem Elliott2025.exactly_zero_eq_none {α : Type u_1} [Finite α] : Det.exactly 0 = Det.none

Zero is none.

theorem Elliott2025.all_eq_delta_top {α : Type u_1} : Det.all = fun (x : PolarGroup α) => x.delta ⊤

All is the ∆-operator of the trivial property.

theorem Elliott2025.none_eq_delta_bot {α : Type u_1} : Det.none = fun (x : PolarGroup α) => x.delta ⊥

None is the ∆-operator of the empty property.

theorem Elliott2025.lessThan_eq_compl {α : Type u_1} (n : ℕ) : Det.lessThan n = (Det.atLeast n)ᶜ

Less than n is the negation of at least n.

Predicates and generalized quantifiers

theorem Elliott2025.toGQ_ofGQ {α : Type u_1} (Q : Quantifier.GQ α) (R S : α → Prop) : (Det.ofGQ Q).toGQ R S ↔ Q R fun (x : α) => R x ∧ S x

Mapped to a predicate and back, a generalized quantifier is evaluated at the restrictor and the part of the scope inside it.

theorem Elliott2025.toGQ_ofGQ_eq_iff {α : Type u_1} (Q : Quantifier.GQ α) : (Det.ofGQ Q).toGQ = Q ↔ Q.Conservative

The round trip is the identity exactly on the conservative quantifiers.

theorem Elliott2025.toGQ_ofGQ_of_conservative {α : Type u_1} {Q : Quantifier.GQ α} (hQ : Q.Conservative) : (Det.ofGQ Q).toGQ = Q

theorem Elliott2025.sentence_ofGQ {α : Type u_1} {Q : Quantifier.GQ α} (hQ : Q.Conservative) (R S : α → Prop) : sentence (Det.ofGQ Q) R S ↔ Q R S

theorem Elliott2025.conservative_toGQ {α : Type u_1} (D : Det α) : D.toGQ.Conservative

Every predicate yields a conservative quantifier, so conservativity is a consequence of the theory rather than a constraint on it.

theorem Elliott2025.ofGQ_toGQ {α : Type u_1} (D : Det α) : Det.ofGQ D.toGQ = D

Mapped to a quantifier and back, a predicate is unchanged.

theorem Elliott2025.toGQ_compl {α : Type u_1} (D : Det α) : Dᶜ.toGQ = D.toGQᶜ

noncomputable def Elliott2025.consGQOrderIso {α : Type u_1} : ↥(Quantifier.GQ.ConsGQ α) ≃o Det α

The predicates are order isomorphic to the conservative quantifiers.

Equations

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

theorem Elliott2025.ofGQ_atom {α : Type u_1} {p q : α → Prop} (h : q ≤ p) : Det.ofGQ (KeenanStavi1986.atom p q) = Quantifier.NP.ident (polarize p q)

The isomorphism sends Keenan and Stavi's atom at a restrictor p and a scope q inside it to the predicate of the single group polarize p q.

noncomputable def Elliott2025.hartig {α : Type u_1} : Quantifier.GQ α

The Härtig quantifier says that restrictor and scope have equally many members.

Equations

• Elliott2025.hartig A B = ({x : α | A x}.ncard = {x : α | B x}.ncard)

theorem Elliott2025.not_conservative_hartig {α : Type u_1} [Finite α] [Nontrivial α] : ¬hartig.Conservative

The Härtig quantifier is not conservative.

theorem Elliott2025.toGQ_ofGQ_hartig {α : Type u_1} [Finite α] : (Det.ofGQ hartig).toGQ = Quantifier.GQ.every

Mapped to a predicate and back, the Härtig quantifier becomes the universal.

The determiners as quantifiers

theorem Elliott2025.all_eq_ofGQ {α : Type u_1} : Det.all = Det.ofGQ Quantifier.GQ.every

theorem Elliott2025.some_eq_ofGQ {α : Type u_1} : Det.some = Det.ofGQ Quantifier.GQ.some

theorem Elliott2025.none_eq_ofGQ {α : Type u_1} : Det.none = Det.ofGQ Quantifier.GQ.no

theorem Elliott2025.notAll_eq_ofGQ {α : Type u_1} : Det.notAll = Det.ofGQ Quantifier.GQ.everyᶜ

theorem Elliott2025.atLeast_eq_ofGQ {α : Type u_1} (n : ℕ) : Det.atLeast n = Det.ofGQ (Quantifier.GQ.atLeast n)

theorem Elliott2025.exactly_eq_ofGQ {α : Type u_1} (n : ℕ) : Det.exactly n = Det.ofGQ (Quantifier.GQ.exactly n)

theorem Elliott2025.most_eq_ofGQ {α : Type u_1} : Det.most = Det.ofGQ Quantifier.GQ.most

theorem Elliott2025.toGQ_atLeast {α : Type u_1} (n : ℕ) : (Det.atLeast n).toGQ = Quantifier.GQ.atLeast n

Two boys sneezed says that at least two boys sneezed.

theorem Elliott2025.toGQ_exactly {α : Type u_1} (n : ℕ) : (Det.exactly n).toGQ = Quantifier.GQ.exactly n

Exactly two boys sneezed says that exactly two boys sneezed.

theorem Elliott2025.toGQ_lessThan {α : Type u_1} (n : ℕ) : (Det.lessThan n).toGQ = (Quantifier.GQ.atLeast n)ᶜ

Less than three boys sneezed says that fewer than three boys sneezed, with no upper-bound or existential-entailment problem.

theorem Elliott2025.toGQ_most {α : Type u_1} : Det.most.toGQ = Quantifier.GQ.most

Most boys sneezed has the truth conditions of the relational most.

theorem Elliott2025.toGQ_all {α : Type u_1} : Det.all.toGQ = Quantifier.GQ.every

All boys sneezed has universal truth conditions.

theorem Elliott2025.toGQ_some {α : Type u_1} : Det.some.toGQ = Quantifier.GQ.some

theorem Elliott2025.toGQ_none {α : Type u_1} : Det.none.toGQ = Quantifier.GQ.no

Counting the predicates

theorem Elliott2025.card_polarGroup {α : Type u_1} [Fintype α] : Nat.card (PolarGroup α) = 3 ^ Fintype.card α

There are 3 ^ n groups on n individuals, one for each trivalent function.

theorem Elliott2025.card_ne_bot {α : Type u_1} [Fintype α] : Nat.card { X : PolarGroup α // X ≠ ⊥ } = 3 ^ Fintype.card α - 1

There are 3 ^ n - 1 nonempty groups on n individuals.

theorem Elliott2025.card_det {α : Type u_1} [Fintype α] : Nat.card (Det α) = 2 ^ 3 ^ Fintype.card α

There are 2 ^ 3 ^ n predicates of groups on n individuals, as many as Keenan and Stavi's conservative quantifiers.

theorem Elliott2025.card_predicates {α : Type u_1} [Fintype α] : Nat.card ({ X : PolarGroup α // X ≠ ⊥ } → Prop) = 2 ^ (3 ^ Fintype.card α - 1)

Without the empty group there are 2 ^ (3 ^ n - 1) predicates of groups on n individuals.

theorem Elliott2025.card_predicates_lt_card_gq {α : Type u_1} [Fintype α] : Nat.card ({ X : PolarGroup α // X ≠ ⊥ } → Prop) < Nat.card (Quantifier.GQ α)

There are fewer predicates than generalized quantifiers.

theorem Elliott2025.eqOn_ofGQ_iff {α : Type u_1} {Q Q' : Quantifier.GQ α} (hQ : Q.Conservative) (hQ' : Q'.Conservative) : Set.EqOn (Det.ofGQ Q) (Det.ofGQ Q') {⊥}ᶜ ↔ Set.EqOn Q Q' {R : α → Prop | ∃ (x : α), R x}

Two conservative quantifiers give predicates that agree on the nonempty groups exactly when they agree on the nonempty restrictors.

Existential and distributive scope

theorem Elliott2025.all_inf_noun {α : Type u_1} (N : α → Prop) : Det.all ⊓ noun N = Quantifier.NP.ident (polarize N ⊤)

All N holds of a single group, the noun's extension polarized positively throughout.

theorem Elliott2025.none_inf_noun {α : Type u_1} (N : α → Prop) : Det.none ⊓ noun N = Quantifier.NP.ident (polarize N ⊥)

No N holds of a single group, the noun's extension polarized negatively throughout.

theorem Elliott2025.all_scopeless {α : Type u_1} (N : α → Prop) : Quantifier.GQ.some (Det.all ⊓ noun N) = Quantifier.NP.individual (polarize N ⊤)

Existential raising of all N is the Montague individual of the noun's wholly positive group, so it is scopeless and the universal force stays with the ∆-operator.

theorem Elliott2025.none_scopeless {α : Type u_1} (N : α → Prop) : Quantifier.GQ.some (Det.none ⊓ noun N) = Quantifier.NP.individual (polarize N ⊥)

Existential raising of no N is scopeless.

theorem Elliott2025.exactly_two_not_individual : ¬∃ (X₀ : PolarGroup (Fin 3)), Quantifier.GQ.some (Det.exactly 2 ⊓ noun ⊤) = Quantifier.NP.individual X₀

Exactly two of three individuals holds of several groups, so its existential raising is no individual and an exceptional scope reading is predicted.

Collective predicates

theorem Elliott2025.delta_collective_iff {β : Type u_2} [PartialOrder β] {C N : β → Prop} {X : PolarGroup β} (hC : ∀ (x : β), C x → ¬Mereology.Atom x) (hX : noun (fun (x : β) => Mereology.Atom x ∧ N x) X) : X.delta C ↔ X.posAtoms = ∅

On a group of a singular noun, a collective predicate, true of no atom, distributes exactly when the group has no positive atom.

theorem Elliott2025.not_some_singular_collective {β : Type u_2} [PartialOrder β] {C N : β → Prop} (hC : ∀ (x : β), C x → ¬Mereology.Atom x) : ¬sentence Det.some (fun (x : β) => Mereology.Atom x ∧ N x) C

Some boy gathered is false, since a positive atom would have to gather.

Questions

theorem Elliott2025.whichDeRe_eq_ker {E : Type u_2} {W : Type u_3} (G P : E → Set W) (w : W) : GroenendijkStokhof1984.whichDeRe G P w = Setoid.ker fun (v : W) => polarize (fun (x : E) => x ∈ GroenendijkStokhof1984.extension G w) fun (x : E) => x ∈ GroenendijkStokhof1984.extension P v

Two indices give the same answer to which G P?, read de re at w, exactly when they polarize the G-individuals alike, so the answers correspond to the groups of the noun.

theorem Elliott2025.sentence_relevant {E : Type u_2} {W : Type u_3} (G P : E → Set W) (w : W) (D : Det E) : (GroenendijkStokhof1984.whichDeRe G P w).Decides {v : W | sentence D (fun (x : E) => x ∈ GroenendijkStokhof1984.extension G w) fun (x : E) => x ∈ GroenendijkStokhof1984.extension P v}

Every predicative sentence is relevant to the question, being a union of its answers.

theorem Elliott2025.relevant_of_conservative {E : Type u_2} {W : Type u_3} (G P : E → Set W) (w : W) {Q : Quantifier.GQ E} (hQ : Q.Conservative) : (GroenendijkStokhof1984.whichDeRe G P w).Decides {v : W | Q (fun (x : E) => x ∈ GroenendijkStokhof1984.extension G w) fun (x : E) => x ∈ GroenendijkStokhof1984.extension P v}

Every conservative determiner is relevant to the question.