Documentation

Studies.Tham2025

Tham (2025): Multidimensionality and the Scalar Components of Physical Disturbance Predicates #

This file formalizes [Tha25]'s account of physical disturbance predicates, change-of-state verbs such as crack, dent and scratch and their deverbal adjectives, whose root has a count noun form naming an irregularity in an affected host ([Kar77a]). The paper argues that the predicates are associated with a gradable scale closed at both ends, against the two-point scale of [RH14] and the partial, upper-open scale of [RW04b]: the verb has durative uses and the adjective comparative ones, (10)–(11), both take completely and partially, (15), (20)–(21), and both telic and atelic uses of the verb entail the adjectival state, (14), (17). The adjective is multidimensional in the sense of [Sas13] and [Sol18a]: badly evokes the quantity, quality or positioning of the disturbances, (22)–(25), and respect phrases individuate the dimensions, (28). The three scalar components have three sources (section 3.4): the lower bound is the existence of a disturbance, so unmodified predication is objective, (26); the gradable interval comes from the dimensions, so degree-modified predication admits faultless disagreement, (27); and the upper bound is the spatial extent of the host, (33).

The adjective's measure function (47b) is the weighted extent of the disturbances relative to the host's spatial extent, degree, with the weights the context's dimensions; the positive form (46) compares it with a degree, Pos. A weighting positive on every dimension makes the degree positive exactly when some disturbance has positive extent, degree_pos_iff, so whether the host is cracked does not depend on the weighting, degree_pos_iff_degree_pos, while the weightings that select single dimensions, the respect phrases respect, can rank two hosts oppositely, more_respect_and_more_respect. A disturbance within the host's extent has a degree at most one, degree_le_one, and the same disturbance on a smaller host has a higher degree, degree_lt_degree_of_lt. The verb (48) describes an event whose final degree meets the root's standard and exceeds the initial degree by a difference degree, Event, Verb: every use of the verb entails the adjective at the standard, Verb.pos_final, and the verb modified by a high difference degree entails the adjective modified by the same degree, Verb.pos, but not conversely, since a pre-existing crack that grows a little leaves the windshield badly cracked without its having cracked badly, Event.pos_not_verb.

Implementation notes #

The measure sums over an index type of dimensions, each with a nonnegative extent measure on hosts, in the profile vocabulary of SocialChoice; the paper's comparative at a weighting is the utilitarian rule on the extent profile when the hosts have the same spatial extent, more_iff_utilitarian. A respect phrase is the weighting Pi.single i 1, so respect phrases and quantification over respects are the paper's grammatical access to dimensions for the adjective; the paper's claim that the verb allows only conceptual access, and its speculation that the difference degree is the reason, are not formalized. The examples are the rows of Data.Examples.Tham2025; the consultant counts of section 4.2 and the online survey of section 3.2.2 are recorded in their comments.

References #

The adjective (section 5.2, (46)–(47)) #

def Tham2025.degree {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] (k : ι → K) (v : SocialChoice.Profile ι α K) (spatial : α → K) (x : α) :
K

The degree of disturbance of a host (47b) is the extent of its disturbances along each dimension, weighted by the context, relative to its spatial extent.

Equations
Instances For
    def Tham2025.respect {ι : Type u_1} {K : Type u_3} [Field K] [DecidableEq ι] (i : ι) :
    ι → K

    A respect phrase weights the single dimension it names.

    Equations
    Instances For
      theorem Tham2025.degree_eq_one_iff {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {k : ι → K} {v : SocialChoice.Profile ι α K} {spatial : α → K} {x : α} (hs : spatial x ≠ 0) :
      degree k v spatial x = 1 ↔ k ⬝ᵥ v x = spatial x

      Completely (20), (33) says that the disturbance exhausts the host's extent.

      theorem Tham2025.degree_respect {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {v : SocialChoice.Profile ι α K} {spatial : α → K} {x : α} [DecidableEq ι] {i : ι} :
      degree (respect i) v spatial x = v x i / spatial x

      Under a respect phrase the degree is the extent along the named dimension.

      def Tham2025.Pos {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (k : ι → K) (v : SocialChoice.Profile ι α K) (spatial : α → K) (d : K) (x : α) :

      The positive form (46) holds when the host is disturbed to degree d or beyond.

      Equations
      Instances For
        def Tham2025.More {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (k : ι → K) (v : SocialChoice.Profile ι α K) (spatial : α → K) (x y : α) :

        The comparative holds when x is more disturbed than y.

        Equations
        Instances For
          theorem Tham2025.degree_nonneg {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {k : ι → K} {v : SocialChoice.Profile ι α K} {spatial : α → K} {x : α} [LinearOrder K] [IsStrictOrderedRing K] (hk : ∀ (i : ι), 0 ≤ k i) (hv : ∀ (i : ι), 0 ≤ v x i) (hs : 0 ≤ spatial x) :
          0 ≤ degree k v spatial x
          theorem Tham2025.degree_pos_iff {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {k : ι → K} {v : SocialChoice.Profile ι α K} {spatial : α → K} {x : α} [LinearOrder K] [IsStrictOrderedRing K] (hk : ∀ (i : ι), 0 < k i) (hv : ∀ (i : ι), 0 ≤ v x i) (hs : 0 < spatial x) :
          0 < degree k v spatial x ↔ ∃ (i : ι), 0 < v x i

          The lower bound is the existence of a disturbance (section 3.4). Under a weighting positive on every dimension, the host has a positive degree exactly when some disturbance has positive extent.

          theorem Tham2025.degree_pos_iff_degree_pos {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {k : ι → K} {v : SocialChoice.Profile ι α K} {spatial : α → K} {x : α} [LinearOrder K] [IsStrictOrderedRing K] {k' : ι → K} (hk : ∀ (i : ι), 0 < k i) (hk' : ∀ (i : ι), 0 < k' i) (hv : ∀ (i : ι), 0 ≤ v x i) (hs : 0 < spatial x) :
          0 < degree k v spatial x ↔ 0 < degree k' v spatial x

          Unmodified predication is objective (section 3.2.1), since whether the host is disturbed at all does not depend on the weighting of the dimensions.

          theorem Tham2025.degree_le_one {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {k : ι → K} {v : SocialChoice.Profile ι α K} {spatial : α → K} {x : α} [LinearOrder K] [IsStrictOrderedRing K] (h : k ⬝ᵥ v x ≤ spatial x) (hs : 0 < spatial x) :
          degree k v spatial x ≤ 1

          The upper bound is the spatial extent of the host (section 3.4), so a disturbance within the host's extent has degree at most one.

          theorem Tham2025.degree_lt_degree_of_lt {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {k : ι → K} {v : SocialChoice.Profile ι α K} {spatial : α → K} {x : α} [LinearOrder K] [IsStrictOrderedRing K] {spatial' : α → K} (h0 : 0 < k ⬝ᵥ v x) (hs : 0 < spatial' x) (h : spatial' x < spatial x) :
          degree k v spatial x < degree k v spatial' x

          The same disturbance on a smaller host is a higher degree of disturbance.

          theorem Tham2025.more_iff_utilitarian {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {k : ι → K} {v : SocialChoice.Profile ι α K} {spatial : α → K} {x y : α} [LinearOrder K] [IsStrictOrderedRing K] (hs : spatial x = spatial y) (hs0 : 0 < spatial x) :
          More k v spatial x y ↔ SocialChoice.utilitarian k v x y ∧ ¬SocialChoice.utilitarian k v y x

          At equal spatial extents the comparative is the utilitarian rule of the weighting on the extent profile.

          Respect phrases (sections 3.2.2 and 4.2) #

          theorem Tham2025.more_respect_iff {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {v : SocialChoice.Profile ι α K} {spatial : α → K} {x y : α} [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq ι] {i : ι} (hs : spatial x = spatial y) (hs0 : 0 < spatial x) :
          More (respect i) v spatial x y ↔ v y i < v x i

          In more dented with respect to dent size (28a), (42a), the comparative under a respect phrase compares the named dimension alone.

          theorem Tham2025.more_respect_and_more_respect {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] {v : SocialChoice.Profile ι α K} {spatial : α → K} {x y : α} [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq ι] {i j : ι} (hs : spatial x = spatial y) (hs0 : 0 < spatial x) (hi : v y i < v x i) (hj : v x j < v y j) :
          More (respect i) v spatial x y ∧ More (respect j) v spatial y x

          Degree-modified predication allows faultless disagreement (27), (28a), since two hosts can each be more disturbed than the other with respect to some dimension.

          The verb (section 5.2, (48)) #

          structure Tham2025.Event {σ : Type u_1} {K : Type u_2} [LinearOrder K] (μ : σ → K) (std : K) :
          Type u_1

          A physical disturbance event (48) is a change between states whose final degree of disturbance meets the root's standard and exceeds the initial degree. The initial degree may already meet the standard, when the host bears an earlier disturbance.

          • init : σ

            The state at the start of the event.

          • final : σ

            The state at the end of the event.

          • lt : μ self.init < μ self.final
          • std_le : std ≤ μ self.final
          Instances For
            def Tham2025.Event.diff {σ : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] {μ : σ → K} {std : K} (e : Event μ std) :
            K

            The difference degree of an event is the degree of change it describes.

            Equations
            Instances For
              def Tham2025.Verb {σ : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] {μ : σ → K} {std : K} (d : K) (e : Event μ std) :

              The verb at a difference degree, its degree argument in (48).

              Equations
              Instances For
                theorem Tham2025.Verb.pos_final {σ : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] {μ : σ → K} {std d : K} {e : Event μ std} :
                Verb d e → std ≤ μ e.final

                Cracked completely/slightly entails is cracked (17a), since every event entails the adjectival state at the root's standard, whatever its difference degree.

                theorem Tham2025.Event.pos_not_verb {σ : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] {μ : σ → K} {std d : K} (e : Event μ std) (hd : d ≤ μ e.final) (h : e.diff < d) :
                d ≤ μ e.final ∧ ¬Verb d e

                Badly cracked holds without cracked badly (section 5.2). A windshield with a pre-existing crack that grows a little is badly cracked at the end, yet did not crack badly, since the difference degree is small.

                theorem Tham2025.Event.diff_pos {σ : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] {μ : σ → K} {std : K} [IsStrictOrderedRing K] (e : Event μ std) :
                0 < e.diff
                theorem Tham2025.Verb.pos {σ : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] {μ : σ → K} {std : K} [IsStrictOrderedRing K] {d : K} {e : Event μ std} (h : Verb d e) (h0 : 0 ≤ μ e.init) :
                d ≤ μ e.final

                Cracked badly entails badly cracked, since the difference degree is at most the final degree.