def Semantics.Events.Krifka1998.UP {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) : Prop

Uniqueness of Participant (UP): each event has at most one θ-filler. eq. (43): θ(x,e) ∧ θ(y,e) → x = y.

Equations

• Semantics.Events.Krifka1998.UP θ = ∀ (x y : α) (e : β), θ x e → θ y e → x = y

def Semantics.Events.Krifka1998.CumTheta {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Cumulative theta (CumTheta): θ preserves sums. eq. (44): θ(x,e) ∧ θ(y,e') → θ(x⊕y, e⊕e'). This is the relational analog of IsSumHom.

Equations

• Semantics.Events.Krifka1998.CumTheta θ = ∀ (x y : α) (e e' : β), θ x e → θ y e' → θ (x ⊔ y) (e ⊔ e')

def Semantics.Events.Krifka1998.ME {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Mapping to Events (ME): object parts map to event parts. eq. (45): θ(x,e) ∧ y ≤ x → ∃e'. e' ≤ e ∧ θ(y,e').

Equations

• Semantics.Events.Krifka1998.ME θ = ∀ (x : α) (e : β) (y : α), θ x e → y ≤ x → ∃ e' ≤ e, θ y e'

def Semantics.Events.Krifka1998.MSE {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Mapping to Strict subEvents (MSE): proper object parts map to proper subevents. eq. (46): θ(x,e) ∧ y < x → ∃e'. e' < e ∧ θ(y,e').

Equations

• Semantics.Events.Krifka1998.MSE θ = ∀ (x : α) (e : β) (y : α), θ x e → y < x → ∃ e' < e, θ y e'

def Semantics.Events.Krifka1998.UE {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Uniqueness of Events (UE): each object part maps to a unique event part. eq. (47): θ(x,e) ∧ y ≤ x → ∃!e'. e' ≤ e ∧ θ(y,e').

Equations

• Semantics.Events.Krifka1998.UE θ = ∀ (x : α) (e : β) (y : α), θ x e → y ≤ x → ∃ e' ≤ e, θ y e' ∧ ∀ e'' ≤ e, θ y e'' → e'' = e'

def Semantics.Events.Krifka1998.MO {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Mapping to Objects (MO): event parts map to object parts. eq. (48): θ(x,e) ∧ e' ≤ e → ∃y. y ≤ x ∧ θ(y,e').

Equations

• Semantics.Events.Krifka1998.MO θ = ∀ (x : α) (e e' : β), θ x e → e' ≤ e → ∃ y ≤ x, θ y e'

def Semantics.Events.Krifka1998.MSO {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Mapping to Strict subObjects (MSO): proper subevents map to proper object parts. eq. (49): θ(x,e) ∧ e' < e → ∃y. y < x ∧ θ(y,e').

Equations

• Semantics.Events.Krifka1998.MSO θ = ∀ (x : α) (e e' : β), θ x e → e' < e → ∃ y < x, θ y e'

def Semantics.Events.Krifka1998.UO {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Uniqueness of Objects (UO): each event part maps to a unique object part. eq. (50): θ(x,e) ∧ e' ≤ e → ∃!y. y ≤ x ∧ θ(y,e').

Equations

• Semantics.Events.Krifka1998.UO θ = ∀ (x : α) (e e' : β), θ x e → e' ≤ e → ∃ y ≤ x, θ y e' ∧ ∀ z ≤ x, θ z e' → z = y

def Semantics.Events.Krifka1998.GUE {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) : Prop

Generalized Uniqueness of Events (GUE): each object participates in at most one event. eq. (52): θ(x,e) ∧ θ(x,e') → e = e'.

Equations

• Semantics.Events.Krifka1998.GUE θ = ∀ (x : α) (e e' : β), θ x e → θ x e' → e = e'

structure Semantics.Events.Krifka1998.SINC {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Strict Incrementality (SINC): the conjunction of MSO, UO, MSE, UE plus a non-degeneracy condition requiring extended entities. eq. (51):

SINC(θ) iff (i) MSO(θ) ∧ UO(θ) ∧ MSE(θ) ∧ UE(θ) (ii) ∃x,y∈U_P ∃e,e'∈U_E [y < x ∧ e' < e ∧ θ(x,e) ∧ θ(y,e')]

Condition (i) guarantees a bijective correspondence between the part structure of the object and the part structure of the event. Condition (ii) ensures θ actually applies to extended entities (ones with proper parts), ruling out degenerate cases where θ only relates atoms. This is the key property of incremental-theme verbs like "eat", "build", "read".

• mso : MSO θ

  Proper subevents map to proper object parts.

• uo : UO θ

  Each event part has a unique object counterpart.

• mse : MSE θ

  Proper object parts map to proper subevents.

• ue : UE θ

  Each object part has a unique event counterpart.

• extended : ∃ (x : α) (y : α) (e : β) (e' : β), y < x ∧ e' < e ∧ θ x e ∧ θ y e'

  Non-degeneracy: θ applies to at least one extended entity pair. eq. (51.ii): the relation must involve entities with proper parts, not just atoms.

theorem Semantics.Events.Krifka1998.me_of_mse {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : MSE θ) : ME θ

MSE implies ME: weaken strict to non-strict. : if proper parts map to proper subevents, then parts (including the whole) also map, taking e' = e when y = x.

theorem Semantics.Events.Krifka1998.mo_of_mso {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : MSO θ) : MO θ

MSO implies MO: weaken strict to non-strict (dual of me_of_mse).

theorem Semantics.Events.Krifka1998.me_of_sinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) : ME θ

SINC implies ME (via MSE).

theorem Semantics.Events.Krifka1998.mo_of_sinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) : MO θ

SINC implies MO (via MSO).

def Semantics.Events.Krifka1998.VP {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) (OBJ : α → Prop) : β → Prop

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

Equations

• Semantics.Events.Krifka1998.VP θ OBJ e = ∃ (y : α), OBJ y ∧ θ y e

theorem Semantics.Events.Krifka1998.cum_propagation {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ : α → Prop} (hCum : CumTheta θ) (hObj : Mereology.CUM OBJ) : Mereology.CUM (VP θ OBJ)

CUM propagation: cumulative θ transmits CUM from NP to VP. §3.3: CumTheta(θ) ∧ CUM(OBJ) → CUM(VP θ OBJ).

"eat apples" is CUM because:

• APPLES is CUM (mass/bare-plural NPs are cumulative)
• EAT's incremental theme is cumulative (CumTheta)
• Therefore VP = λe.∃y[apples(y) ∧ eat(y,e)] is CUM

Proof: Given VP(e₁) and VP(e₂), we have y₁ with OBJ(y₁) ∧ θ(y₁,e₁) and y₂ with OBJ(y₂) ∧ θ(y₂,e₂). By CumTheta, θ(y₁⊔y₂, e₁⊔e₂). By CUM(OBJ), OBJ(y₁⊔y₂). So VP(e₁⊔e₂).

theorem Semantics.Events.Krifka1998.qua_propagation {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ : α → Prop} (hUP : UP θ) (hMSO : MSO θ) (hQua : Mereology.QUA OBJ) : Mereology.QUA (VP θ OBJ)

QUA propagation: UP + MSO + UO transmit QUA from NP to VP. §3.3: UP(θ) ∧ MSO(θ) ∧ UO(θ) ∧ QUA(OBJ) → QUA(VP θ OBJ).

"eat two apples" is QUA because:

• TWO-APPLES is QUA (quantized NPs have no P-proper-parts)
• EAT's incremental theme is SINC + UP
• Therefore VP = λe.∃y[two-apples(y) ∧ eat(y,e)] is QUA

Proof: Suppose VP(e) via ⟨y, OBJ(y), θ(y,e)⟩ and e' < e. We must show ¬VP(e'). Suppose for contradiction VP(e') via ⟨z, OBJ(z), θ(z,e')⟩. By UP, z = y' for any other filler of e'. By MSO, ∃ y' < y with θ(y',e'). By UP, z = y'. So OBJ(y') with y' < y. But QUA(OBJ) says ¬OBJ(y'). Contradiction.

Functional case: When θ is a function (not a relation) with IsSumHom + Function.Injective, this reduces to qua_of_injective_sumHom in Core/Mereology.lean via qua_pullback. The relational UP + MSO conditions collapse to functional injectivity + monotonicity.

theorem Semantics.Events.Krifka1998.qua_propagation_sinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ : α → Prop} (hUP : UP θ) (hSinc : SINC θ) (hQua : Mereology.QUA OBJ) : Mereology.QUA (VP θ OBJ)

QUA propagation from SINC + UP (convenience wrapper). In practice, incremental-theme verbs satisfy both SINC and UP.

def Semantics.Events.Krifka1998.GRAD {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) (μ_obj : α → ℚ) (μ_ev : β → ℚ) : Prop

Graduality (GRAD): more object measure entails more event measure. @cite{krifka-1989}: GRAD(θ, μ_obj, μ_ev) ⇔ ∀x,y,e,e'. θ(x,e) ∧ θ(y,e') ∧ μ_obj(x) < μ_obj(y) → μ_ev(e) < μ_ev(e'). GRAD captures the intuition that eating more food takes more time.

Equations

• Semantics.Events.Krifka1998.GRAD θ μ_obj μ_ev = ∀ (x y : α) (e e' : β), θ x e → θ y e' → μ_obj x < μ_obj y → μ_ev e < μ_ev e'

theorem Semantics.Events.Krifka1998.grad_of_sinc {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) (μ_obj : α → ℚ) (μ_ev : β → ℚ) (_hSinc : SINC θ) [_hObj : Mereology.ExtMeasure α μ_obj] [_hEv : Mereology.ExtMeasure β μ_ev] (hProp : Mereology.MeasureProportional θ μ_obj μ_ev) : GRAD θ μ_obj μ_ev

SINC + extensive measures + measure proportionality → GRAD. @cite{krifka-1989}: strictly incremental themes with extensive measures and a constant consumption rate exhibit gradual change.

Proof: if μ_ev(e) = c · μ_obj(x) and μ_ev(e') = c · μ_obj(y), then μ_obj(x) < μ_obj(y) implies c · μ_obj(x) < c · μ_obj(y) since c > 0, giving μ_ev(e) < μ_ev(e').

structure Semantics.Events.Krifka1998.GRADSquare {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup γ] (θ : α → γ → Prop) (μ_obj : α → ℚ) (τ_fn : γ → β) (dur : β → ℚ) extends Mereology.LaxMeasureSquare θ μ_obj τ_fn dur : Type

The GRAD square extends LaxMeasureSquare with strict incrementality (SINC), enabling the derivation of GRAD (gradual change). The non-SINC theorems (MereoDim, QUA pullback, lax commutativity) are inherited from LaxMeasureSquare.

• laxComm : MeasureProportional θ μ_obj (dur ∘ τ_fn)
• ext₁ : ExtMeasure α μ_obj
• ext₂ : ExtMeasure γ (dur ∘ τ_fn)
• sinc : SINC θ

  Strict incrementality of the thematic role.

theorem Semantics.Events.Krifka1998.GRADSquare.laxCommutativity {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup γ] {θ : α → γ → Prop} {μ_obj : α → ℚ} {τ_fn : γ → β} {dur : β → ℚ} (sq : GRADSquare θ μ_obj τ_fn dur) {x : α} {e : γ} (hθ : θ x e) : dur (τ_fn e) = sq.laxComm.rate * μ_obj x

The defining equation of the GRAD square: for any θ-pair (x,e), the temporal measure equals the rate times the object measure.

theorem Semantics.Events.Krifka1998.GRADSquare.grad {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup γ] {θ : α → γ → Prop} {μ_obj : α → ℚ} {τ_fn : γ → β} {dur : β → ℚ} (sq : GRADSquare θ μ_obj τ_fn dur) : GRAD θ μ_obj (dur ∘ τ_fn)

GRAD follows from the square via grad_of_sinc.

theorem Semantics.Events.Krifka1998.GRADSquare.objMereoDim {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup γ] {θ : α → γ → Prop} {μ_obj : α → ℚ} {τ_fn : γ → β} {dur : β → ℚ} (sq : GRADSquare θ μ_obj τ_fn dur) : Mereology.MereoDim μ_obj

The object arm is a MereoDim (via ExtMeasure).

theorem Semantics.Events.Krifka1998.GRADSquare.evMereoDim {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup γ] {θ : α → γ → Prop} {μ_obj : α → ℚ} {τ_fn : γ → β} {dur : β → ℚ} (sq : GRADSquare θ μ_obj τ_fn dur) : Mereology.MereoDim (dur ∘ τ_fn)

The temporal arm (composed path) is a MereoDim (via ExtMeasure).

theorem Semantics.Events.Krifka1998.GRADSquare.qua_pullback_ev {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup γ] {θ : α → γ → Prop} {μ_obj : α → ℚ} {τ_fn : γ → β} {dur : β → ℚ} (sq : GRADSquare θ μ_obj τ_fn dur) {P : ℚ → Prop} (hP : Mereology.QUA P) : Mereology.QUA (P ∘ dur ∘ τ_fn)

QUA pullback through the temporal path: QUA on ℚ pulls back to QUA on events via the composed measure dur ∘ τ_fn.

inductive Semantics.Events.Krifka1998.VerbIncClass : Type

Incrementality annotations for verbs. §3.2–3.7: verbs differ in which thematic role properties their incremental theme satisfies.

• sinc : VerbIncClass

  Strictly incremental: consumption/creation verbs (eat, build). SINC + GUE on object role. Krifka §3.3.

• inc : VerbIncClass

  Incremental: allows backups (read, write). INC but ¬SINC on object role. Krifka §3.6.

• cumOnly : VerbIncClass

  Cumulative only: non-incremental (push, carry). CumTheta but ¬MSE on object role. Krifka §3.2.

instance Semantics.Events.Krifka1998.instDecidableEqVerbIncClass : DecidableEq VerbIncClass

Equations

• Semantics.Events.Krifka1998.instDecidableEqVerbIncClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Events.Krifka1998.instReprVerbIncClass.repr : VerbIncClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Semantics.Events.Krifka1998.instReprVerbIncClass : Repr VerbIncClass

Equations

• Semantics.Events.Krifka1998.instReprVerbIncClass = { reprPrec := Semantics.Events.Krifka1998.instReprVerbIncClass.repr }

instance Semantics.Events.Krifka1998.instBEqVerbIncClass : BEq VerbIncClass

Equations

• Semantics.Events.Krifka1998.instBEqVerbIncClass = { beq := Semantics.Events.Krifka1998.instBEqVerbIncClass.beq }

def Semantics.Events.Krifka1998.instBEqVerbIncClass.beq : VerbIncClass → VerbIncClass → Bool

Equations

• Semantics.Events.Krifka1998.instBEqVerbIncClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

class Semantics.Events.Krifka1998.VerbIncrementality (α : Type u_3) (β : Type u_4) [SemilatticeSup α] [SemilatticeSup β] (eat push build read_ : α → β → Prop) : Prop

Meaning postulates for verb incrementality. These axiomatize which verbs have which incrementality properties on their object/theme role.

• eat_sinc : SINC eat

  "eat" has a strictly incremental theme: consumption creates a bijection between food parts and eating subevents.

• eat_gue : GUE eat

  "eat" satisfies GUE: each portion of food is eaten at most once.

• push_cum : CumTheta push

  "push" is cumulative but not strictly incremental: the cart doesn't have parts that correspond to pushing subevents.

• build_sinc : SINC build

  "build" has a strictly incremental theme: creation mirrors consumption.

• build_gue : GUE build

  "build" satisfies GUE: each part is built at most once.

• read_cum : CumTheta read_

  "read" is incremental but not strictly so: allows re-reading.

inductive Semantics.Events.Krifka1998.IncClosure {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ' : α → β → Prop) : α → β → Prop

General Incrementality (INC): θ is the closure of some strictly incremental θ' under sum formation. eq. (59): θ is incremental iff there exists a SINC θ' such that θ(x,e) holds iff (x,e) can be decomposed into θ'-pairs that sum to (x,e). This handles "read the article" (allows re-reading/backups): reading events are built from strictly incremental reading-parts that can overlap in their object coverage.

Formulated inductively: the smallest relation containing θ' and closed under componentwise sum.

• base {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ' : α → β → Prop} {x : α} {e : β} : θ' x e → IncClosure θ' x e

  Base: anything in θ' is in the closure.

• sum {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ' : α → β → Prop} {x₁ x₂ : α} {e₁ e₂ : β} : IncClosure θ' x₁ e₁ → IncClosure θ' x₂ e₂ → IncClosure θ' (x₁ ⊔ x₂) (e₁ ⊔ e₂)

  Sum: if (x₁,e₁) and (x₂,e₂) are in the closure, so is (x₁⊔x₂, e₁⊔e₂).

def Semantics.Events.Krifka1998.INC {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

General Incrementality: θ is the IncClosure of some SINC θ'.

Equations

• Semantics.Events.Krifka1998.INC θ = ∃ (θ' : α → β → Prop), Semantics.Events.Krifka1998.SINC θ' ∧ ∀ (x : α) (e : β), θ x e ↔ Semantics.Events.Krifka1998.IncClosure θ' x e

theorem Semantics.Events.Krifka1998.inc_of_sinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) (hCum : CumTheta θ) : INC θ

SINC + CumTheta implies INC: a strictly incremental θ that is cumulative is trivially its own closure. CumTheta ensures the reverse direction: IncClosure θ ⊆ θ.

theorem Semantics.Events.Krifka1998.sinc_cum_propagation {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ : α → Prop} (hCumTheta : CumTheta θ) (hObj : Mereology.CUM OBJ) : Mereology.CUM (VP θ OBJ)

Bridge: CUM propagation via CumTheta + CUM(OBJ). CumTheta(θ) ∧ CUM(OBJ) → CUM(VP θ OBJ). In CEM models, SINC implies CumTheta, so this covers the "SINC verb + CUM noun → CUM VP" case from §3.3.

theorem Semantics.Events.Krifka1998.sinc_qua_propagation {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ : α → Prop} (hUP : UP θ) (hSinc : SINC θ) (hQua : Mereology.QUA OBJ) : Mereology.QUA (VP θ OBJ)

Bridge: QUA propagation from SINC + UP (renamed for API).

theorem Semantics.Events.Krifka1998.roleHom_implies_cumTheta {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : β → α} (hf : Mereology.IsSumHom f) : CumTheta fun (x : α) (e : β) => f e = x

Bridge: RoleHom (functional θ from Mereology.lean) implies CumTheta (relational θ). A sum-homomorphic function θ : β → α induces a cumulative relation λ x e, θ(e) = x.

With injectivity, we additionally get StrictMono via IsSumHom.strictMono_of_injective (Core/Mereology.lean §10), which enables qua_of_injective_sumHom — the functional QUA propagation theorem.