Documentation

Linglib.Theories.Semantics.Aspect.Cumulativity

Cumulativity and Quantization Propagation #

@cite{krifka-1998} @cite{krifka-1989} @cite{champollion-2017}

The central K98 §3.3 result: a thematic relation θ between objects and events propagates mereological properties (CUM, QUA) from the object NP to the VP it forms via existential closure. Plus VP formation itself (eq. 53) and the bridge theorems linking SINC + UP to the two propagation chains.

Topic-named (not paper-named): defines the deep substrate that @cite{krifka-1998} §3.3 establishes, that @cite{krifka-1989}'s nominal-reference-to-VP-aspect chain depends on, and that @cite{champollion-2017}'s stratified-reference modernization rests on.

Mathlib discipline: typeclass form is canonical #

The public API is the typeclass-form cum_propagation and qua_propagation (taking [IsCumThetaVerb θ] / [IsSincVerb θ]). The explicit-witness variants (cum_propagation_of_cumTheta, qua_propagation_of_mso, qua_propagation_of_sinc) are private proof-factoring helpers, not part of the public API — mathlib pattern.

VP Formation (K98 §3.3 eq. 53) #

source
def Semantics.Aspect.Cumulativity.VP {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) (OBJ : α → Prop) :
β → Prop

VP predicate formed by existential closure over the object argument. @cite{krifka-1998} eq. 53: VP_θ,OBJ = λe.∃y[OBJ(y) ∧ θ(y,e)]. "eat apples" = λe.∃y[apples(y) ∧ eat.theme(y,e)].

Equations
Instances For

    CUM Propagation (K98 §3.3) #

    QUA Propagation (K98 §3.3) #

    Public typeclass-form API (mathlib discipline) #

    The canonical public API: typeclass-form propagation theorems that consumers should prefer over the _of_* smart constructors above. Mathlib pattern — add_assoc [Semigroup α] is the canonical name; explicit-witness variants are smart constructors with _of_* suffixes when they exist at all.

    source
    theorem Semantics.Aspect.Cumulativity.cum_propagation {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} [ArgumentStructure.IsCumThetaVerb θ] {OBJ : α → Prop} (hObj : Mereology.CUM OBJ) :
    Mereology.CUM (VP θ OBJ)

    CUM propagation (canonical typeclass form). Fires on any verb θ with [IsCumThetaVerb θ] — including SINC and INC verbs via the upward instances in Aspect/Incremental.lean / Aspect/Incremental.lean.

    source
    theorem Semantics.Aspect.Cumulativity.qua_propagation {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} [Incremental.IsSincVerb θ] {OBJ : α → Prop} (hQua : Mereology.QUA OBJ) :
    Mereology.QUA (VP θ OBJ)

    QUA propagation (canonical typeclass form). Fires on [IsSincVerb θ] — the typeclass bundles the SINC + UP witnesses needed by K98 §3.3 quantization-propagation.