Documentation

Linglib.Phenomena.Plurals.Studies.BarLev2021

Bar-Lev (2021): An Implicature Account of Homogeneity and Non-Maximality #

@cite{bar-lev-2021}

An Implicature Account of Homogeneity and Non-Maximality. Linguistics and Philosophy 44:1045–1097.

Core Contribution #

Bar-Lev derives homogeneity, universality, and non-maximality for plural definites from a single mechanism: exhaustification with subdomain alternatives via the Exh^{IE+II} operator of @cite{bar-lev-fox-2020}.

The key ingredients:

  1. ∃-PL (existential pluralization): The basic meaning of a plural definite like "the kids laughed" is existential: at least one kid laughed. This operator is defined in ExistentialPL.lean.

  2. Subdomain alternatives: Replacing the domain variable D with subsets D' ⊆ D generates alternatives that are NOT closed under conjunction — structurally parallel to free choice disjunction (@cite{fox-2007}).

  3. Exh^{IE+II}: The same exhaustivity operator that derives free choice from ◇(A ∨ B) derives universality from ∃-PL. Since the subdomain alternatives are not closed under ∧, no non-prejacent alternative is innocently excludable, and all are innocently includable.

Structural Parallel with Free Choice #

This file proves that the Exh^{IE+II} derivation for homogeneity is structurally isomorphic to the free choice derivation in InnocentInclusion.lean:

Free ChoiceHomogeneity
FCWorld (5 worlds)HomWorld (4 worlds)
◇(A ∨ B) (prejacent)someLaughed (∃-PL)
{◇(A∨B), ◇A, ◇B, ◇(A∧B)}{someLaughed, kellyL, janeL}
◇A ∧ ◇B ∉ ALTkellyL ∧ janeL ∉ ALT
IE = {◇(A∧B)}IE = ∅
II = {◇A, ◇B}II = {kellyL, janeL}
Free choiceUniversal reading

Asymmetry of Positive and Negative #

A key prediction: the positive and negative cases are not symmetric.

This asymmetry is derived in negative_universal below.

source
inductive Phenomena.Plurals.Studies.BarLev2021.HomWorld :
Type

Possible worlds for a two-atom plurality {Kelly, Jane} and a predicate P (e.g., "laughed").

Instances For
    source
    instance Phenomena.Plurals.Studies.BarLev2021.instDecidableEqHomWorld :
    DecidableEq HomWorld
    Equations
    source
    def Phenomena.Plurals.Studies.BarLev2021.instBEqHomWorld.beq :
    HomWorld → HomWorld → Bool
    Equations
    Instances For
      source
      instance Phenomena.Plurals.Studies.BarLev2021.instBEqHomWorld :
      BEq HomWorld
      Equations
      source
      instance Phenomena.Plurals.Studies.BarLev2021.instReprHomWorld :
      Repr HomWorld
      Equations
      source
      def Phenomena.Plurals.Studies.BarLev2021.instReprHomWorld.repr :
      HomWorld → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Phenomena.Plurals.Studies.BarLev2021.instInhabitedHomWorld.default :
        HomWorld
        Equations
        Instances For
          source
          instance Phenomena.Plurals.Studies.BarLev2021.instInhabitedHomWorld :
          Inhabited HomWorld
          Equations
          source
          def Phenomena.Plurals.Studies.BarLev2021.kellyLaughed :
          Prop' HomWorld

          Kelly laughed (subdomain alternative for D = {Kelly}).

          Equations
          Instances For
            source
            def Phenomena.Plurals.Studies.BarLev2021.janeLaughed :
            Prop' HomWorld

            Jane laughed (subdomain alternative for D = {Jane}).

            Equations
            Instances For
              source
              def Phenomena.Plurals.Studies.BarLev2021.someLaughed :
              Prop' HomWorld

              The prejacent: ∃-PL_{D={Kelly,Jane}} P (the kids) = "some kid laughed." This is the basic existential meaning of "the kids laughed."

              Equations
              Instances For

                Grounding in ExistentialPL.lean #

                The propositions above are instances of the existPL operator from ExistentialPL.lean. We make this connection structural: each proposition is provably equivalent to existPL applied with the appropriate domain variable D.

                source
                inductive Phenomena.Plurals.Studies.BarLev2021.Kid :
                Type

                The two atoms of the plurality "the kids".

                Instances For
                  source
                  instance Phenomena.Plurals.Studies.BarLev2021.instDecidableEqKid :
                  DecidableEq Kid
                  Equations
                  source
                  def Phenomena.Plurals.Studies.BarLev2021.instBEqKid.beq :
                  Kid → Kid → Bool
                  Equations
                  Instances For
                    source
                    instance Phenomena.Plurals.Studies.BarLev2021.instBEqKid :
                    BEq Kid
                    Equations
                    source
                    instance Phenomena.Plurals.Studies.BarLev2021.instReprKid :
                    Repr Kid
                    Equations
                    source
                    def Phenomena.Plurals.Studies.BarLev2021.instReprKid.repr :
                    Kid → ℕ → Std.Format
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Phenomena.Plurals.Studies.BarLev2021.laughed :
                      Kid → HomWorld → Prop

                      The predicate "laughed" as a function of atoms and worlds.

                      Equations
                      Instances For
                        source
                        def Phenomena.Plurals.Studies.BarLev2021.theKids :
                        Finset Kid

                        The plurality "the kids" = {Kelly, Jane}.

                        Equations
                        Instances For
                          source
                          theorem Phenomena.Plurals.Studies.BarLev2021.someLaughed_eq_existPL (w : HomWorld) :
                          someLaughed w ↔ Semantics.Lexical.Plural.ExistentialPL.existPL theKids laughed theKids w

                          Grounding: someLaughed is the ∃-PL operator applied with full domain variable D = theKids.

                          source
                          theorem Phenomena.Plurals.Studies.BarLev2021.kellyLaughed_eq_existPL (w : HomWorld) :
                          kellyLaughed w ↔ Semantics.Lexical.Plural.ExistentialPL.existPL {Kid.kelly} laughed theKids w

                          Grounding: kellyLaughed is ∃-PL with singleton domain D = {Kelly}.

                          source
                          theorem Phenomena.Plurals.Studies.BarLev2021.janeLaughed_eq_existPL (w : HomWorld) :
                          janeLaughed w ↔ Semantics.Lexical.Plural.ExistentialPL.existPL {Kid.jane} laughed theKids w

                          Grounding: janeLaughed is ∃-PL with singleton domain D = {Jane}.

                          source
                          def Phenomena.Plurals.Studies.BarLev2021.homAlt :
                          Set (Prop' HomWorld)

                          The subdomain alternative set.

                          Full domain variable D = {Kelly, Jane}. Subdomain alternatives arise from D' ⊆ D:

                          • D' = {Kelly, Jane}: someLaughed (= prejacent)
                          • D' = {Kelly}: kellyLaughed
                          • D' = {Jane}: janeLaughed
                          • D' = ∅: trivially true (excluded as non-informative)

                          Crucially, the conjunction kellyLaughed ∧ janeLaughed is NOT in this set — the alternatives are not closed under ∧.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def Phenomena.Plurals.Studies.BarLev2021.homPrejacent :
                            Prop' HomWorld

                            The prejacent: ∃-PL with full domain.

                            Equations
                            Instances For
                              source
                              theorem Phenomena.Plurals.Studies.BarLev2021.hom_not_closed :
                              ¬∀ X ⊆ homAlt, ⋀ X ∈ homAlt

                              The subdomain alternatives are NOT closed under conjunction.

                              kellyLaughed ∧ janeLaughed (= "both laughed") is not equivalent to any member of homAlt. This is the structural property that enables the Exh^{IE+II} derivation, parallel to free choice.

                              IE Computation #

                              For φ = someLaughed and ALT = {someLaughed, kellyLaughed, janeLaughed}:

                              There are two MC-sets (maximal sets of negated alternatives consistent with the prejacent):

                              The IE set is {a ∈ ALT : ∼a ∈ every MC-set}. The intersection MC₁ ∩ MC₂ = {φ}, and since ∼φ is never in an MC-set (contradicts the prejacent), no alternative is innocently excludable.

                              More precisely: ∼kellyLaughed ∉ MC₁ and ∼janeLaughed ∉ MC₂, so neither individual alternative is in IE. And someLaughed = φ cannot be IE-excluded by definition.

                              This contrasts with free choice, where ◇(A ∧ B) IS IE-excludable. The difference: homAlt has only 3 elements (no conjunction member), while fcALT has 4 (including ◇(A ∧ B)).

                              source
                              theorem Phenomena.Plurals.Studies.BarLev2021.nothing_ie (q : Prop' HomWorld) (hqIE : Exhaustification.isInnocentlyExcludable homAlt homPrejacent q) :
                              False

                              Nothing is innocently excludable in the homogeneity configuration.

                              This is the key difference from free choice, where ◇(A ∧ B) IS IE-excludable. Here, the alternatives lack a conjunction member entirely, so neither individual alternative can be consistently excluded from all MC-sets.

                              II Computation #

                              Since IE = ∅ (nothing is excludable), the II constraint set is just {someLaughed} (the prejacent, with no IE negations).

                              All members of homAlt hold at .both, so adding any target to an II-compatible set R preserves II-compatibility (witness: .both).

                              Result: II = {kellyLaughed, janeLaughed} (and someLaughed, but the prejacent is already asserted).

                              source
                              theorem Phenomena.Plurals.Studies.BarLev2021.kellyLaughed_ii :
                              Exhaustification.isInnocentlyIncludable homAlt homPrejacent kellyLaughed

                              kellyLaughed is innocently includable.

                              source
                              theorem Phenomena.Plurals.Studies.BarLev2021.janeLaughed_ii :
                              Exhaustification.isInnocentlyIncludable homAlt homPrejacent janeLaughed

                              janeLaughed is innocently includable.

                              source
                              theorem Phenomena.Plurals.Studies.BarLev2021.universality (w : HomWorld) :
                              Exhaustification.exhIEII homAlt homPrejacent w → kellyLaughed w ∧ janeLaughed w

                              Universality from Exh^{IE+II}: exhaustified "the kids laughed" entails that both Kelly and Jane laughed.

                              Exh^{IE+II}(∃-PL_C(laughed)(the kids)) ⊢ ∀ x ∈ {K,J}. laughed(x)

                              This is the homogeneity derivation: the universal reading of a plural definite arises as an implicature, not from basic semantics.

                              Compare free_choice in InnocentInclusion.lean.

                              source
                              theorem Phenomena.Plurals.Studies.BarLev2021.negative_universal (w : HomWorld) :
                              ¬someLaughed w → ¬kellyLaughed w ∧ ¬janeLaughed w

                              Negative asymmetry: Under negation, the universal reading comes for free from the basic (existential) semantics: ¬∃x. laughed(x) ⊢ ∀x. ¬laughed(x).

                              No exhaustification needed — this is just the classical equivalence ¬∃ = ∀¬. This asymmetry between positive and negative is a key prediction that distinguishes the implicature account from trivalent theories (where both polarities are symmetric).

                              source
                              theorem Phenomena.Plurals.Studies.BarLev2021.gap_both_false (w : HomWorld) :
                              someLaughed w → ¬(kellyLaughed w ∧ janeLaughed w) → ¬Exhaustification.exhIEII homAlt homPrejacent w ∧ ¬¬someLaughed w

                              In a gap scenario (some but not all laughed), the positive sentence is false (universality fails) and the negative sentence is false (existence holds). This non-complementarity IS the homogeneity gap.

                              source
                              theorem Phenomena.Plurals.Studies.BarLev2021.onlyKelly_is_gap :
                              someLaughed HomWorld.onlyKelly ∧ ¬(kellyLaughed HomWorld.onlyKelly ∧ janeLaughed HomWorld.onlyKelly)

                              Witness: onlyKelly is a gap scenario.

                              source
                              theorem Phenomena.Plurals.Studies.BarLev2021.onlyJane_is_gap :
                              someLaughed HomWorld.onlyJane ∧ ¬(kellyLaughed HomWorld.onlyJane ∧ janeLaughed HomWorld.onlyJane)

                              Witness: onlyJane is a gap scenario.

                              Non-Maximality via Pruning #

                              @cite{bar-lev-2021} §5 derives non-maximal readings via pruning: when context makes certain subdomain alternatives irrelevant, they are removed from ALT before exhaustification. With fewer alternatives, Exh^{IE+II} produces a weaker (non-maximal) reading.

                              The pruning spectrum for a 2-atom plurality {Kelly, Jane}:

                              ALTResult
                              {φ, kellyL, janeL} (full)Universal (both laughed)
                              {φ, janeL} (kelly pruned)janeL excluded by IE
                              {φ, kellyL} (jane pruned)kellyL excluded by IE
                              {φ} (fully pruned)Existential (some kid laughed)

                              Note: with only 2 atoms, partial pruning yields exclusive readings (IE excludes the remaining alternative), not intermediate non-maximal readings. True non-maximality (e.g., "7 of 10 kids laughed" counting as "the kids laughed") requires ≥3 atoms, where pruning some but not all individual alternatives weakens the II result to something between existential and universal.

                              In the fire hazard context (NonMaximality.lean), the distinction between "all kids laughed" and "some kids laughed" is irrelevant, so ALL individual alternatives are pruned. Exh is then vacuous and the existential basic meaning surfaces directly.

                              source
                              def Phenomena.Plurals.Studies.BarLev2021.prunedAlt :
                              Set (Prop' HomWorld)

                              Fully pruned alternative set: only the prejacent remains.

                              Equations
                              Instances For
                                source
                                theorem Phenomena.Plurals.Studies.BarLev2021.pruned_existential (w : HomWorld) :
                                Exhaustification.exhIEII prunedAlt homPrejacent w → someLaughed w

                                With a fully pruned alternative set, Exh^{IE+II} reduces to the basic existential meaning (no strengthening occurs).

                                source
                                theorem Phenomena.Plurals.Studies.BarLev2021.existential_suffices_pruned (w : HomWorld) :
                                someLaughed w → Exhaustification.exhIEII prunedAlt homPrejacent w

                                The converse: the basic meaning suffices for Exh with pruned alternatives.

                                source
                                theorem Phenomena.Plurals.Studies.BarLev2021.pruning_weakens :
                                (∀ (w : HomWorld), Exhaustification.exhIEII homAlt homPrejacent w → someLaughed w) ∧ ¬∀ (w : HomWorld), someLaughed w → Exhaustification.exhIEII homAlt homPrejacent w

                                Pruning strictly weakens the reading: the universal reading (full ALT) entails the existential reading (pruned ALT), but not vice versa.

                                source
                                def Phenomena.Plurals.Studies.BarLev2021.partialPrunedAlt :
                                Set (Prop' HomWorld)

                                Partially pruned alternative set: kellyLaughed removed, janeLaughed retained.

                                With this ALT = {φ, janeLaughed}, there is a single MC-set {φ, ∼janeLaughed} (witness: onlyKelly). So janeLaughed ∈ IE, and Exh^{IE}(φ) = someLaughed ∧ ¬janeLaughed. The 2-atom case yields exclusive readings under partial pruning, not weakened universals. True non-maximal readings require ≥3 atoms.

                                Equations
                                Instances For
                                  source
                                  theorem Phenomena.Plurals.Studies.BarLev2021.partial_pruning_not_universal :
                                  ¬∀ (w : HomWorld), Exhaustification.exhIEII partialPrunedAlt homPrejacent w → kellyLaughed w ∧ janeLaughed w

                                  Partial pruning (removing kellyLaughed) does not yield universality.

                                  Counterexample: .onlyKelly satisfies Exh^{IE+II} (janeLaughed is IE-excluded and someLaughed is II-included) but not the universal kellyLaughed ∧ janeLaughed.

                                  source
                                  theorem Phenomena.Plurals.Studies.BarLev2021.matches_switches_data :
                                  Homogeneity.switchesExample.positiveInAll = Homogeneity.HomogeneityJudgment.clearlyTrue ∧ Homogeneity.switchesExample.negativeInAll = Homogeneity.HomogeneityJudgment.clearlyFalse ∧ Homogeneity.switchesExample.positiveInNone = Homogeneity.HomogeneityJudgment.clearlyFalse ∧ Homogeneity.switchesExample.negativeInNone = Homogeneity.HomogeneityJudgment.clearlyTrue ∧ Homogeneity.switchesExample.positiveInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Homogeneity.switchesExample.negativeInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

                                  Bar-Lev's theory predicts the full truth-value pattern for the switches example: universal in ALL, denial in NONE, gap in between. This matches the empirical judgments in Homogeneity.lean.

                                  source
                                  theorem Phenomena.Plurals.Studies.BarLev2021.is_implicature_account :
                                  Multiplicity.implicaturePrediction.childrenComputeFewer = true ∧ Multiplicity.implicaturePrediction.multiplicityCorrelatesWithSI = true ∧ Multiplicity.implicaturePrediction.accountsForPolarityAsymmetry = true

                                  Bar-Lev's theory is an implicature account: multiplicity inferences arise via the same mechanism as scalar implicatures, predicting uniform monotonicity sensitivity.

                                  Comparison with @cite{magri-2014} #

                                  Both Magri and Bar-Lev derive universality from exhaustification of an existential basic meaning. The key differences:

                                  1. Magri: Uses double exhaustification (EXH(EXH(THE))) with non-transitive Horn-mateness to block THE from excluding ALL directly.

                                  2. Bar-Lev: Uses single Exh^{IE+II} with subdomain alternatives. The key insight is that subdomain alternatives are not closed under ∧, which is what triggers II (Innocent Inclusion).

                                  Bar-Lev's approach is more economical (one application of Exh, not two) and unifies homogeneity with free choice through a shared structural property (non-closure under ∧).

                                  source
                                  theorem Phenomena.Plurals.Studies.BarLev2021.magri_agreement :
                                  Magri2014.primalMeaning Magri2014.Role.mystery = Magri2014.someMeaning ∧ Magri2014.effectiveInterpretation Magri2014.TheoryVariant.primal Core.Polarity.positive = Magri2014.Role.strong

                                  Both theories agree that the basic meaning is existential and the strengthened meaning is universal. The key structural difference: Magri requires two applications of EXH (double exhaustification via non-transitive Horn-mateness), while Bar-Lev requires one application of Exh^{IE+II} (the richer operator compensates for fewer iterations). Bar-Lev's approach also unifies homogeneity with free choice through the shared structural property of non-closure under ∧.

                                  How "All" Removes Homogeneity #

                                  @cite{bar-lev-2021} §8.3: "all the kids laughed" does not display homogeneity because all universally quantifies over the plurality, eliminating the domain variable D. Without D, there are no subdomain alternatives, so Exh^{IE+II} is vacuous — the universal reading is the basic meaning, not an implicature. Since it's not an implicature, it can't be weakened by pruning, which is why "all" blocks non-maximality.

                                  This connects to Homogeneity.lean's HomogeneityRemover.all and to @cite{kriz-2016}'s removeGap (which collapses the truth-value gap into the negative extension — a different mechanism but the same empirical prediction).

                                  source
                                  theorem Phenomena.Plurals.Studies.BarLev2021.all_removes_homogeneity_prediction :
                                  Homogeneity.allRemovesHomogeneity.remover = Homogeneity.HomogeneityRemover.all ∧ Homogeneity.allRemovesHomogeneity.homogeneousJudgment = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Homogeneity.allRemovesHomogeneity.preciseJudgment = Homogeneity.HomogeneityJudgment.clearlyFalse

                                  Bar-Lev's theory predicts that "all" removes homogeneity: the allRemovesHomogeneity datum records that the gap scenario yields .clearlyFalse for "all the doors are open" (vs .neitherTrueNorFalse for the bare plural). This aligns with Bar-Lev's mechanism: "all" eliminates subdomain alternatives, making the universal reading semantic (not an implicature) and therefore non-cancelable.

                                  source
                                  theorem Phenomena.Plurals.Studies.BarLev2021.all_exh_vacuous (w : HomWorld) :
                                  Exhaustification.exhIEII {homPrejacent} homPrejacent w ↔ someLaughed w

                                  Without subdomain alternatives, exhaustification is vacuous: the prejacent passes through unchanged. This models the effect of all, which eliminates the domain variable D.

                                  Comparison with @cite{kriz-2016} (Trivalent Account) #

                                  @cite{kriz-2016} and @cite{kriz-spector-2021} derive homogeneity from trivalent semantics: plural predication yields a three-valued denotation (true/false/gap), and non-maximality arises when the gap is pragmatically exploitable. The two accounts differ in:

                                  PropertyBar-Lev (implicature)Križ (trivalent)
                                  Basic meaningexistential (∃-PL)trivalent (T/F/gap)
                                  Universal readingimplicature (Exh^{IE+II})semantic (true extension)
                                  Non-maximalitypruning alternativespragmatic gap exploitation
                                  Positive/negativeasymmetricsymmetric
                                  "All" removes gapeliminates C variablecollapses gap (removeGap)

                                  Key Distinguishing Prediction: Asymmetry #

                                  The most important empirical difference concerns the status of the universal inference under negation:

                                  This asymmetry is captured by negative_universal above: under negation, the universal reading follows from basic semantics without exhaustification. Križ's trivalent account would instead derive both through the gap mechanism symmetrically.

                                  source
                                  theorem Phenomena.Plurals.Studies.BarLev2021.positive_negative_asymmetry :
                                  (∃ (w : HomWorld), someLaughed w ∧ ¬(kellyLaughed w ∧ janeLaughed w)) ∧ ∀ (w : HomWorld), ¬someLaughed w → ¬kellyLaughed w ∧ ¬janeLaughed w

                                  The positive–negative asymmetry: positive universality requires exhaustification, while negative universality does not.

                                  This is a distinguishing prediction of the implicature account: universality needs the full Exh^{IE+II} machinery, but negative_universal is a simple logical entailment. In the trivalent account (@cite{kriz-2016}), both arise from the gap structure.