Documentation

Linglib.Theories.Semantics.Lexical.Measurement

Cross-Categorial Measurement Semantics #

@cite{wellwood-2015} @cite{kennedy-2007}

@cite{wellwood-2015} argues that all comparative sentences contain a covert much morpheme whose semantics is a measure function μ assigned by a variable assignment A:

⟦much_μ⟧^A = A(μ)

The measure function must be monotonic: for all α, β in a part-whole ordered domain, if α ≺^Part β then μ(α) ≺^Deg μ(β). This is @cite{schwarzschild-wilkinson-2002}'s monotonicity condition, and corresponds exactly to StrictMono / MereoDim / CSW's admissibleMeasure in linglib.

The key insight is a three-way cross-categorial parallel:

Dimensionality differences (VOLUME vs TEMPERATURE vs DURATION) follow from what is measured (entities, events, states), not from which expression introduces the measurement (§3.4). This is formalized as DimensionallyRestricted: a domain is dimensionally restricted iff any two admissible measure functions agree on the comparative ordering — which holds exactly for linear orders (GA state domains) and fails for partial orders with incomparable elements (entity/event domains where weight and volume can disagree).

Key Identifications #

Interpretive Note #

@cite{wellwood-2015} does not explicitly label GA state domains as "cumulative" in Krifka's technical sense (closure under join). She argues they "form mereologies" — ordered domains with proper parts. We classify them as .cumulative because the structural consequence is the same: mereological structure enables monotonic measurement by much.

source
inductive Semantics.Lexical.Measurement.MereologicalStatus :
Type

Cross-categorial mereological classification (§2–3).

Predicates across nominal, verbal, and adjectival domains fall into two classes based on their mereological properties:

  • cumulative: domain has mereological structure with proper parts, enabling monotonic measurement by much. Includes mass nouns (CUM), atelic VPs (CUM), and gradable adjectives (states form mereologies).
  • quantized: domain lacks non-trivial part-whole structure for measurement. Count nouns (QUA), telic VPs (QUA), and non-gradable adjectives (atomic, unordered states).
Instances For
    source
    instance Semantics.Lexical.Measurement.instDecidableEqMereologicalStatus :
    DecidableEq MereologicalStatus
    Equations
    source
    def Semantics.Lexical.Measurement.instBEqMereologicalStatus.beq :
    MereologicalStatus → MereologicalStatus → Bool
    Equations
    Instances For
      source
      instance Semantics.Lexical.Measurement.instBEqMereologicalStatus :
      BEq MereologicalStatus
      Equations
      source
      instance Semantics.Lexical.Measurement.instReprMereologicalStatus :
      Repr MereologicalStatus
      Equations
      source
      def Semantics.Lexical.Measurement.instReprMereologicalStatus.repr :
      MereologicalStatus → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Semantics.Lexical.Measurement.MereologicalStatus.toBoundedness :
        MereologicalStatus → Core.Scale.Boundedness

        Map mereological status to Kennedy scale boundedness.

        CUM → no inherent endpoint → open scale (→ blocked degree modifiers) QUA → inherent endpoint → closed scale (→ licensed degree modifiers)

        This connects cross-categorial classification to Kennedy's scale structure, via the existing cumBoundedness/quaBoundedness annotations in Core.MereoDim.

        Equations
        Instances For
          source
          theorem Semantics.Lexical.Measurement.toBoundedness_coherent :
          MereologicalStatus.cumulative.toBoundedness = Mereology.cumBoundedness ∧ MereologicalStatus.quantized.toBoundedness = Mereology.quaBoundedness

          The toBoundedness mapping agrees with the existing mereological scale annotations in Core.MereoDim.

          source
          @[reducible, inline]
          abbrev Semantics.Lexical.Measurement.MuchSem {A : Type u_1} {D : Type u_2} [Preorder A] [Preorder D] (μ : A → D) :
          Prop

          Admissibility constraint on measure functions introduced by much.

          much_μ has the denotation ⟦much_μ⟧^A = A(μ) — simply a variable-assignment lookup returning a measure function μ. The admissibility condition on that measure function requires strict monotonicity (order preservation):

          for all α, β ∈ D_≤Part, if α ≺^Part β then μ(α) ≺^Deg μ(β)

          MuchSem μ captures this felicity condition, not much's denotation itself. It is StrictMono, equivalently MereoDim.toStrictMono or CSW's admissibleMeasure.

          Equations
          Instances For
            source
            theorem Semantics.Lexical.Measurement.muchSem_eq_admissibleMeasure {S : Type u_1} {D : Type u_2} [Preorder S] [Preorder D] (μ : S → D) :
            MuchSem μ ↔ Adjective.StatesBased.admissibleMeasure μ

            MuchSem is definitionally equal to CSW's admissible measure constraint. Both require strict order preservation. This makes the–CSW identification explicit: changing either definition breaks this theorem.

            source
            theorem Semantics.Lexical.Measurement.muchSem_of_mereoDim {A : Type u_1} {D : Type u_2} [PartialOrder A] [PartialOrder D] {μ : A → D} (h : Mereology.MereoDim μ) :
            MuchSem μ

            Every MereoDim witness provides a MuchSem proof. MereoDim bundles StrictMono in a typeclass; MuchSem is the unbundled predicate.

            source
            def Semantics.Lexical.Measurement.telicityToStatus :
            Tense.Aspect.LexicalAspect.Telicity → MereologicalStatus

            Telicity determines mereological status: atelic VPs have CUM domains (activities, states), telic VPs have QUA domains (achievements, accomplishments).

            Equations
            Instances For
              source
              def Semantics.Lexical.Measurement.numberToStatus :
              Noun.Kind.Dayal2004.NumberFeature → MereologicalStatus

              Number feature determines mereological status: mass nouns have CUM domains; count nouns (sg/pl) have QUA domains.

              Note: plural count nouns are CUM at the plurality level ("Plural predicates are cumulative"), but their measurement is restricted to NUMBER (counting atoms). At the lexical level, count nouns are QUA.

              Equations
              Instances For
                source
                def Semantics.Lexical.Measurement.gradableToStatus :
                MereologicalStatus

                Gradable adjectives predicate of states that "form mereologies", enabling monotonic measurement by much.

                Interpretive note: does not explicitly use the label CUM for GA state domains. She argues they have mereological structure (ordered domains with proper parts). We classify them as .cumulative because the structural consequence is identical: mereological structure enables monotonic measurement.

                Equations
                Instances For
                  source
                  def Semantics.Lexical.Measurement.nonGradableToStatus :
                  MereologicalStatus

                  Non-gradable adjectives (wooden, triangular) predicate of "atomic, unordered objects". Their state domains lack both mereological structure and comparative ordering, making them not measurable by much.

                  This is stronger than QUA in the strict technical sense: QUA merely requires no P-proper-parts on a partial order, while non-GA states lack ordering entirely. We classify them as .quantized as the closest approximation.

                  Equations
                  Instances For
                    source
                    def Semantics.Lexical.Measurement.vendlerToStatus (c : Tense.Aspect.LexicalAspect.VendlerClass) :
                    MereologicalStatus

                    Vendler classification determines mereological status via telicity. States and activities are atelic → cumulative; achievements and accomplishments are telic → quantized.

                    Equations
                    Instances For
                      source
                      theorem Semantics.Lexical.Measurement.state_is_cumulative :
                      vendlerToStatus Tense.Aspect.LexicalAspect.VendlerClass.state = MereologicalStatus.cumulative
                      source
                      theorem Semantics.Lexical.Measurement.activity_is_cumulative :
                      vendlerToStatus Tense.Aspect.LexicalAspect.VendlerClass.activity = MereologicalStatus.cumulative
                      source
                      theorem Semantics.Lexical.Measurement.achievement_is_quantized :
                      vendlerToStatus Tense.Aspect.LexicalAspect.VendlerClass.achievement = MereologicalStatus.quantized
                      source
                      theorem Semantics.Lexical.Measurement.accomplishment_is_quantized :
                      vendlerToStatus Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = MereologicalStatus.quantized
                      source
                      theorem Semantics.Lexical.Measurement.telicize_shifts_status (p : Tense.Aspect.LexicalAspect.AspectualProfile) (h : p.telicity = Tense.Aspect.LexicalAspect.Telicity.atelic) :
                      telicityToStatus p.telicity = MereologicalStatus.cumulative ∧ telicityToStatus p.telicize.telicity = MereologicalStatus.quantized

                      Telicization shifts measurement status from cumulative to quantized.

                      Adding a goal PP to an atelic VP ("ran" → "ran to the park") changes the predicate's mereological status, blocking extensive dimensions (DURATION, DISTANCE) and restricting to NUMBER. This connects grammar-shifts-measurement claim to the existing AspectualProfile.telicize operation.

                      source
                      theorem Semantics.Lexical.Measurement.atelicize_shifts_status (p : Tense.Aspect.LexicalAspect.AspectualProfile) (h : p.telicity = Tense.Aspect.LexicalAspect.Telicity.telic) :
                      telicityToStatus p.telicity = MereologicalStatus.quantized ∧ telicityToStatus p.atelicize.telicity = MereologicalStatus.cumulative

                      Atelicization shifts measurement status from quantized to cumulative.

                      The progressive on a telic VP ("built the house" → "was building the house") restores extensive dimensions.

                      source
                      def Semantics.Lexical.Measurement.DimensionallyRestricted (α : Type u_1) [Preorder α] :
                      Prop

                      A domain is dimensionally restricted when any two admissible measure functions (StrictMono maps to ℚ) agree on the comparative ordering of all elements.

                      This captures claim that GAs lexically fix a single dimension while nouns/verbs allow contextual dimension selection:

                      • GA state domains: linearly ordered → any two StrictMono μ₁, μ₂ agree on the comparative → dimensionally restricted
                      • Entity/event domains: partially ordered with incomparable elements → different ExtMeasures (weight vs volume) can disagree → not dimensionally restricted

                      The structural content: dimensional restriction holds iff the ambient preorder is total (a LinearOrder). The forward direction is linearOrder_dimensionallyRestricted; the converse is witnessed by any two incomparable elements with disagreeing measures.

                      Equations
                      Instances For
                        source
                        theorem Semantics.Lexical.Measurement.linearOrder_dimensionallyRestricted {α : Type u_1} [LinearOrder α] :
                        DimensionallyRestricted α

                        Linear orders are dimensionally restricted: the comparative ordering is uniquely determined by the ambient order, regardless of which admissible measure function is chosen.

                        Proof: on a linear order, StrictMono reflects the strict order (by trichotomy + irreflexivity), so μ₁ a < μ₁ b ↔ a < b ↔ μ₂ a < μ₂ b.

                        source
                        theorem Semantics.Lexical.Measurement.statesBasedEntry_restricted {S : Type u_1} [LinearOrder S] (_entry : Adjective.StatesBased.StatesBasedEntry S) :
                        DimensionallyRestricted S

                        A StatesBasedEntry over a linearly ordered state domain is dimensionally restricted: the comparative meaning is independent of which admissible measure function is chosen.

                        This explains CSW's observation (72): scale-mates like confident and certain share a background ordering, and any admissible measure on that ordering gives the same comparative truth conditions. The comparative is determined by the ordering alone, not by which adjective introduces it.