Champollion 2016: Noun Coordination and the Intersective Theory of Conjunction

[Cha16b]

Champollion argues that and has ONE lexical entry: the intersective (Boolean meet) generalized conjunction INT ([Cha16b] eq. 16/17 — this IS linglib's [PR83] genConj = Coordinator.op .j = ⊓). Collective readings (John and Mary met, ten men and women got married) are NOT a join on individuals folded into and; they are derived by silent type-shifters (Existential/ Choice Raising, Intersection, Minimization). Two results, both routing through the Coordinator.op API:

• The type-shift ⊔ ↦ ⊓ is guarded, not free. Partee's lift typeRaise : e → GQ (x ↦ λP. P x) relates the individual-join x ⊔ y to the GQ-meet Coordinator.op .j (= ⊓) of the raised individuals exactly on the predicates that distribute the join (typeRaise_join_eq_op_iff). It is NOT a clean anti-homomorphism: for a collective predicate (met/gather) the two diverge (typeRaise_join_ne_op_collective) — which is why Champollion needs Raising + Minimization rather than reducing collectivity to raising + intersection. The guard is grounded in Link distributivity: Link's ᴰ-closed predicates satisfy it under join-prime atoms (linkD_distributiveOverJoin).

• The collective theory overgenerates. The rival entry of [HZ05] — the "set product" of [Cha16b] eq. 101, which builds and from set union on individuals — wrongly predicts No man and no woman smiled TRUE in the model where a man (John) and a woman (Mary) smiled and no-one else did (§7.1, journal p. 608), where the intersective Coordinator.op .j correctly predicts FALSE (setProduct_overgenerates). This divergence is the payoff: it refutes join-on-individuals as the meaning of and.

Main results

• typeRaise_join_eq_op_iff — the type-shift ⊔ ↦ ⊓ holds at P iff P distributes the join.
• typeRaise_join_eq_op_of_distributive, linkD_distributiveOverJoin — the guard is Link distributivity.
• collective_not_distributiveOverJoin, typeRaise_join_ne_op_of_not_distributive — a collective predicate breaks the type-shift.
• setProduct_overgenerates — H&Z's set-product and gets No man and no woman smiled wrong; op .j gets it right.

The type-shift ⊔ ↦ ⊓ is guarded to distributive predicates

The intersective entry says and is INT ([Cha16b] eq. 16): generalized conjunction genConj, which is Coordinator.op .j = the Boolean meet ⊓. On two type-raised individuals it returns λP. P x ∧ P y. The collective behaviour people attribute to and (a join x ⊔ y on individuals) coincides with this meet only for predicates that distribute the join — for genuinely collective predicates the two come apart, which is the whole motivation for Champollion's silent operators.

def Champollion2016.DistributiveOverJoin {E : Type u_1} [SemilatticeSup E] (P : E → Prop) : Prop

A predicate distributes a join when it decomposes x ⊔ y into a meet: P (x ⊔ y) ↔ P x ∧ P y. Link's ᴰ-closed (distributive) predicates satisfy this; collective predicates (met, gather) do not.

Equations

• Champollion2016.DistributiveOverJoin P = ∀ (x y : E), P (x ⊔ y) ↔ P x ∧ P y

theorem Champollion2016.typeRaise_join_apply {E W : Type} [SemilatticeSup E] (x y : E) (P : E → Prop) : Intensional.Conjunction.typeRaise (x ⊔ y) P = P (x ⊔ y)

typeRaise (x ⊔ y) applied to P is P (x ⊔ y) (Montague's lift).

theorem Champollion2016.coordEntities_eq_opj {E W : Type} (x y : E) : Intensional.Conjunction.coordEntities x y = Coordinator.op Coordinator.Role.j (Intensional.Conjunction.typeRaise x) (Intensional.Conjunction.typeRaise y)

coordEntities (the intersective and of two raised individuals) IS the GQ-meet Coordinator.op .j — [Cha16b]'s INT (eq. 16) as the Boolean ⊓ at the GQ type (flow-through bucket (a): genConj is op).

theorem Champollion2016.op_typeRaise_apply {E W : Type} (x y : E) (P : E → Prop) : Coordinator.op Coordinator.Role.j (Intensional.Conjunction.typeRaise x) (Intensional.Conjunction.typeRaise y) P = (P x ∧ P y)

The intersective and of two raised individuals applied to P is P x ∧ P y. The two-atom case of Link distributive predication: it equals distMaximal P {x, y} (see [BGD+25] mu_is_distributive_check).

theorem Champollion2016.typeRaise_join_eq_op_iff {E W : Type} [SemilatticeSup E] (x y : E) (P : E → Prop) : (Intensional.Conjunction.typeRaise (x ⊔ y) P ↔ Coordinator.op Coordinator.Role.j (Intensional.Conjunction.typeRaise x) (Intensional.Conjunction.typeRaise y) P) ↔ (P (x ⊔ y) ↔ P x ∧ P y)

The type-shift ⊔ ↦ ⊓, guarded. Type-raising the individual-join x ⊔ y agrees with the GQ-meet Coordinator.op .j of the raised individuals at P iff P distributes this join. The bare anti-homomorphism (for all P) is therefore FALSE; distributivity is exactly the guard.

theorem Champollion2016.typeRaise_join_eq_op_of_distributive {E W : Type} [SemilatticeSup E] (x y : E) {P : E → Prop} (hP : DistributiveOverJoin P) : Intensional.Conjunction.typeRaise (x ⊔ y) P ↔ Coordinator.op Coordinator.Role.j (Intensional.Conjunction.typeRaise x) (Intensional.Conjunction.typeRaise y) P

For a distributive predicate the type-shift holds: typeRaise (x ⊔ y) agrees with the GQ-meet on P.

theorem Champollion2016.linkD_distributiveOverJoin {E : Type u_1} [SemilatticeSup E] (hJP : Semantics.Plurality.Algebra.AtomJoinPrime E) (Q : E → Prop) : DistributiveOverJoin (Semantics.Plurality.Algebra.D Q)

The guard is Link distributivity. A Link ᴰ-closed predicate ᴰQ ([Lin87b]) distributes every join, given join-prime atoms ([Lin83]). So Champollion's distributive and IS Link's distributive predication, and the predicates that break the type-shift are precisely the non-ᴰ-closed (collective) ones.

theorem Champollion2016.typeRaise_join_eq_op_of_linkD {E W : Type} [SemilatticeSup E] (hJP : Semantics.Plurality.Algebra.AtomJoinPrime E) (x y : E) (Q : E → Prop) : Intensional.Conjunction.typeRaise (x ⊔ y) (Semantics.Plurality.Algebra.D Q) ↔ Coordinator.op Coordinator.Role.j (Intensional.Conjunction.typeRaise x) (Intensional.Conjunction.typeRaise y) (Semantics.Plurality.Algebra.D Q)

A Link ᴰ-closed predicate licenses the type-shift ⊔ ↦ ⊓.

theorem Champollion2016.typeRaise_join_ne_op_of_not_distributive {E W : Type} [SemilatticeSup E] {P : E → Prop} (h : ¬DistributiveOverJoin P) : ∃ (x : E) (y : E), ¬(Intensional.Conjunction.typeRaise (x ⊔ y) P ↔ Coordinator.op Coordinator.Role.j (Intensional.Conjunction.typeRaise x) (Intensional.Conjunction.typeRaise y) P)

The guard is necessary, lifted to the type-shift. A predicate that does NOT distribute the join breaks the ⊔ ↦ ⊓ agreement at the witnessing pair: there typeRaise (x ⊔ y) and the GQ-meet Coordinator.op .j come apart.

theorem Champollion2016.collective_not_distributiveOverJoin : ∃ (P : Finset Bool → Prop), ¬DistributiveOverJoin P

A collective predicate breaks the guard. True of the plural {false, true} (John and Mary met) but of neither part (Finset Bool, ∪ as ⊔): this collective predicate is not DistributiveOverJoin, so by typeRaise_join_ne_op_of_not_distributive it breaks the type-shift ⊔ ↦ ⊓. This is why Champollion derives collectivity via silent Raising + Minimization rather than via raising + intersection.

The collective theory overgenerates (§7.1, journal p. 608)

Champollion's case against the collective theory: take [HZ05]'s entry, which builds and by set product — combining two quantifier denotations Q, Q' by forming the union A ∪ B of a Q-witness and a Q'-witness ([Cha16b] eq. 101):

⟦and_coll⟧ = λQ λQ'. λP. ∃A ∃B [Q(A) ∧ Q'(B) ∧ P = A ∪ B]

We model the conjuncts at the property-of-pluralities level (type ⟨et,t⟩), following Champollion's prose reduction of the eq. (104) generalized-quantifier argument on journal p. 608: ⟦no man⟧/⟦no woman⟧ as the man-free / woman-free witness-set properties. The overgeneration: No man and no woman smiled (103a) comes out TRUE in the model where a smiling man (John) and a smiling woman (Mary) are the only smilers — take A = {Mary} (no man) and B = {John} (no woman), so A ∪ B = {John, Mary} = the smilers — even though a man did smile. The intersective Coordinator.op .j correctly makes it FALSE.

inductive Champollion2016.Person : Type

The two-individual model of [Cha16b] §7.1: persons John and Mary.

• john : Person
• mary : Person

@[implicit_reducible]

instance Champollion2016.instDecidableEqPerson : DecidableEq Person

Equations

• Champollion2016.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Champollion2016.instReprPerson.repr : Person → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Champollion2016.instReprPerson : Repr Person

Equations

• Champollion2016.instReprPerson = { reprPrec := Champollion2016.instReprPerson.repr }

@[reducible, inline]

abbrev Champollion2016.Plur : Type

A plurality / witness set, as the characteristic function of a set of individuals (type ⟨e,t⟩).

Equations

• Champollion2016.Plur = (Champollion2016.Person → Prop)

def Champollion2016.man : Person → Prop

man holds of John only.

Equations

• Champollion2016.man Champollion2016.Person.john = True
• Champollion2016.man Champollion2016.Person.mary = False

def Champollion2016.woman : Person → Prop

woman holds of Mary only.

Equations

• Champollion2016.woman Champollion2016.Person.john = False
• Champollion2016.woman Champollion2016.Person.mary = True

def Champollion2016.smiled : Plur

In the model, both John and Mary smiled — and they are the only people.

Equations

• Champollion2016.smiled x✝ = True

def Champollion2016.noMan : Plur → Prop

⟦no man⟧ as a property of pluralities: the set contains no man.

Equations

• Champollion2016.noMan X = ∀ (a : Champollion2016.Person), X a → ¬Champollion2016.man a

def Champollion2016.noWoman : Plur → Prop

⟦no woman⟧ as a property of pluralities: the set contains no woman.

Equations

• Champollion2016.noWoman X = ∀ (a : Champollion2016.Person), X a → ¬Champollion2016.woman a

def Champollion2016.andIntersective : (Plur → Prop) → (Plur → Prop) → Plur → Prop

Champollion's intersective and on quantifier denotations is Coordinator.op .j (the Boolean meet ⊓ on the Plur → Prop carrier) — [Cha16b] eq. 16.

Equations

• Champollion2016.andIntersective = Coordinator.op Coordinator.Role.j

def Champollion2016.andSetProduct (Q Q' : Plur → Prop) : Plur → Prop

Heycock & Zamparelli's set-product (collective) and ([HZ05]; [Cha16b] eq. 101): holds of a plurality P iff P is the union A ∪ B of a Q-witness A and a Q'-witness B.

Equations

• Champollion2016.andSetProduct Q Q' P = ∃ (A : Champollion2016.Plur) (B : Champollion2016.Plur), Q A ∧ Q' B ∧ P = fun (a : Champollion2016.Person) => A a ∨ B a

theorem Champollion2016.andIntersective_apply (Q Q' : Plur → Prop) (P : Plur) : andIntersective Q Q' P ↔ Q P ∧ Q' P

def Champollion2016.onlyMary : Plur

The two witness sets from journal p. 608.

Equations

• Champollion2016.onlyMary Champollion2016.Person.john = False
• Champollion2016.onlyMary Champollion2016.Person.mary = True

def Champollion2016.onlyJohn : Plur

Equations

• Champollion2016.onlyJohn Champollion2016.Person.john = True
• Champollion2016.onlyJohn Champollion2016.Person.mary = False

theorem Champollion2016.intersective_false : ¬andIntersective noMan noWoman smiled

Intersective: correct. The intersective Coordinator.op .j entry predicts No man and no woman smiled FALSE — a man (John) smiled, so no man already fails.

theorem Champollion2016.setProduct_true : andSetProduct noMan noWoman smiled

Set product: wrong. The [HZ05] set-product entry predicts No man and no woman smiled TRUE — witness A = {Mary} (no man), B = {John} (no woman), A ∪ B = the smilers. ([Cha16b] §7.1, journal p. 608.)

theorem Champollion2016.setProduct_overgenerates : andSetProduct noMan noWoman smiled ∧ ¬andIntersective noMan noWoman smiled

The payoff ([Cha16b] §7.1): on No man and no woman smiled in the John-and-Mary-smiled model, the collective set-product entry ([HZ05]) and the intersective Coordinator.op .j entry assign OPPOSITE truth values. The intersective answer (FALSE) is correct; the set-product (join-on-individuals) entry overgenerates (TRUE) — refuting the collective theory of and.