Documentation

Linglib.Phenomena.Plurals.Studies.KrizSpector2021

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 Issue" (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:

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

source
theorem Phenomena.Plurals.Studies.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.Lexical.Plural.Distributivity.isStronglyRelevantProp q (Semantics.Homogeneity.bivalentPred S)

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

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.

source
theorem Phenomena.Plurals.Studies.KrizSpector2021.all_addressing_iff_relevant {Atom : Type u_1} {W : Type u_2} (q : QUD W) (P : Atom → W → Bool) (x : Finset Atom) :
Semantics.Homogeneity.addressesIssue q (Kriz2016.allPluralTV P x) ↔ Semantics.Lexical.Plural.Distributivity.isStronglyRelevantProp q (Semantics.Lexical.Plural.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.

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.

source
theorem Phenomena.Plurals.Studies.KrizSpector2021.candidateConjunction_matches_plural {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) (hne : x.Nonempty) :
(Semantics.Lexical.Plural.Distributivity.pluralTruthValue P x w = Core.Duality.Truth3.true ↔ Semantics.Lexical.Plural.Distributivity.trueOnAll (Semantics.Lexical.Plural.Distributivity.fullCandidateSet P x) w) ∧ (Semantics.Lexical.Plural.Distributivity.pluralTruthValue P x w = Core.Duality.Truth3.false ↔ Semantics.Lexical.Plural.Distributivity.falseOnAll (Semantics.Lexical.Plural.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.

source
theorem Phenomena.Plurals.Studies.KrizSpector2021.forallH_triangle {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) :
Semantics.Lexical.Plural.Distributivity.allViaForallH P x w ↔ Semantics.Lexical.Plural.Distributivity.allSatisfy P x w = true

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

@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.

WorldMary readsJohn reads"Exactly one read the books"
maryAlla, b∅TRUE (intended)
bothAlla, ba, bFALSE
maryAllJohnAa, baGAP (underdetermined)
noneRead∅∅FALSE
source
inductive Phenomena.Plurals.Studies.KrizSpector2021.NMStudent :
Type
Instances For
    source
    instance Phenomena.Plurals.Studies.KrizSpector2021.instDecidableEqNMStudent :
    DecidableEq NMStudent
    Equations
    source
    def Phenomena.Plurals.Studies.KrizSpector2021.instReprNMStudent.repr :
    NMStudent → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Phenomena.Plurals.Studies.KrizSpector2021.instReprNMStudent :
      Repr NMStudent
      Equations
      source
      inductive Phenomena.Plurals.Studies.KrizSpector2021.NMBook :
      Type
      Instances For
        source
        instance Phenomena.Plurals.Studies.KrizSpector2021.instDecidableEqNMBook :
        DecidableEq NMBook
        Equations
        source
        def Phenomena.Plurals.Studies.KrizSpector2021.instReprNMBook.repr :
        NMBook → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance Phenomena.Plurals.Studies.KrizSpector2021.instReprNMBook :
          Repr NMBook
          Equations
          source
          inductive Phenomena.Plurals.Studies.KrizSpector2021.NMWorld :
          Type
          Instances For
            source
            instance Phenomena.Plurals.Studies.KrizSpector2021.instDecidableEqNMWorld :
            DecidableEq NMWorld
            Equations
            source
            def Phenomena.Plurals.Studies.KrizSpector2021.instReprNMWorld.repr :
            NMWorld → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance Phenomena.Plurals.Studies.KrizSpector2021.instReprNMWorld :
              Repr NMWorld
              Equations
              source
              instance Phenomena.Plurals.Studies.KrizSpector2021.instFintypeNMStudent :
              Fintype NMStudent
              Equations
              • One or more equations did not get rendered due to their size.
              source
              instance Phenomena.Plurals.Studies.KrizSpector2021.instFintypeNMBook :
              Fintype NMBook
              Equations
              • One or more equations did not get rendered due to their size.
              source
              instance Phenomena.Plurals.Studies.KrizSpector2021.instFintypeNMWorld :
              Fintype NMWorld
              Equations
              • One or more equations did not get rendered due to their size.
              source
              def Phenomena.Plurals.Studies.KrizSpector2021.nmRead :
              NMStudent → NMBook → NMWorld → Bool

              Did this student read this book in this world?

              Equations
              Instances For
                source
                def Phenomena.Plurals.Studies.KrizSpector2021.nmBooks :
                Finset NMBook
                Equations
                Instances For
                  source
                  theorem Phenomena.Plurals.Studies.KrizSpector2021.john_reads_gap_maryAllJohnA :
                  Semantics.Lexical.Plural.Distributivity.pluralTruthValue (nmRead NMStudent.john) nmBooks NMWorld.maryAllJohnA = Core.Duality.Truth3.gap
                  source
                  theorem Phenomena.Plurals.Studies.KrizSpector2021.john_reads_false_maryAll :
                  Semantics.Lexical.Plural.Distributivity.pluralTruthValue (nmRead NMStudent.john) nmBooks NMWorld.maryAll = Core.Duality.Truth3.false
                  source
                  theorem Phenomena.Plurals.Studies.KrizSpector2021.mary_reads_true_maryAll :
                  Semantics.Lexical.Plural.Distributivity.pluralTruthValue (nmRead NMStudent.mary) nmBooks NMWorld.maryAll = Core.Duality.Truth3.true
                  source
                  theorem Phenomena.Plurals.Studies.KrizSpector2021.singleton_a_is_candidate :
                  Semantics.Lexical.Plural.Distributivity.candidateProp (nmRead NMStudent.john) {NMBook.a} ∈ Semantics.Lexical.Plural.Distributivity.fullCandidateSet (nmRead NMStudent.john) nmBooks

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

                  source
                  theorem Phenomena.Plurals.Studies.KrizSpector2021.singleton_a_true_at_gap :
                  Semantics.Lexical.Plural.Distributivity.candidateProp (nmRead NMStudent.john) {NMBook.a} NMWorld.maryAllJohnA = true

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

                  source
                  theorem Phenomena.Plurals.Studies.KrizSpector2021.maximal_candidate_false_at_gap :
                  Semantics.Lexical.Plural.Distributivity.candidateProp (nmRead NMStudent.john) nmBooks NMWorld.maryAllJohnA = false

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

                  source
                  theorem Phenomena.Plurals.Studies.KrizSpector2021.gap_is_candidate_disagreement :
                  Semantics.Lexical.Plural.Distributivity.gapOnCandidates (Semantics.Lexical.Plural.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.

                  source
                  theorem Phenomena.Plurals.Studies.KrizSpector2021.upward_homogeneity_gap {Atom : Type u_1} [DecidableEq Atom] (P : Finset Atom → Bool) (domain : Finset (Finset Atom)) (x : Finset Atom) (hPx : P x = false) (b : Finset Atom) (hb : b ∈ domain) (hov : Semantics.Homogeneity.overlaps x b = true) (hPb : P b = true) :
                  Semantics.Homogeneity.generalisedTV P domain x = Core.Duality.Truth3.gap

                  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.