@cite{krifka-1989} "Nominal Reference, Temporal Constitution and Quantification"

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

The foundational paper connecting nominal reference properties (mass/count/plural) to aspectual properties (telic/atelic) via thematic role homomorphisms. This module builds on the polymorphic mereological infrastructure in Mereology.lean and the thematic role properties in Krifka1998.lean to provide:

1. Nominal reference instantiation: mass nouns = CUM, count nouns = QUA, bare plurals = AlgClosure (§1)
2. QMOD bridge theorems: QMOD + extensive measure → QUA (§2)
3. Temporal adverbials via QMOD: "V for δ" as a QMOD instance (§3)
4. Unified telicity transfer chain: the full @cite{krifka-1989} story connecting nominal reference → VP aspect (§4)
5. Bridge to Scontras's measurement framework (§5)
6. GRAD Square Instantiation: canonical GRADSquare for the Krifka event structure (§6)

@[reducible, inline]

abbrev Semantics.Events.Krifka1989.MassNoun {α : Type u_1} [SemilatticeSup α] (P : α → Prop) : Prop

Mass nouns have cumulative reference: water ⊕ water = water. @cite{krifka-1989} §2: mass nouns denote predicates satisfying CUM.

Equations

• Semantics.Events.Krifka1989.MassNoun P = Mereology.CUM P

@[reducible, inline]

abbrev Semantics.Events.Krifka1989.CountNoun {α : Type u_1} [PartialOrder α] (P : α → Prop) : Prop

Count nouns have quantized reference: no proper part of a cat is a cat. @cite{krifka-1989} §2: count nouns denote predicates satisfying QUA.

Equations

• Semantics.Events.Krifka1989.CountNoun P = Mereology.QUA P

@[reducible, inline]

abbrev Semantics.Events.Krifka1989.BarePlural {α : Type u_1} [SemilatticeSup α] (P : α → Prop) : α → Prop

Bare plurals are algebraic closures: *CAT = the closure of CAT under ⊕. @cite{krifka-1989} §2: bare plurals denote *P, the smallest superset of P closed under sum formation.

Equations

• Semantics.Events.Krifka1989.BarePlural P = Mereology.AlgClosure P

theorem Semantics.Events.Krifka1989.barePlural_cum {α : Type u_1} [SemilatticeSup α] {P : α → Prop} : Mereology.CUM (BarePlural P)

Bare plurals are cumulative (reuses algClosure_cum from Mereology).

theorem Semantics.Events.Krifka1989.qmod_qua {α : Type u_1} [SemilatticeSup α] {R : α → Prop} {μ : α → ℚ} [hμ : Mereology.ExtMeasure α μ] {n : ℚ} (hn : 0 < n) : Mereology.QUA (Mereology.QMOD R μ n)

QMOD produces QUA predicates when μ is extensive and n > 0. @cite{krifka-1989} §2: "three kilos of rice" is QUA because no proper part of a 3kg entity also weighs 3kg (extensivity of weight). Chains to extMeasure_qua from Krifka1998.

theorem Semantics.Events.Krifka1989.qmod_of_cum_is_qua {α : Type u_1} [SemilatticeSup α] {R : α → Prop} (_hCum : Mereology.CUM R) {μ : α → ℚ} [Mereology.ExtMeasure α μ] {n : ℚ} (hn : 0 < n) : Mereology.QUA (Mereology.QMOD R μ n)

The full @cite{krifka-1989} quantizing story: a CUM mass noun combined with QMOD (via an extensive measure) yields a QUA measure phrase. "rice" is CUM → "three kilos of rice" = QMOD(rice, μ_kg, 3) is QUA.

def Semantics.Events.Krifka1989.durationMeasure {Time : Type u_3} [LinearOrder Time] (len : Core.Time.Interval Time → ℚ) : Ev Time → ℚ

Duration measure: maps events to the length of their runtime. This is a wrapper around τ (runtime extraction) composed with an interval-length function. @cite{krifka-1989}: temporal adverbials modify via QMOD on duration.

Equations

• Semantics.Events.Krifka1989.durationMeasure len e = len e.runtime

theorem Semantics.Events.Krifka1989.forAdverbial_subsumes_qmod {Time : Type u_3} [LinearOrder Time] [SemilatticeSup (Ev Time)] {V : Ev Time → Prop} {len : Core.Time.Interval Time → ℚ} {dur : Core.Time.Interval Time} {e : Ev Time} (h : StratifiedReference.forAdverbialMeaning V dur e) : Mereology.QMOD V (durationMeasure len) (len dur) e

"V for δ" as QMOD: the for-adverbial restricts VP events to those whose duration equals δ. This connects @cite{krifka-1989}'s QMOD analysis to @cite{champollion-2017}'s forAdverbialMeaning.

Krifka: "run for an hour" = QMOD(run, duration, 1hr) Champollion: "run for δ" = λe. run(e) ∧ τ(e) = δ ∧ SSR(run)(e)

The QMOD analysis captures the duration constraint; Champollion adds the SSR requirement for felicity. The two are complementary: QMOD explains why the resulting VP is QUA (telic-like bounded), while SSR explains why the base predicate must be atelic.

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

CUM transfer (atelic): CumTheta + CUM noun → CUM VP. "eat apples" yields a CUM (atelic) VP because:

1. APPLES (bare plural) is CUM (barePlural_cum)
2. EAT has a CumTheta incremental theme (follows from SINC in CEM)
3. CumTheta + CUM(OBJ) → CUM(VP) (sinc_cum_propagation)

CUM is Krifka's mereological characterization of atelicity: the VP has cumulative reference, so no natural endpoint. The connection to VendlerClass goes via vendlerClass_atelic_implies_cum_intent in Mereology.lean: atelic classes (states, activities) have CUM.

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

QUA transfer (telic): QUA noun + SINC + UP verb → QUA VP. "eat two apples" yields a QUA (telic) VP because:

1. TWO-APPLES is QUA (count noun + numeral → quantized)
2. EAT has a SINC incremental theme with UP
3. SINC + UP + QUA(OBJ) → QUA(VP) (qua_propagation_sinc)

QUA is Krifka's mereological characterization of telicity: the VP has quantized reference, so it has a natural endpoint. The connection to VendlerClass goes via vendlerClass_telic_implies_qua_intent in Mereology.lean: telic classes (achievements, accomplishments) have QUA.

theorem Semantics.Events.Krifka1989.measure_phrase_makes_qua {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {R : α → Prop} (_hCum : Mereology.CUM R) {μ : α → ℚ} [Mereology.ExtMeasure α μ] {n : ℚ} (hn : 0 < n) {θ : α → β → Prop} (hUP : Krifka1998.UP θ) (hSinc : Krifka1998.SINC θ) : Mereology.QUA (Krifka1998.VP θ (Mereology.QMOD R μ n))

The full @cite{krifka-1989} measure phrase story: QMOD(mass_noun, extensive_μ, n)

• SINC verb → QUA VP (telic).

"eat three kilos of rice" yields a QUA VP because:

1. RICE is CUM (mass noun)
2. "three kilos of rice" = QMOD(rice, μ_kg, 3) is QUA (qmod_of_cum_is_qua)
3. EAT has a SINC incremental theme with UP
4. SINC + UP + QUA(QMOD) → QUA(VP) (qua_propagation_sinc)

This is the central result of @cite{krifka-1989}: measure phrases turn mass nouns into quantized predicates, and quantization propagates through strictly incremental verbs to yield telic (QUA) VPs.

Scontras vs. Krifka: different properties, different predicates

@cite{scontras-2014}'s QU (quantity-uniform) applies to the base predicate: QU_μ(rice) says that rice-quantities of the same μ-measure can be summed.

@cite{krifka-1989}'s QUA applies to the modified predicate: QUA("three kilos of rice") says no proper part of a 3kg-of-rice entity is also 3kg-of-rice.

These are complementary: QU is a precondition on the base noun for measure modification to be felicitous, while QUA is a consequence of the modification that drives telicity transfer. The bridge between them: when MeasureFn is extensive, QMOD produces QUA predicates, which is exactly the quantizing effect that Krifka's telicity transfer chain requires.

def Semantics.Events.Krifka1989.MeasureFn.IsExtensive {E : Type u_3} [SemilatticeSup E] (μ : Probabilistic.Measurement.MeasureFn E) : Prop

A MeasureFn is extensive (in Krifka's sense) when its underlying function satisfies ExtMeasure: additivity over non-overlapping entities and positivity. This bridges Scontras's measurement framework to Krifka's mereological telicity machinery.

Equations

• Semantics.Events.Krifka1989.MeasureFn.IsExtensive μ = Mereology.ExtMeasure E μ.apply

theorem Semantics.Events.Krifka1989.measureTerm_default_applyNumeral_eq {E : Type u_3} (μ : Probabilistic.Measurement.MeasureFn E) (n : ℚ) (x : E) : { measureFn := μ }.applyNumeral n x = (μ.apply x == n)

When a measure term uses the default exact relation (= n), applyNumeral n checks μ(x) == n. This is the Boolean analog of Krifka's QMOD. Stated for the default-rel constructor to ensure definitional equality.

theorem Semantics.Events.Krifka1989.extensive_measureFn_qmod_qua {E : Type u_3} [inst : SemilatticeSup E] {μ : Probabilistic.Measurement.MeasureFn E} (hExt : MeasureFn.IsExtensive μ) {R : E → Prop} {n : ℚ} (hn : 0 < n) : Mereology.QUA (Mereology.QMOD R μ.apply n)

When a MeasureFn is extensive (in Krifka's sense), QMOD with that measure function at any positive value produces a QUA predicate. This bridges Scontras's MeasureFn to Krifka's telicity machinery.

theorem Semantics.Events.Krifka1989.durationMeasure_eq_comp {Time : Type u_3} [LinearOrder Time] (len : Core.Time.Interval Time → ℚ) : durationMeasure len = len ∘ fun (e : Ev Time) => e.runtime

durationMeasure len = len ∘ (fun e => e.runtime) by definition.

def Semantics.Events.Krifka1989.krifkaGRADSquare {Entity : Type u_3} {Time : Type u_4} [SemilatticeSup Entity] [LinearOrder Time] [SemilatticeSup (Ev Time)] (θ : Entity → Ev Time → Prop) (μ_obj : Entity → ℚ) (len : Core.Time.Interval Time → ℚ) (hSinc : Krifka1998.SINC θ) (hObjExt : Mereology.ExtMeasure Entity μ_obj) (hEvExt : Mereology.ExtMeasure (Ev Time) (durationMeasure len)) (hProp : Mereology.MeasureProportional θ μ_obj (durationMeasure len)) : Krifka1998.GRADSquare θ μ_obj (fun (e : Ev Time) => e.runtime) len

Constructor for the GRAD square in the Krifka event structure case: Entity →θ Ev Time →runtime Interval Time →len ℚ.

Equations

• Semantics.Events.Krifka1989.krifkaGRADSquare θ μ_obj len hSinc hObjExt hEvExt hProp = { laxComm := hProp, ext₁ := hObjExt, ext₂ := hEvExt, sinc := hSinc }

theorem Semantics.Events.Krifka1989.krifka_lax_commutativity {Entity : Type u_3} {Time : Type u_4} [SemilatticeSup Entity] [LinearOrder Time] [SemilatticeSup (Ev Time)] {θ : Entity → Ev Time → Prop} {μ_obj : Entity → ℚ} {len : Core.Time.Interval Time → ℚ} (sq : Krifka1998.GRADSquare θ μ_obj (fun (e : Ev Time) => e.runtime) len) {x : Entity} {e : Ev Time} (hθ : θ x e) : len e.runtime = sq.laxComm.rate * μ_obj x

Named lax commutativity for the canonical case: len(e.runtime) = rate * μ_obj(x) for θ-pairs.