Documentation

Linglib.Theories.Semantics.ArgumentStructure.Affectedness.Defs

Scalar Result Substrate #

@cite{beavers-2011} @cite{beavers-koontz-garboden-2020} @cite{rappaport-hovav-levin-2001}

Substrate primitives for the scalar-theoretic affectedness hierarchy.

Two independent typeclasses, mirroring Beavers' two empirical primitives:

Three abstract Props characterise Beavers (60a-c) on a thematic relation θ : α → β → Prop. Beavers (60d) Unspecified (mere participation) is not formalised — it is True for every binary relation and contributes no content to the typeclass chain. The discrete AffectednessDegree enum in AffectednessHierarchy.lean keeps unspecified as a level tag; the typeclass chain bottoms at IsPotentialAffected.

Mathlib decomposition #

HasScalarResult and HasLatentScale are data-bearing typeclasses (per-verb structural commitments — patient type, dimension type, event type). The three Beavers Props are plain definitions, used as typeclass content one layer up in Theories/Semantics/Events/Scalar/Affectedness.lean.

Mathlib pattern: cf. MeasurableSpace α (structure) + MeasurableSet s (Prop using the structure) + IsFiniteMeasure μ (Prop using both).

Why Unspecified is not formalised #

@cite{beavers-2011} (60d): φ → ∃e∃θ'[θ'(x, e)] — mere participation. For any binary θ : α → β → Prop, θ x e IS the participation, so the implication θ x e → ∃ θ', θ'(x, e) holds vacuously by taking θ' = θ. A formal definition Unspecified θ := True (or its β-equivalent θ → θ) carries no content and adds no information to consumer proofs. The hierarchy "bottoms out" at Potential for typeclass purposes; the unspecified enum tag in AffectednessHierarchy.lean represents "no class declared," parallel to mathlib's separation-axiom enums having more cases than typeclasses (only T0/T1/T2/... are typeclasses; "non-T0" isn't).

HasScalarResult — result-state typeclass #

source
class Semantics.ArgumentStructure.Affectedness.HasScalarResult (α : Type u_1) (δ : Type u_2) (β : Type u_3) :
Type (max (max u_1 u_2) u_3)

HasScalarResult α δ β provides the predicate resultAt x g e: "patient x : α ends event e : β holding degree g : δ."

The primitive that @cite{beavers-2011} eq. (60a-b) requires to define Quantized and Non-quantized affectedness. The "state" token s in Beavers' eq. (60) is decorative for level-typing (Quantized / Non-quantized are existential generalisations over s) and elided in the 3-place form here. Consumers needing s for result-XP licensing or halfway-modification semantics (@cite{beavers-koontz-garboden-2020} §1.6.1) reintroduce it downstream.

Mathlib pattern: structural typeclass with multiple type parameters, analogous to Module R M. Per-verb the dimension δ is determined by lexical content (cool on temperature, widen on width, eat on consumption); each verb's θ : α → β → Prop references the appropriate instance.

  • resultAt : α → δ → β → Prop

    Patient x ends event e holding degree g on dimension δ.

Instances

    HasLatentScale — force-recipient typeclass #

    source
    class Semantics.ArgumentStructure.Affectedness.HasLatentScale (α : Type u_1) (β : Type u_2) :
    Type (max u_1 u_2)

    HasLatentScale α β provides the predicate latentScale x e: "patient x : α is a force-recipient at event e : β, related to some scale (latent), no transition entailed."

    The primitive that @cite{beavers-2011} eq. (60c) requires to define Potential affectedness. Originates with @cite{rappaport-hovav-levin-2001}'s "force recipient" — a verb that imparts force to its theme without committing to a specific result state (surface contact / impact verbs: wipe, scrub, rub, punch, hit, kick, slap).

    Independent from HasScalarResult: a verb may have a latent scale without entailing a final degree (Potential-only verbs), entail a final degree without an explicit force-recipient relation (NonQuantized verbs whose Potential is derived via the implication chain in §4), or both.

    • latentScale : α → β → Prop

      Patient x is a force-recipient at event e (latent scale relation).

    Instances

      Beavers (60a-c) Affectedness Props #

      source
      def Semantics.ArgumentStructure.Affectedness.Quantized {α : Type u_1} {δ : Type u_2} {β : Type u_3} [HasScalarResult α δ β] (θ : α → β → Prop) (g_φ : δ) :
      Prop

      @cite{beavers-2011} eq. (60a) Quantized: θ entails patient x ends event e holding the SPECIFIC degree g_φ. φ → ∃e∃s[result'(x, s, g_φ, e)].

      The g_φ is fixed by the predicate φ — Beavers' point is that quantized verbs name a specific endpoint (dead for kill, broken for break, g₁₀₀°C for heat to 100°C). Per-verb g_φ lives in IsQuantizedAffected as data (a typeclass field, not existentially bound), preserving the lexical commitment.

      Linguistic exemplars: accomplishments / achievements (break, shatter, destroy, devour x).

      Equations
      Instances For
        source
        def Semantics.ArgumentStructure.Affectedness.NonQuantized {α : Type u_1} {δ : Type u_2} {β : Type u_3} [HasScalarResult α δ β] (θ : α → β → Prop) :
        Prop

        @cite{beavers-2011} eq. (60b) Non-quantized: θ entails patient x ends event e holding SOME degree (not necessarily specific). φ → ∃e∃s∃g[result'(x, s, g, e)].

        Linguistic exemplars: degree achievements (widen, cool, lengthen, cut, slice x).

        Equations
        Instances For
          source
          def Semantics.ArgumentStructure.Affectedness.Potential {α : Type u_1} {β : Type u_2} [HasLatentScale α β] (θ : α → β → Prop) :
          Prop

          @cite{beavers-2011} eq. (60c) Potential: θ entails patient x is a force-recipient at event e (latent scale exists, no transition entailed). φ → ∃e∃s∃θ_scale[θ_scale(x, s, e)].

          Defined via the HasLatentScale primitive — NOT by excluded middle over a result state (that encoding would be vacuous, equivalent to Nonempty δ via Classical.em). The latent-scale relation IS the formal content of "force recipient" per @cite{rappaport-hovav-levin-2001}.

          Linguistic exemplars: surface contact / impact verbs (wipe, scrub, rub, punch, hit, kick, slap x).

          Equations
          Instances For

            Implication Chain (Beavers eq. 62) #

            @cite{beavers-2011} eq. (62) — The Affectedness Hierarchy: quantized → non-quantized → potential. Each level entails the next-weaker. The Quantized → Non-quantized step is direct; the Non-quantized → Potential step requires a forgetful link from HasScalarResult to HasLatentScale (since they are independent typeclasses by design — see §2 docstring rationale).

            source
            theorem Semantics.ArgumentStructure.Affectedness.nonQuantized_of_quantized {α : Type u_1} {δ : Type u_2} {β : Type u_3} [HasScalarResult α δ β] {θ : α → β → Prop} {g_φ : δ} (h : Quantized θ g_φ) :
            NonQuantized θ

            Quantized entails Non-quantized: a specific final degree witnesses the existential. @cite{beavers-2011} eq. (62) leftmost arrow.

            source
            theorem Semantics.ArgumentStructure.Affectedness.potential_of_nonQuantized {α : Type u_1} {δ : Type u_2} {β : Type u_3} [HasScalarResult α δ β] [HasLatentScale α β] {θ : α → β → Prop} (forget : ∀ (x : α) (e : β), (∃ (g : δ), HasScalarResult.resultAt x g e) → HasLatentScale.latentScale x e) (h : NonQuantized θ) :
            Potential θ

            Non-quantized entails Potential under a forgetful link: if the HasScalarResult instance can be projected to a HasLatentScale instance (i.e., having a result state at any degree implies being a force-recipient), then NonQuantized lifts to Potential. @cite{beavers-2011} eq. (62) middle arrow.

            The link witness forget is the explicit assumption that "patient ends event with some result state" implies "patient is a force-recipient at the event." This always holds in the canonical model (a result-bearing event is, a fortiori, force-receiving) but is stated as a hypothesis here to keep the typeclasses formally independent.