Documentation

Studies.HaslingerEtAl2025

Haslinger, Rosina, Schmitt and Wurm (2025): On the relation between distributivity and maximality #

Haslinger, Rosina, Schmitt and Wurm ask whether every obligatorily distributive operator blocks non-maximal construals of its associate plural, and answer no. German jed- is distributive and exception-intolerant in both its determiner and its distance use, alle and numeral indefinites are exception-intolerant but not distributive, and definite plurals are neither (5); the distance distributor jeweils fills the remaining cell, since some speakers accept it in scenarios whose question under discussion makes an exception irrelevant, where DP-jeder is rejected and distance jeder mostly rejected (§3). Item.class is the classification of (5), which the paper's truth-value judgments in the scenarios of (3) confirm (class_of_rows), and jeweils_answers_Q is their answer.

The semantics of §2 relativizes a predicate to a tolerance relation, (14), which relates a plurality to the parts of it that are similar enough to it (tolerant). Varying the tolerance yields exactly Križ and Spector's readings of the plural predication (exists_isTolerance_iff_mem_readings), which is why footnote 3 can call the difference between the two ways of modelling the parameter irrelevant. all, which quantifies over tolerances, forces the maximal reading (all_maximal), and so does each, (21c), since an atom has no part short of itself (each_maximal). An exception-tolerant distributor has to depend on the tolerance itself, as jeweils does in (25): in the magnets scenario of (23) it is true under the tolerance the explosion question induces (jeweils_accepts_magnets) and false for the speakers whose tolerance is the identity (jeweils_identity_rejects_magnets). The hypothetical determiner jeder* of (27) is (25) applied to the sum of its restrictor, so the framework does not predict the absence of exception-tolerant distributive determiners; the paper relates jeweils's permissiveness to its lacking a determiner use instead (determiner_maximal).

Implementation notes #

The questionnaire's ratings are prose: DP-jeder was overwhelmingly rejected, jeweils judged bimodally, distance jeder mostly rejected, and 15 of 18 participants rated the jeweils member of a minimal pair above its distance-jeder counterpart. The paper's examples and scenarios are the rows of Data/Examples/HaslingerEtAl2025.json; the (3) judgments classify an item as distributive when it is false in the cumulative scenario (3b) and as maximal when it is false in the exception scenario (3c), which for jeweils out of the blue gives the maximal cell, the non-maximal construal needing the questionnaire's contexts. Pluralities are finite sets of individuals, whose empty set is excluded from the parts of a plurality as the paper's domain has no empty individual. The tolerance of the magnets scenario tolerates every part of the boxes, since one box with two magnets already answers the explosion question.

References #

Tolerance relations (§2.2) #

source
structure HaslingerEtAl2025.IsTolerance {α : Type u_1} [PartialOrder α] (r : α → α → Prop) :
Prop

A tolerance relation (14) relates a part z of y to y when z is similar enough to y. It is reflexive and contained in parthood, and whatever lies between a tolerated part and the whole is tolerated too.

  • refl (x : α) : r x x
  • le_of_rel {x y : α} : r x y → x ≤ y
  • rel_of_le_of_le {x y z : α} : r x y → x ≤ z → z ≤ y → r z y
Instances For
    source
    theorem HaslingerEtAl2025.isTolerance_eq {α : Type u_1} [PartialOrder α] :
    IsTolerance fun (x1 x2 : α) => x1 = x2

    The identity relation of (16a), under which no proper part is similar enough.

    source
    theorem HaslingerEtAl2025.isTolerance_le {α : Type u_1} [PartialOrder α] :
    IsTolerance fun (x1 x2 : α) => x1 ≤ x2

    Parthood itself, (16b), under which every part is similar enough.

    source
    def HaslingerEtAl2025.tolerant {α : Type u_1} {W : Type u_2} [PartialOrder α] (r : α → α → Prop) (Q : α → Set W) (y : α) :
    Set W

    A predicate relativized to a tolerance (15a) holds of y where it holds of a non-bottom part of y that is similar enough to y.

    Equations
    Instances For
      source
      theorem HaslingerEtAl2025.tolerant_eq {α : Type u_1} {W : Type u_2} [PartialOrder α] {Q : α → Set W} {y : α} (hy : ¬IsBot y) :
      tolerant (fun (x1 x2 : α) => x1 = x2) Q y = Q y

      Under the identity relation, (16a), the predication is maximal.

      source
      theorem HaslingerEtAl2025.exists_isTolerance_iff_mem_readings {α : Type u_1} {W : Type u_2} [PartialOrder α] {Q : α → Set W} {y : α} {p : Set W} :
      (∃ (r : α → α → Prop), IsTolerance r ∧ p = tolerant r Q y) ↔ p ∈ Homogeneity.readings Q y

      Every tolerance yields one of [KS21b]'s readings and every reading comes from a tolerance, which is why footnote 3 can set the difference aside.

      source
      theorem HaslingerEtAl2025.all_maximal {α : Type u_1} {W : Type u_2} [PartialOrder α] {Q : α → Set W} {y : α} {w : W} (hy : ¬IsBot y) :
      (∀ (r : α → α → Prop), IsTolerance r → w ∈ tolerant r Q y) ↔ w ∈ Q y

      all, which quantifies over tolerances (20), forces the maximal reading.

      each (§2.3) #

      source
      theorem HaslingerEtAl2025.each_maximal {Atom : Type u_1} {W : Type u_2} {r : Finset Atom → Finset Atom → Prop} (hr : IsTolerance r) (Q : Finset Atom → Set W) (x : Finset Atom) :
      {w : W | ∀ a ∈ x, w ∈ tolerant r Q {a}} = {w : W | ∀ a ∈ x, w ∈ Q {a}}

      each (21c) applies its predicate to the atoms of its argument, and an atom has no part short of itself, so each is maximal even over a predicate relativized to a tolerance (§2.3, (21d)).

      The classification of (5) #

      source
      inductive HaslingerEtAl2025.DistMaxClass :
      Type

      The four cells of (5) cross obligatory distributivity with exception intolerance.

      Instances For
        source
        @[instance_reducible]
        instance HaslingerEtAl2025.instDecidableEqDistMaxClass :
        DecidableEq DistMaxClass
        Equations
        source
        def HaslingerEtAl2025.instReprDistMaxClass.repr :
        DistMaxClass → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance HaslingerEtAl2025.instReprDistMaxClass :
          Repr DistMaxClass
          Equations
          source
          def HaslingerEtAl2025.DistMaxClass.isDistributive :
          DistMaxClass → Prop

          The item applies its predicate to each atom separately.

          Equations
          Instances For
            source
            @[instance_reducible]
            instance HaslingerEtAl2025.instDecidablePredDistMaxClassIsDistributive :
            DecidablePred DistMaxClass.isDistributive
            Equations
            source
            def HaslingerEtAl2025.DistMaxClass.isMaximal :
            DistMaxClass → Prop

            The item tolerates no exceptions.

            Equations
            Instances For
              source
              @[instance_reducible]
              instance HaslingerEtAl2025.instDecidablePredDistMaxClassIsMaximal :
              DecidablePred DistMaxClass.isMaximal
              Equations
              source
              inductive HaslingerEtAl2025.Item :
              Type

              The expressions of (5) and (22) are the distance distributor jeweils and the determiner and distance uses of jed-, beside alle, numeral indefinites and definite plurals.

              Instances For
                source
                @[instance_reducible]
                instance HaslingerEtAl2025.instDecidableEqItem :
                DecidableEq Item
                Equations
                source
                @[instance_reducible]
                instance HaslingerEtAl2025.instReprItem :
                Repr Item
                Equations
                source
                def HaslingerEtAl2025.instReprItem.repr :
                Item → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[instance_reducible]
                  instance HaslingerEtAl2025.instFintypeItem :
                  Fintype Item
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  def HaslingerEtAl2025.Item.IsDeterminer :
                  Item → Prop

                  Whether the item is a determiner.

                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    instance HaslingerEtAl2025.instDecidablePredItemIsDeterminer :
                    DecidablePred Item.IsDeterminer
                    Equations
                    source
                    def HaslingerEtAl2025.Item.class :
                    Item → DistMaxClass

                    The classification of (5), obligatory distributivity crossed with exception intolerance.

                    Equations
                    Instances For
                      source
                      theorem HaslingerEtAl2025.jeweils_answers_Q :
                      Item.jeweils.class.isDistributive ∧ ¬Item.jeweils.class.isMaximal

                      Their question Q has a negative answer, since jeweils is obligatorily distributive and permits exceptions.

                      source
                      theorem HaslingerEtAl2025.four_cells (c : DistMaxClass) :
                      ∃ (i : Item), i.class = c

                      Every cell of the classification is filled, the fourth by jeweils.

                      source
                      theorem HaslingerEtAl2025.determiner_maximal (i : Item) :
                      i.IsDeterminer → i.class.isMaximal

                      §4 observation: among the attested items, every determiner is exception-intolerant.

                      The scenarios of (3) #

                      source
                      def HaslingerEtAl2025.classOfDatum (ex : Datum) :
                      Option DistMaxClass

                      The classification an example row's judgments in (3) determine: distributive if false in the cumulative scenario (3b), maximal if false in the exception scenario (3c).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem HaslingerEtAl2025.class_of_rows (p : Item × Datum) :
                        p ∈ [(Item.jederDP, Examples.ex1), (Item.jederDistance, Examples.ex2), (Item.alle, Examples.ex4a), (Item.numeralIndefinite, Examples.ex4b), (Item.definitePlural, Examples.ex4c)] → classOfDatum p.2 = some p.1.class

                        The rows of (1), (2), (4) and (22a) classify the items as (5) does, jeweils out of the blue included.

                        source
                        theorem HaslingerEtAl2025.jeweils_maximal_out_of_the_blue :
                        classOfDatum Examples.ex22a = some DistMaxClass.distMax

                        The magnets scenario of (23) #

                        source
                        @[reducible, inline]
                        abbrev HaslingerEtAl2025.Box :
                        Type

                        The five boxes of (23a).

                        Equations
                        Instances For
                          source
                          def HaslingerEtAl2025.hasTwoMagnets (b : Box) :
                          Prop

                          Every box but the fifth contains two magnets.

                          Equations
                          Instances For
                            source
                            @[instance_reducible]
                            instance HaslingerEtAl2025.instDecidablePredBoxHasTwoMagnets :
                            DecidablePred hasTwoMagnets
                            Equations
                            source
                            theorem HaslingerEtAl2025.jeder_rejects_magnets :
                            ¬∀ b ∈ Finset.univ, hasTwoMagnets b

                            jeder in either use, (21c), is false in the scenario, since one box has one magnet.

                            source
                            theorem HaslingerEtAl2025.jeweils_accepts_magnets :
                            () ∈ tolerant (fun (x1 x2 : Finset Box) => x1 ⊆ x2) (fun (z : Finset Box) => {_u : Unit | ∀ b ∈ z, hasTwoMagnets b}) Finset.univ

                            jeweils, (25), under the tolerance the explosion question induces, every part, is true, witnessed by the four boxes with two magnets. So is the determiner jeder* of (27), which is (25) applied to the sum of its restrictor, here all five boxes.

                            source
                            theorem HaslingerEtAl2025.jeweils_identity_rejects_magnets :
                            () ∉ tolerant (fun (x1 x2 : Finset Box) => x1 = x2) (fun (z : Finset Box) => {_u : Unit | ∀ b ∈ z, hasTwoMagnets b}) Finset.univ

                            The speakers who reject jeweils in the scenario are those whose tolerance is the identity, for whom it coincides with jeder.