Križ & Spector (2021): Interpreting Plural Predication

@cite{kriz-spector-2021}

Interpreting Plural Predication: Homogeneity and Non-Maximality. Linguistics and Philosophy, 44, 1131-1178.

Core Contribution

Križ & Spector 2021 refine @cite{kriz-2016}'s pragmatic mechanism for non-maximality. Where Križ 2016 used "Addressing an Question" (no QUD cell straddles the true/false boundary), K&S replace this with strong relevance filtering: a candidate interpretation is relevant only if its truth predicate is constant on each cell of the QUD partition.

Bridge Theorems

This file proves the correspondence between the two accounts:

1. bivalent_addressing_iff_stronglyRelevant: For bivalent sentences (those modified by all), Križ 2016's Addressing constraint is equivalent to Križ & Spector 2021's strong relevance of the truth predicate to the QUD.

2. all_addressing_iff_relevant: Specialization to all-sentences: Addressing the QUD ↔ allSatisfy is strongly relevant.

These theorems connect two independently formalized mechanisms:

• Semantics.Homogeneity.addressesIssue (from Križ 2016)
• Semantics.Plurality.Distributivity.isStronglyRelevantProp (from K&S 2021)

showing they agree on the bivalent fragment.

For bivalent sentences, the two pragmatic constraints are equivalent. Križ 2016's Addressing says no QUD cell has both true and false worlds. K&S 2021's strong relevance says the truth predicate is constant on each cell. For bivalent sentences these coincide: if the predicate varies within a cell, one world must be true and the other false (there is no gap).

theorem KrizSpector2021.bivalent_addressing_iff_stronglyRelevant {W : Type u_2} (q : QUD W) (S : Semantics.Homogeneity.SentenceTV W) (hbiv : Semantics.Homogeneity.isBivalent S) : Semantics.Homogeneity.addressesIssue q S ↔ Semantics.Plurality.Distributivity.isStronglyRelevantProp q fun (w : W) => Semantics.Homogeneity.bivalentPred S w = true

For bivalent sentences, Addressing ↔ strong relevance of the truth predicate.

The Addressing condition says no cell has both true and false worlds. Strong relevance says the truth predicate is constant on each cell. For bivalent sentences these are equivalent: if the predicate varies within a cell, one world must be true and the other false (there is no gap to break the dichotomy).

bivalentPred S : W → Bool is wrapped as (· = true) : W → Prop to feed the Prop-typed isStronglyRelevantProp.

For all-sentences, the bridge specializes further: Addressing ↔ allSatisfy is strongly relevant to the QUD. This connects directly to nonMaximality_from_coarse_qud in Distributivity.lean: when the QUD groups an all-true world with a not-all-true world, the all-sentence fails to address the issue, so all cannot be used non-maximally.

theorem KrizSpector2021.all_addressing_iff_relevant {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : QUD W) (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Semantics.Homogeneity.addressesIssue q (Phenomena.Plurals.Studies.Kriz2016.allPluralTV P x) ↔ Semantics.Plurality.Distributivity.isStronglyRelevantProp q (Semantics.Plurality.Distributivity.allSatisfy P x)

For all-sentences, Addressing ↔ allSatisfy is strongly relevant.

This bridges Križ 2016's pragmatic mechanism (Addressing) to K&S 2021's filtering mechanism (strong relevance) for the specific case of universal quantification over pluralities. After the @cite{kriz-2016} §3.1 refactor that derives allPluralTV from removeGap, the bridge becomes a pointwise-equivalence result via bivalentPred_allPluralTV_eq_allSatisfy.

The two independently developed mechanisms for non-maximality — pragmatic (communicatedContent from Križ 2016) and semantic (candidate conjunction from K&S 2021) — are connected by this bridge: communicatedContent is exactly the set of worlds where the conjunction of strongly relevant candidates is usable.

For simple cases (single plural DP, distributive predicate), the candidate conjunction reproduces pluralTruthValue. The pragmatic filtering via strong relevance then determines the communicated content by selecting which candidates matter.

theorem KrizSpector2021.candidateConjunction_matches_plural {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hne : x.Nonempty) : (Semantics.Plurality.Distributivity.pluralTruthValue P x w = Core.Duality.Truth3.true ↔ Semantics.Plurality.Distributivity.trueOnAll (Semantics.Plurality.Distributivity.fullCandidateSet P x) w) ∧ (Semantics.Plurality.Distributivity.pluralTruthValue P x w = Core.Duality.Truth3.false ↔ Semantics.Plurality.Distributivity.falseOnAll (Semantics.Plurality.Distributivity.fullCandidateSet P x) w)

The candidate conjunction matches pluralTruthValue when all candidates are included (before relevance filtering). This is the central correspondence of @cite{kriz-spector-2021} §3: the simple trivalent semantics IS truth-on-all-readings applied to the full candidate set.

This is a restatement of pluralTruthValue_eq_candidateSemantics in terms of the candidate conjunction operator.

The H-parameter framework from Distributivity.lean provides a deeper derivation of the same trivalent semantics. Here we connect the three characterizations:

1. pluralTruthValue (supervaluation over atoms)
2. fullCandidateSet + conjunction (truth on all readings)
3. allViaForallH (∀H quantification)

All three agree: they are three views of the same trivalent denotation.

theorem KrizSpector2021.forallH_triangle {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Semantics.Plurality.Distributivity.allViaForallH P x w ↔ Semantics.Plurality.Distributivity.allSatisfy P x w

The ∀H characterization of all agrees with allSatisfy, which agrees with allPluralTV_eq_removeGap. This closes the triangle: ∀H ↔ allSatisfy ↔ removeGap(barePluralTV).

theorem KrizSpector2021.removeGap_iff_forallH {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hne : x.Nonempty) : Semantics.Homogeneity.removeGap (fun (w : W) => Semantics.Plurality.Distributivity.pluralTruthValue P x w) w = Core.Duality.Truth3.true ↔ Semantics.Plurality.Distributivity.allViaForallH P x w

The full bridge: removeGap on bare plural truth = allViaForallH. This formally connects Križ 2016's mechanism (removeGap) to K&S 2021's deeper derivation (∀H). The semantic contribution of all can be understood either as gap removal or as universal H-quantification — they are provably the same.

@cite{kriz-spector-2021} §2.2.3, §3.1: The enriched candidate set correctly handles plural definites in non-monotonic contexts like "Exactly one student read the books." Unlike the two-candidate approach (Krifka 1996), the full candidate set ensures that the conjunction of candidates captures both "one student read all" AND "the others read none."

We demonstrate this with a concrete model: 2 students, 2 books, 4 worlds.

World	Mary reads	John reads	"Exactly one read the books"
maryAll	a, b	∅	TRUE (intended)
bothAll	a, b	a, b	FALSE
maryAllJohnA	a, b	a	GAP (underdetermined)
noneRead	∅	∅	FALSE

inductive KrizSpector2021.NMStudent : Type

• mary : NMStudent
• john : NMStudent

@[implicit_reducible]

instance KrizSpector2021.instDecidableEqNMStudent : DecidableEq NMStudent

Equations

• KrizSpector2021.instDecidableEqNMStudent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KrizSpector2021.instReprNMStudent.repr : NMStudent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KrizSpector2021.instReprNMStudent : Repr NMStudent

Equations

• KrizSpector2021.instReprNMStudent = { reprPrec := KrizSpector2021.instReprNMStudent.repr }

inductive KrizSpector2021.NMBook : Type

• a : NMBook
• b : NMBook

@[implicit_reducible]

instance KrizSpector2021.instDecidableEqNMBook : DecidableEq NMBook

Equations

• KrizSpector2021.instDecidableEqNMBook x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KrizSpector2021.instReprNMBook : Repr NMBook

Equations

• KrizSpector2021.instReprNMBook = { reprPrec := KrizSpector2021.instReprNMBook.repr }

def KrizSpector2021.instReprNMBook.repr : NMBook → ℕ → Std.Format

Equations

• KrizSpector2021.instReprNMBook.repr KrizSpector2021.NMBook.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KrizSpector2021.NMBook.a")).group prec✝
• KrizSpector2021.instReprNMBook.repr KrizSpector2021.NMBook.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KrizSpector2021.NMBook.b")).group prec✝

inductive KrizSpector2021.NMWorld : Type

• maryAll : NMWorld
• bothAll : NMWorld
• maryAllJohnA : NMWorld
• noneRead : NMWorld

@[implicit_reducible]

instance KrizSpector2021.instDecidableEqNMWorld : DecidableEq NMWorld

Equations

• KrizSpector2021.instDecidableEqNMWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KrizSpector2021.instReprNMWorld.repr : NMWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KrizSpector2021.instReprNMWorld : Repr NMWorld

Equations

• KrizSpector2021.instReprNMWorld = { reprPrec := KrizSpector2021.instReprNMWorld.repr }

@[implicit_reducible]

instance KrizSpector2021.instFintypeNMStudent : Fintype NMStudent

Equations

• KrizSpector2021.instFintypeNMStudent = { elems := {KrizSpector2021.NMStudent.mary, KrizSpector2021.NMStudent.john}, complete := KrizSpector2021.instFintypeNMStudent._proof_1 }

@[implicit_reducible]

instance KrizSpector2021.instFintypeNMBook : Fintype NMBook

Equations

• KrizSpector2021.instFintypeNMBook = { elems := {KrizSpector2021.NMBook.a, KrizSpector2021.NMBook.b}, complete := KrizSpector2021.instFintypeNMBook._proof_1 }

@[implicit_reducible]

instance KrizSpector2021.instFintypeNMWorld : Fintype NMWorld

Equations

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

def KrizSpector2021.nmRead : NMStudent → NMBook → NMWorld → Prop

Did this student read this book in this world?

Equations

• KrizSpector2021.nmRead KrizSpector2021.NMStudent.mary x✝ KrizSpector2021.NMWorld.maryAll = True
• KrizSpector2021.nmRead KrizSpector2021.NMStudent.mary x✝ KrizSpector2021.NMWorld.bothAll = True
• KrizSpector2021.nmRead KrizSpector2021.NMStudent.mary x✝ KrizSpector2021.NMWorld.maryAllJohnA = True
• KrizSpector2021.nmRead KrizSpector2021.NMStudent.mary x✝ KrizSpector2021.NMWorld.noneRead = False
• KrizSpector2021.nmRead KrizSpector2021.NMStudent.john x✝ KrizSpector2021.NMWorld.maryAll = False
• KrizSpector2021.nmRead KrizSpector2021.NMStudent.john x✝ KrizSpector2021.NMWorld.bothAll = True
• KrizSpector2021.nmRead KrizSpector2021.NMStudent.john KrizSpector2021.NMBook.a KrizSpector2021.NMWorld.maryAllJohnA = True
• KrizSpector2021.nmRead KrizSpector2021.NMStudent.john KrizSpector2021.NMBook.b KrizSpector2021.NMWorld.maryAllJohnA = False
• KrizSpector2021.nmRead KrizSpector2021.NMStudent.john x✝ KrizSpector2021.NMWorld.noneRead = False

@[implicit_reducible]

instance KrizSpector2021.nmRead.instDecidable (s : NMStudent) (b : NMBook) (w : NMWorld) : Decidable (nmRead s b w)

Equations

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

def KrizSpector2021.nmBooks : Finset NMBook

Equations

• KrizSpector2021.nmBooks = Finset.univ

theorem KrizSpector2021.john_reads_gap_maryAllJohnA : Semantics.Plurality.Distributivity.pluralTruthValue (nmRead NMStudent.john) nmBooks NMWorld.maryAllJohnA = Core.Duality.Truth3.indet

theorem KrizSpector2021.john_reads_false_maryAll : Semantics.Plurality.Distributivity.pluralTruthValue (nmRead NMStudent.john) nmBooks NMWorld.maryAll = Core.Duality.Truth3.false

theorem KrizSpector2021.mary_reads_true_maryAll : Semantics.Plurality.Distributivity.pluralTruthValue (nmRead NMStudent.mary) nmBooks NMWorld.maryAll = Core.Duality.Truth3.true

theorem KrizSpector2021.singleton_a_is_candidate : Semantics.Plurality.Distributivity.candidateProp (nmRead NMStudent.john) {NMBook.a} ∈ Semantics.Plurality.Distributivity.fullCandidateSet (nmRead NMStudent.john) nmBooks

The singleton candidate {a} for John IS a candidate in the full set.

theorem KrizSpector2021.singleton_a_true_at_gap : Semantics.Plurality.Distributivity.candidateProp (nmRead NMStudent.john) {NMBook.a} NMWorld.maryAllJohnA

That singleton candidate is TRUE at maryAllJohnA (John did read book a).

theorem KrizSpector2021.maximal_candidate_false_at_gap : ¬Semantics.Plurality.Distributivity.candidateProp (nmRead NMStudent.john) nmBooks NMWorld.maryAllJohnA

But the maximal candidate is FALSE (John didn't read all books).

theorem KrizSpector2021.gap_is_candidate_disagreement : Semantics.Plurality.Distributivity.gapOnCandidates (Semantics.Plurality.Distributivity.fullCandidateSet (nmRead NMStudent.john) nmBooks) NMWorld.maryAllJohnA

The gap for John arises from candidate disagreement: some candidates are true (singleton {a}) and some are false (maximal {a,b}). This is precisely the K&S diagnosis of homogeneity as candidate disagreement.

@cite{kriz-spector-2021} §3.3, Appendix: Upward homogeneity arises when a predicate is true of a super-plurality containing x but not of x itself. For example, "The soldiers of my brigade didn't surround the castle" is false if the brigade together with other soldiers surrounded the castle.

The existing generalisedTV in Homogeneity.lean captures this via the overlaps relation. Here we prove the connection: when an overlapping super-plurality satisfies P, the sentence about x is gapped, not false.

theorem KrizSpector2021.upward_homogeneity_gap {Atom : Type u_1} [DecidableEq Atom] (P : Finset Atom → Prop) [DecidablePred P] (domain : Finset (Finset Atom)) (x : Finset Atom) (hPx : ¬P x) (b : Finset Atom) (hb : b ∈ domain) (hov : Semantics.Homogeneity.overlaps x b) (hPb : P b) : Semantics.Homogeneity.generalisedTV P domain x = Core.Duality.Truth3.indet

Upward homogeneity: if P is false of x but true of some overlapping super-plurality in the domain, then the generalised truth value is GAP, not FALSE. The predicate's truth "leaks upward" through overlap.

This captures @cite{kriz-spector-2021} §3.3: "The soldiers of my brigade didn't surround the castle" is undefined (not false) when the brigade participated with other soldiers in surrounding the castle.