Champollion 2016: noun coordination and the intersective theory of conjunction

Champollion argues that and has one lexical entry, the intersection of Partee and Rooth, and that its collective uses, as in a man and woman met, come from silent operators of Winter that raise each noun to a quantifier and keep the minimal sets of the conjunction. Pluralities are sets. Existential Raising sends a noun to the upper closure of its singletons, and the upper closure takes the set product ⊻ to intersection and union to union, so the derivation yields the man–woman pairs for and and only singletons for or. Choice functions closed above Minimization repair the case of overlapping nouns and give the mixtures that ten men and women counts. The collective entry of Heycock and Zamparelli is the set product itself, which agrees with intersection on upward-entailing conjuncts and overgenerates on the others.

Main definitions

• existentialRaising, minimization, predicateDistributivity: ER (12), MIN (19), PDIST (27)
• choiceRaising, distributiveChoiceRaising: CR (46) and DCR (78) under a choice function
• determinerFitting: DFIT (92)

Main results

• minimization_and_existentialRaising: Minimization after Existential Raising keeps the singletons of the overlap and the pairs from the differences (p. 580), the man–woman pairs (20) for disjoint nouns
• minimization_and_Ici: Minimization of two principal filters is their join
• exists_mem_minimization_choiceRaising_iff, exists_mem_minimization_distributiveChoiceRaising_iff: Choice Closure above Minimization gives every pair (57) and every mixture (80)
• inter_setOf_ncard_minimization_existentialRaising_predicateDistributivity: no numeral above two counts the Existential Raising of plural nouns (76)
• minimization_or_existentialRaising, determinerFitting_every_and_iff_or: or is never collective, and every cat and dog is every cat or dog (95), (96), (99)
• sups_eq_and, sups_noMan_noWoman, sups_individual_card: the set product (101) is intersection on upper sets and overgenerates in (103) and (105)

Implementation notes

A plurality is a Set E and a property of pluralities a Set (Set E), as in the paper. The determiner a is Quantifier.GQ.some, the Montague lift is Quantifier.NP.individual, and and or are what the English coordinators denote, Coordinator.denote, and Choice Closure quantifies over Reference.ChoiceFunction, whose totality turns the definedness condition N ≠ ∅ of Choice Raising into a hypothesis. The counterexamples to the set product read Heycock and Zamparelli's sets of singletons as the individuals they contain, and (76) applies the numeral at the type of the sets it counts. The paper's (99a) writes MIN(ER(cat)) or MIN(ER(dog)) for the MIN(ER(cat) or ER(dog)) of its prose and (99b), and (83c) swaps the Americans and Russians of (82a) and (83b).

TODO

The scope constraints on Choice Closure (§4.4), determiner doubling for the ten-people reading (§5.1), the split scope of indefinite numerals (84)–(87), and Winter's pair semantics (§7.2) are not formalized.

References

• [Cha16b]
• [PR83]
• [Win01a]
• [HZ05]
• [Ber82]

The operators

def Champollion2016.existentialRaising {α : Type u_1} (N : Set α) : Set (Set α)

Existential Raising (12) sends N to the sets that meet it. At any type it is the indefinite article a (23).

Equations

• Champollion2016.existentialRaising N = {P : Set α | Quantifier.GQ.some N P}

@[simp]

theorem Champollion2016.mem_existentialRaising {α : Type u_1} {N P : Set α} : P ∈ existentialRaising N ↔ ∃ x ∈ N, x ∈ P

def Champollion2016.minimization {E : Type u_2} (Q : Set (Set E)) : Set (Set E)

Minimization (19) keeps the minimal sets of Q.

Equations

• Champollion2016.minimization Q = {P : Set E | Minimal (fun (x : Set E) => x ∈ Q) P}

theorem Champollion2016.mem_minimization_iff {E : Type u_2} {Q : Set (Set E)} {P : Set E} : P ∈ minimization Q ↔ P ∈ Q ∧ ∀ P' ⊂ P, P' ∉ Q

A set survives Minimization iff it is in Q and none of its proper subsets is, the form (19b) of the operator.

def Champollion2016.predicateDistributivity {E : Type u_2} (P' : Set E) : Set (Set E)

Predicate Distributivity (27) sends P' to its nonempty subsets. A plural noun is its singular under this operator (72).

Equations

• Champollion2016.predicateDistributivity P' = {P : Set E | P.Nonempty ∧ P ⊆ P'}

def Champollion2016.choiceRaising {E : Type u_2} (f : Reference.ChoiceFunction E) (N : Set E) : Set (Set E)

Choice Raising (46) is the Montague lift of the member of N that f chooses.

Equations

• Champollion2016.choiceRaising f N = {P : Set E | Quantifier.NP.individual (f N) P}

def Champollion2016.distributiveChoiceRaising {E : Type u_2} (f : Reference.ChoiceFunction (Set E)) (N : Set (Set E)) : Set (Set E)

Distributive Choice Raising (78) holds of the sets that contain every member of the plurality f chooses from N.

Equations

• Champollion2016.distributiveChoiceRaising f N = {P : Set E | Quantifier.GQ.every (f N) P}

def Champollion2016.determinerFitting {E : Type u_2} (D : Quantifier.GQ E) (A B : Set (Set E)) : Prop

Determiner Fitting (92) applies a determiner of individuals to the union of a property of pluralities and to the union of its meet with the scope.

Equations

• Champollion2016.determinerFitting D A B = D (⋃₀ A) (⋃₀ (A ∩ B))

Raising and the Montague lift as upper closures

theorem Champollion2016.existentialRaising_eq_upperClosure {α : Type u_1} (N : Set α) : existentialRaising N = ↑(upperClosure ((fun (x : α) => {x}) '' N))

Existential Raising is the upper closure of the singletons of the noun, the sets that contain some man or other (13).

theorem Champollion2016.existentialRaising_union {α : Type u_1} (N N' : Set α) : existentialRaising (N ∪ N') = existentialRaising N ∪ existentialRaising N'

Existential Raising preserves unions.

theorem Champollion2016.setOf_individual {E : Type u_2} (x : E) : {P : Set E | Quantifier.NP.individual x P} = Set.Ici {x}

The Montague lift of x is the principal filter of {x}.

theorem Champollion2016.choiceRaising_eq_Ici {E : Type u_2} (f : Reference.ChoiceFunction E) (N : Set E) : choiceRaising f N = Set.Ici {f N}

Choice Raising is the principal filter of the singleton of the choice.

theorem Champollion2016.distributiveChoiceRaising_eq_Ici {E : Type u_2} (f : Reference.ChoiceFunction (Set E)) (N : Set (Set E)) : distributiveChoiceRaising f N = Set.Ici (f N)

Distributive Choice Raising is the principal filter of the chosen plurality.

theorem Champollion2016.distributiveChoiceRaising_eq_setOf {E : Type u_2} (f : Reference.ChoiceFunction (Set E)) {N : Set (Set E)} (h : (f N).Nonempty) : distributiveChoiceRaising f N = {P : Set E | f N ∈ predicateDistributivity P}

The alternative definition of Distributive Choice Raising through Predicate Distributivity (79), for a nonempty choice.

Raising, Intersection, Minimization

theorem Champollion2016.image_singleton_sups {E : Type u_2} (N N' : Set E) : (fun (x : E) => {x}) '' N ⊻ (fun (x : E) => {x}) '' N' = {P : Set E | ∃ x ∈ N, ∃ y ∈ N', P = {x, y}}

The pairs drawn from N and N' are the set product of their singletons.

theorem Champollion2016.and_existentialRaising {E : Type u_2} (N N' : Set E) : English.Coordination.and_.denote {existentialRaising N, existentialRaising N'} = ↑(upperClosure {P : Set E | ∃ x ∈ N, ∃ y ∈ N', P = {x, y}})

The conjunction ER(man) and ER(woman) is the upper closure of the pairs of a man and a woman, the sets that contain both (18).

theorem Champollion2016.minimization_and_existentialRaising {E : Type u_2} (N N' : Set E) : minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N'}) = {P : Set E | ∃ x ∈ N ∩ N', P = {x}} ∪ {P : Set E | ∃ x ∈ N \ N', ∃ y ∈ N' \ N, P = {x, y}}

Minimization after Existential Raising. The minimal sets containing an N and an N' are the singletons of their overlap and the pairs of an N that is not an N' with an N' that is not an N (journal p. 580).

theorem Champollion2016.minimization_and_existentialRaising_of_disjoint {E : Type u_2} {N N' : Set E} (h : Disjoint N N') : minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N'}) = {P : Set E | ∃ x ∈ N, ∃ y ∈ N', P = {x, y}}

For disjoint nouns, Raising, Intersection and Minimization give the sets of one man and one woman, the meaning mw-pair of man and woman (10), (20).

theorem Champollion2016.minimization_and_existentialRaising_self {E : Type u_2} (N : Set E) : minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N}) = (fun (x : E) => {x}) '' N

When the nouns coincide, only singletons survive Minimization, so that A doctor and lawyer met would be deviant like #John met (42).

theorem Champollion2016.minimization_and_individual_existentialRaising {E : Type u_2} {N : Set E} {j : E} (hj : j ∈ N) : minimization (English.Coordination.and_.denote {{P : Set E | Quantifier.NP.individual j P}, existentialRaising N}) = {{j}}

When John is a man, the singleton of John is the only minimal set that contains John and a man, so John and some man met (43) would be deviant.

theorem Champollion2016.mem_existentialRaising_minimization_inter_iff {E : Type u_2} {N N' : Set E} (h : Disjoint N N') (R S : Set (Set E)) : S ∈ existentialRaising (minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N'}) ∩ R) ↔ ∃ x ∈ N, ∃ y ∈ N', {x, y} ∈ R ∧ {x, y} ∈ S

The hydra A man and woman who dated met (24) is true iff the couple of some man and some woman both dated and met.

theorem Champollion2016.predicateDistributivity_mem_existentialRaising_minimization_iff {E : Type u_2} {N N' : Set E} (h : Disjoint N N') (S : Set E) : predicateDistributivity S ∈ existentialRaising (minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N'})) ↔ ∃ x ∈ N, ∃ y ∈ N', x ∈ S ∧ y ∈ S

With Predicate Distributivity on the scope, A man and woman had a beer (29) is true iff some man and some woman each had a beer.

Choice Raising

theorem Champollion2016.minimization_and_Ici {E : Type u_2} (a b : Set E) : minimization (English.Coordination.and_.denote {Set.Ici a, Set.Ici b}) = {a ∪ b}

Minimization of the meet of two principal filters keeps only their join. This is how Intersection and Minimization form a collective individual.

theorem Champollion2016.minimization_and_individual {E : Type u_2} (x y : E) : minimization (English.Coordination.and_.denote {{P : Set E | Quantifier.NP.individual x P}, {P : Set E | Quantifier.NP.individual y P}}) = {{x, y}}

Minimization of the conjoined Montague lifts of John and Mary keeps only their pair (40).

theorem Champollion2016.exists_mem_choiceRaising_iff {E : Type u_2} {N P : Set E} (hN : N.Nonempty) : (∃ (f : Reference.ChoiceFunction E), P ∈ choiceRaising f N) ↔ P ∈ existentialRaising N

On a nonempty noun, Choice Closure directly above Choice Raising is Existential Raising (p. 583).

theorem Champollion2016.exists_mem_minimization_individual_choiceRaising_iff {E : Type u_2} {N P : Set E} (hN : N.Nonempty) (j : E) : (∃ (f : Reference.ChoiceFunction E), P ∈ minimization (English.Coordination.and_.denote {{P : Set E | Quantifier.NP.individual j P}, choiceRaising f N})) ↔ ∃ x ∈ N, P = {j, x}

With Choice Closure above Minimization, John and some man (53) holds of the pair of John and any man.

theorem Champollion2016.exists_mem_minimization_choiceRaising_iff {E : Type u_2} {N N' P : Set E} (hN : N.Nonempty) (hN' : N'.Nonempty) : (∃ (f₁ : Reference.ChoiceFunction E) (f₂ : Reference.ChoiceFunction E), P ∈ minimization (English.Coordination.and_.denote {choiceRaising f₁ N, choiceRaising f₂ N'})) ↔ ∃ x ∈ N, ∃ y ∈ N', P = {x, y}

With Choice Closure above Minimization, a doctor and lawyer (57) holds of the pair of any doctor and any lawyer, whether or not they share their professions.

Plurals

theorem Champollion2016.inter_setOf_ncard_minimization_existentialRaising_predicateDistributivity {E : Type u_2} (N N' : Set E) {n : ℕ} (hn : 2 < n) : {Q : Set (Set E) | Q.ncard = n} ∩ minimization (English.Coordination.and_.denote {existentialRaising (predicateDistributivity N), existentialRaising (predicateDistributivity N')}) = ∅

Existential Raising of plural nouns followed by Minimization gives sets of at most two pluralities {M, W}, which no numeral above two counts (75), (76).

theorem Champollion2016.exists_mem_minimization_distributiveChoiceRaising_iff {E : Type u_2} {N N' : Set (Set E)} {P : Set E} (hN : N.Nonempty) (hN' : N'.Nonempty) : (∃ (f₁ : Reference.ChoiceFunction (Set E)) (f₂ : Reference.ChoiceFunction (Set E)), P ∈ minimization (English.Coordination.and_.denote {distributiveChoiceRaising f₁ N, distributiveChoiceRaising f₂ N'})) ↔ P ∈ N ⊻ N'

With Distributive Choice Raising and Choice Closure above Minimization, men and women (80) denotes the mixtures, the unions of a plurality from each noun, which form the set product.

theorem Champollion2016.exists_mem_existentialRaising_minimization_distributiveChoiceRaising_iff {E : Type u_2} {N N' : Set (Set E)} (hN : N.Nonempty) (hN' : N'.Nonempty) (S : Set (Set E)) : (∃ (f₁ : Reference.ChoiceFunction (Set E)) (f₂ : Reference.ChoiceFunction (Set E)), S ∈ existentialRaising (minimization (English.Coordination.and_.denote {distributiveChoiceRaising f₁ N, distributiveChoiceRaising f₂ N'}))) ↔ ∃ M ∈ N, ∃ W ∈ N', M ∪ W ∈ S

With Choice Closure at the sentence, as in Two Americans and three Russians made a team (83), the conjunction of two plural nouns holds of a scope iff the union of a plurality from each noun does.

And and or

theorem Champollion2016.minimization_or_existentialRaising {E : Type u_2} (N N' : Set E) : minimization (English.Coordination.or_.denote {existentialRaising N, existentialRaising N'}) = (fun (x : E) => {x}) '' (N ∪ N')

Minimization after Existential Raising of a disjunction keeps only singletons, so or is never collective (§6.2).

theorem Champollion2016.determinerFitting_some_iff {E : Type u_2} {A B : Set (Set E)} (hB : ∅ ∉ B) : determinerFitting Quantifier.GQ.some A B ↔ Quantifier.GQ.some A B

Determiner Fitting does not change the indefinite article when the scope excludes the empty set (p. 604).

theorem Champollion2016.determinerFitting_no_predicateDistributivity_iff {E : Type u_2} (N : Set E) (S : Set (Set E)) : determinerFitting Quantifier.GQ.no (predicateDistributivity N) S ↔ ¬∃ x ∈ N, ∃ P ∈ S, x ∈ P ∧ P ⊆ N

Determiner Fitting of no to a plural noun, as in No students met (94), says that no student is in a set of students that met.

theorem Champollion2016.determinerFitting_every_minimization_and {E : Type u_2} {N N' : Set E} (h : Disjoint N N') (hN : N.Nonempty) (hN' : N'.Nonempty) (S : Set E) : determinerFitting Quantifier.GQ.every (minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N'})) (predicateDistributivity S) ↔ Quantifier.GQ.every (English.Coordination.or_.denote {N, N'}) S

For disjoint nonempty nouns, Determiner Fitting of every to the collective cat and dog says that every cat and every dog is licensed (95).

theorem Champollion2016.determinerFitting_every_minimization_or {E : Type u_2} (N N' S : Set E) : determinerFitting Quantifier.GQ.every (minimization (English.Coordination.or_.denote {existentialRaising N, existentialRaising N'})) (predicateDistributivity S) ↔ Quantifier.GQ.every (English.Coordination.or_.denote {N, N'}) S

Under its collective structure, every cat or dog is licensed (99) says that every cat and every dog is licensed.

theorem Champollion2016.determinerFitting_every_and_iff_or {E : Type u_2} {N N' : Set E} (h : Disjoint N N') (hN : N.Nonempty) (hN' : N'.Nonempty) (S : Set E) : determinerFitting Quantifier.GQ.every (minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N'})) (predicateDistributivity S) ↔ determinerFitting Quantifier.GQ.every (minimization (English.Coordination.or_.denote {existentialRaising N, existentialRaising N'})) (predicateDistributivity S)

Every cat and dog and every cat or dog agree, which solves the universal half of Bergmann's puzzle (95), (96), (99).

theorem Champollion2016.determinerFitting_some_minimization_and {E : Type u_2} {N N' : Set E} (h : Disjoint N N') (S : Set E) : determinerFitting Quantifier.GQ.some (minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N'})) (predicateDistributivity S) ↔ Quantifier.GQ.some N S ∧ Quantifier.GQ.some N' S

A cat and dog came running in (97) says that a cat and a dog came, where a cat or dog (98) says that one of them did.

theorem Champollion2016.some_or_and_not_determinerFitting_some {E : Type u_2} {N N' S : Set E} (h : Disjoint N N') {x : E} (hx : x ∈ N) (hxS : x ∈ S) (hN'S : Disjoint N' S) : Quantifier.GQ.some (English.Coordination.or_.denote {N, N'}) S ∧ ¬determinerFitting Quantifier.GQ.some (minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N'})) (predicateDistributivity S)

When a cat came and no dog did, a cat or dog came running in (98) is true and a cat and dog came running in (97) is false.

The collective theory

theorem Champollion2016.and_subset_sups {α : Type u_1} [Lattice α] (Q Q' : Set α) : English.Coordination.and_.denote {Q, Q'} ⊆ Q ⊻ Q'

Heycock and Zamparelli's collective entry (101), the set product Q ⊻ Q', holds wherever intersection does.

theorem Champollion2016.sups_eq_and {α : Type u_1} [Lattice α] {Q Q' : Set α} (hQ : IsUpperSet Q) (hQ' : IsUpperSet Q') : Q ⊻ Q' = English.Coordination.and_.denote {Q, Q'}

On upward-entailing conjuncts the collective and the intersective entries agree, so the collective theory goes wrong only on conjuncts that are not upward entailing (p. 608).

theorem Champollion2016.sups_setOf_ncard_eq_one {E : Type u_2} {N N' : Set E} (h : Disjoint N N') : {A : Set E | A.ncard = 1 ∧ A ⊆ N} ⊻ {B : Set E | B.ncard = 1 ∧ B ⊆ N'} = minimization (English.Coordination.and_.denote {existentialRaising N, existentialRaising N'})

Man and woman under the collective entry (102), with nouns as sets of singletons, is the meaning that Raising, Intersection and Minimization derive (20).

theorem Champollion2016.sups_noMan_noWoman {E : Type u_2} {N N' : Set E} (h : Disjoint N N') {x y : E} (hx : x ∈ N) (hy : y ∈ N') : {x, y} ∈ {P : Set E | Quantifier.GQ.no N P} ⊻ {P : Set E | Quantifier.GQ.no N' P} ∧ {x, y} ∉ English.Coordination.and_.denote {{P : Set E | Quantifier.GQ.no N P}, {P : Set E | Quantifier.GQ.no N' P}}

When a man and a woman are the only smilers, the collective entry holds of the smilers in No man and no woman smiled (103a) and the intersective entry does not.

theorem Champollion2016.sups_individual_nobodyElse {E : Type u_2} {x y : E} (hxy : x ≠ y) : {x, y} ∈ {P : Set E | Quantifier.NP.individual y P} ⊻ {P : Set E | Quantifier.GQ.no (fun (x : E) => x ≠ y) P} ∧ {x, y} ∉ English.Coordination.and_.denote {{P : Set E | Quantifier.NP.individual y P}, {P : Set E | Quantifier.GQ.no (fun (x : E) => x ≠ y) P}}

When Mary and someone else smiled, the collective entry still holds of the smilers in Mary and nobody else smiled (103b).

theorem Champollion2016.sups_individual_card {E : Type u_2} {N W : Set E} {j : E} (hj : j ∉ N) (hW : W ⊆ N) (hW4 : W.ncard = 4) {p : ℕ → Prop} (h3 : p 3) (h4 : ¬p 4) : insert j W ∈ {P : Set E | Quantifier.NP.individual j P} ⊻ {P : Set E | p (N ∩ P).ncard} ∧ insert j W ∉ English.Coordination.and_.denote {{P : Set E | Quantifier.NP.individual j P}, {P : Set E | p (N ∩ P).ncard}}

Take a condition on the number of women that three meets and four does not, such as between one and three or an odd number (105). The collective entry holds of John and four women, and the intersective entry does not.