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

K89's algebraic semantics tying nominal-reference properties (CUM/QUA via §3 mass/count/bare-plural) to verbal aspect (CUM/QUA on VPs via §4 thematic-relation properties + §5 temporal-trace homomorphisms). A schema-level study: each section either records data (NP/verb/reading items with enumerated source kinds) or calls a propositional theorem on abstract domains.

Main definitions

• NPDatum + k89NPData — 15 NPs from K89 §3 (mass/count/measure/definite)
• qmod_qua / qmod_of_cum_is_qua / measure_phrase_makes_qua — K89 §2-§3 measure-phrase substrate (T6 + D28; inlined from former Events/MeasurePhrases.lean)
• K89ThematicClass + K89ThematicDatum + k89Table14 — K89 §4 eq. 14 verbs (write/eat/read/touch/see) with feature profiles {SUM, GRAD, UNI-E}
• ATM + qua_implies_atm — K89 D17/D18/T4 atomicity (§5 in-X licensing)
• K89ThematicClass.toVerbIncClass — K89 → K98 refinement bridge
• K89QuantDatum + k89Section7Data — K89 §7 quantification data items

TODO

• K89 GRAD propositional chain: SINC + ExtMeasure + MeasureProportional → GRAD was deleted in 0.231.55 (formerly in Events/GradualChange.lean, zero-consumer). Bool-tag proxy predictsGRAD survives in Studies/Krifka1998.lean § 7. Future K89 §4 propositional-faithfulness pass needs to rebuild.
• K89↔Champollion forAdverbial_subsumes_qmod bridge: also dropped in 0.231.55 as dead. ~5 LOC over forAdverbialMeaning + QMOD to re-derive when a Champollion replication wants the cross-framework bridge.
• K89 §7 quantification (max/MXE/MXT/cumulative-distributive derivations): registered as data here; full formalization left to a successor file naturally clustering with Plurals/Quantification.
• GRAD collapse caveat (§ 4): ThematicProfile collapses K89's 5-tuple {SUM, UNI-O, UNI-E, MAP-O, MAP-E} to 3-tuple {SUM, GRAD, UNI-E}. K89 D35 has GRAD ↔ UNI-O ∧ MAP-O ∧ MAP-E. K89 T11/T12 use UNI-O and MAP-O individually; the unbundled form is needed there.
• Atomicity-without-quantization witness: § 5 explains that Ann drank wine in 0.43 seconds is ATM-but-not-QUA, but the substrate witness requires event-CEM atom infrastructure beyond this file's scope.

What this file is NOT

• Not a verb-classification study (that's Studies/Krifka1998.lean's VerbIncClass; the K89 → K98 refinement bridge in § 4 makes the connection explicit).
• Not a for-X / in-X diagnostic study (that's Phenomena/TenseAspect/Diagnostics.lean).
• Not a critique of K89's binary CUM/QUA (that's Studies/Filip2012.lean, which proves the three-way classification's middle ground stable).

References

• @cite{krifka-1989} (primary, anchor for this file)
• Sister: Studies/Krifka1998.lean (K98, same-author 9-years-later refinement; covers both §3 incrementality and §4 motion); Studies/Filip2012.lean (three-way classification critique).

K89 measure-phrase substrate (inlined from Events/MeasurePhrases.lean in 0.231.55)

theorem 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).

theorem 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)

A CUM mass noun combined with QMOD (via an extensive measure) yields a QUA measure phrase. @cite{krifka-1989} §3 D28.

theorem 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} [Semantics.Aspect.Incremental.IsSincVerb θ] : Mereology.QUA (Semantics.Aspect.Cumulativity.VP θ (Mereology.QMOD R μ n))

K89 measure-phrase chain: QMOD(mass_noun, extensive_μ, n) + [IsSincVerb θ] → QUA VP (telic). Central K89 result: measure phrases turn mass nouns into quantized predicates, and quantization propagates through strictly incremental verbs to yield telic VPs.

Nominal Reference Classification (K89 §3)

inductive Krifka1989.NPRefSource : Type

Why an NP has the reference type it does, per @cite{krifka-1989} §3. Each constructor names the structural source of CUM or QUA reference. Replaces a free-form String justification field with an enumerated typology so per-source consistency can be checked.

Note: §7 proportional quantifiers (most girls, less than three girls) are intentionally NOT a constructor here. K89 §7 gives them maximal-event semantics (D44 MXT, D45 MXE, D46 max), not §3 CUM/QUA classification. They live in K89QuantDatum (§6) as sentence-level data without a §3 reference type.

• massNoun : NPRefSource
• barePlural : NPRefSource
• countNumeral : NPRefSource
• measurePhrase : NPRefSource
• definite : NPRefSource
• singularCount : NPRefSource

@[implicit_reducible]

instance Krifka1989.instDecidableEqNPRefSource : DecidableEq NPRefSource

Equations

• Krifka1989.instDecidableEqNPRefSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka1989.instReprNPRefSource.repr : NPRefSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka1989.instReprNPRefSource : Repr NPRefSource

Equations

• Krifka1989.instReprNPRefSource = { reprPrec := Krifka1989.instReprNPRefSource.repr }

def Krifka1989.NPRefSource.expectedRef : NPRefSource → Core.Scale.MereoTag

The structural source uniquely determines CUM vs QUA per K89 §3. Mass nouns and bare plurals are CUM; count, measured, definite NPs are QUA.

Equations

• Krifka1989.NPRefSource.massNoun.expectedRef = Core.Scale.MereoTag.cum
• Krifka1989.NPRefSource.barePlural.expectedRef = Core.Scale.MereoTag.cum
• Krifka1989.NPRefSource.countNumeral.expectedRef = Core.Scale.MereoTag.qua
• Krifka1989.NPRefSource.measurePhrase.expectedRef = Core.Scale.MereoTag.qua
• Krifka1989.NPRefSource.definite.expectedRef = Core.Scale.MereoTag.qua
• Krifka1989.NPRefSource.singularCount.expectedRef = Core.Scale.MereoTag.qua

structure Krifka1989.NPDatum : Type

An NP datum: English form, mereological reference tag, structural source. The source field justifies the refType per K89 §3, and all_nps_consistent_with_source verifies they agree.

• np : String
• refType : Core.Scale.MereoTag
• source : NPRefSource

@[implicit_reducible]

instance Krifka1989.instReprNPDatum : Repr NPDatum

Equations

• Krifka1989.instReprNPDatum = { reprPrec := Krifka1989.instReprNPDatum.repr }

def Krifka1989.instReprNPDatum.repr : NPDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka1989.instBEqNPDatum : BEq NPDatum

Equations

• Krifka1989.instBEqNPDatum = { beq := Krifka1989.instBEqNPDatum.beq }

def Krifka1989.instBEqNPDatum.beq : NPDatum → NPDatum → Bool

Equations

• Krifka1989.instBEqNPDatum.beq { np := a, refType := a_1, source := a_2 } { np := b, refType := b_1, source := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Krifka1989.instBEqNPDatum.beq x✝¹ x✝ = false

def Krifka1989.applesNP : NPDatum

"apples" — bare plural, CUM via algebraic closure.

Equations

• Krifka1989.applesNP = { np := "apples", refType := Core.Scale.MereoTag.cum, source := Krifka1989.NPRefSource.barePlural }

def Krifka1989.twoApplesNP : NPDatum

"two apples" — count noun + numeral, QUA.

Equations

• Krifka1989.twoApplesNP = { np := "two apples", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.countNumeral }

def Krifka1989.waterNP : NPDatum

"water" — mass noun, CUM.

Equations

• Krifka1989.waterNP = { np := "water", refType := Core.Scale.MereoTag.cum, source := Krifka1989.NPRefSource.massNoun }

def Krifka1989.threeKilosWaterNP : NPDatum

"three kilos of water" — QMOD on extensive measure, QUA. K89 §3 D28.

Equations

• Krifka1989.threeKilosWaterNP = { np := "three kilos of water", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.measurePhrase }

def Krifka1989.aHouseNP : NPDatum

"a house" — singular count noun, QUA.

Equations

• Krifka1989.aHouseNP = { np := "a house", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.singularCount }

def Krifka1989.housesNP : NPDatum

"houses" — bare plural, CUM.

Equations

• Krifka1989.housesNP = { np := "houses", refType := Core.Scale.MereoTag.cum, source := Krifka1989.NPRefSource.barePlural }

def Krifka1989.riceNP : NPDatum

"rice" — mass noun, CUM. K89 §3 paradigm example.

Equations

• Krifka1989.riceNP = { np := "rice", refType := Core.Scale.MereoTag.cum, source := Krifka1989.NPRefSource.massNoun }

def Krifka1989.theCartNP : NPDatum

"the cart" — singular count noun + definite, QUA via singular reference.

Equations

• Krifka1989.theCartNP = { np := "the cart", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.singularCount }

K89 §4 table 14 NP exemplars (eq. 14, p. 96): NPs that pair with the five thematic-class verbs.

def Krifka1989.aLetterNP : NPDatum

"a letter" — singular count, QUA. K89 (12-13), §4 table example.

Equations

• Krifka1989.aLetterNP = { np := "a letter", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.singularCount }

def Krifka1989.anAppleNP : NPDatum

"an apple" — singular count, QUA. K89 (14), gradual-consumed-patient row (eat an apple).

Equations

• Krifka1989.anAppleNP = { np := "an apple", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.singularCount }

def Krifka1989.aCatNP : NPDatum

"a cat" — singular count, QUA. K89 (14), affected-patient row (touch a cat).

Equations

• Krifka1989.aCatNP = { np := "a cat", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.singularCount }

def Krifka1989.aHorseNP : NPDatum

"a horse" — singular count, QUA. K89 (14), stimulus row (see a horse).

Equations

• Krifka1989.aHorseNP = { np := "a horse", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.singularCount }

K89 §5 NP exemplars (eq. 19, p. 99): the wine pair used to argue atomicity ≠ quantization.

def Krifka1989.wineNP : NPDatum

"wine" — mass noun, CUM. K89 §5 (drink wine). The §5 punchline Ann drank wine in 0.43 seconds shows that the in-X licensing condition is ATM (atomicity), not QUA — see §5 below.

Equations

• Krifka1989.wineNP = { np := "wine", refType := Core.Scale.MereoTag.cum, source := Krifka1989.NPRefSource.massNoun }

def Krifka1989.aGlassOfWineNP : NPDatum

"a glass of wine" — measure construction, QUA. K89 §5 contrast partner to wine.

Equations

• Krifka1989.aGlassOfWineNP = { np := "a glass of wine", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.measurePhrase }

def Krifka1989.sevenApplesNP : NPDatum

"seven apples" — count + numeral, QUA. K89 §7 cumulative-reading object NP (two girls ate seven apples, eq. 37).

Equations

• Krifka1989.sevenApplesNP = { np := "seven apples", refType := Core.Scale.MereoTag.qua, source := Krifka1989.NPRefSource.countNumeral }

def Krifka1989.k89NPData : List NPDatum

All NP data items registered by §3 classification. Excludes K89 §7 proportional quantifiers (those live in §6 K89QuantDatum data).

Equations

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

theorem Krifka1989.all_nps_consistent_with_source : (k89NPData.all fun (d : NPDatum) => d.source.expectedRef == d.refType) = true

Each NP's refType matches its structural source per K89 §3. Catches typos and mis-classifications when the data list grows.

Grounding in K89 Theory's propositional predicates

These theorems exercise the K89 theory file's propositional predicates on abstract domains, providing the bridge from the file-level Bool-tag classification (MereoTag.cum/.qua) to K89's algebraic content (CUM/QUA on α → Prop). The pattern: the applesNP.refType = .cum claim is a Bool tag; the corresponding propositional claim is CUM (BarePlural P) for any apples-like P, and that follows from barePlural_cum in K89 theory.

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

Bare-plural NPs are cumulative — citation of barePlural_cum from Theories/Semantics/Events/Krifka1989.lean. K89 §3 derives this from algebraic closure (*P closed under sum).

theorem Krifka1989.massNoun_grounded {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (h : Mereology.CUM P) : Semantics.Plurality.MassCount.MassNoun P

Mass nouns are cumulative by definition (K89 §3, abbrev MassNoun = CUM in K89 theory).

theorem Krifka1989.countNoun_grounded {α : Type u_1} [PartialOrder α] {P : α → Prop} (h : Mereology.QUA P) : Semantics.Plurality.MassCount.CountNoun P

Count nouns are quantized by definition (K89 §3, abbrev CountNoun = QUA in K89 theory).

Measure phrases — exercise qmod / measure_phrase_makes_qua

K89 §3 derives that measure phrases like three kilos of rice are quantized via D28 (QMOD, §3 p. 82) and the upstream T6 (extensive measure → quantized, §2 p. 80). These theorems CALL the K89 theory file's qmod_of_cum_is_qua and measure_phrase_makes_qua on an abstract [ExtMeasure α μ] instance — the docstring promise the previous file's measure_phrase_qua (which was just ⟨rfl, rfl⟩ on stipulated fields) failed to honor.

theorem Krifka1989.threeKilosRice_qua_via_qmod {α : Type u_1} [SemilatticeSup α] {Rice : α → Prop} (hRice : Mereology.CUM Rice) {μ : α → ℚ} [Mereology.ExtMeasure α μ] : Mereology.QUA (Mereology.QMOD Rice μ 3)

Three kilos of rice is QUA: a CUM mass noun + an extensive measure

• a positive value yields a quantized predicate. Direct call to qmod_of_cum_is_qua (K89 theory §2).

theorem Krifka1989.eatThreeKilosRice_qua_vp {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {Rice : α → Prop} (hRice : Mereology.CUM Rice) {μ : α → ℚ} [Mereology.ExtMeasure α μ] {θ : α → β → Prop} [Semantics.Aspect.Incremental.IsSincVerb θ] : Mereology.QUA (Semantics.Aspect.Cumulativity.VP θ (Mereology.QMOD Rice μ 3))

Eat three kilos of rice is QUA: K89's full chain — CUM noun + QMOD via extensive measure → QUA NP, then [IsSincVerb θ] propagates QUA to the VP. Direct call to measure_phrase_makes_qua (K89 theory §4, typeclass-canonical form).

K89 §4 thematic-relation features (eq. 14, p. 96)

K89 §4 (eq. 14, p. 96) classifies thematic relations by a feature profile {SUM, UNI-O, UNI-E, MAP-O, MAP-E}, with GRAD = UNI-O ∧ MAP-O ∧ MAP-E (D35). The five rows of K89's table:

| example         | SUM | GRAD | UNI-E | label                    |
|-----------------|-----|------|-------|--------------------------|
| write a letter  |  X  |  X   |  X    | gradual effected patient |
| eat an apple    |  X  |  X   |  X    | gradual consumed patient |
| read a letter   |  X  |  X   |  -    | gradual patient          |
| touch a cat     |  X  |  -   |  -    | affected patient         |
| see a horse     |  X  |  -   |  -    | stimulus                 |

These five labels are K89's thematic-relation classes. The
propositional predicates (SUM, UP, MO, MSO, MSE, UE, UO, GUE) are
K89 D29-D35 (§4, pp. 92-96) and live in
`Theories/Semantics/Events/Krifka1998.lean` for organizational
reasons. Below, each class is captured as a Bool feature profile;
a successor study could instantiate the propositional predicates
on concrete θ relations.

**GRAD collapse caveat.** The `ThematicProfile` collapses K89's
5-tuple {SUM, UNI-O, UNI-E, MAP-O, MAP-E} to 3-tuple {SUM, GRAD,
UNI-E}. K89 D35 defines GRAD ↔ UNI-O ∧ MAP-O ∧ MAP-E, and all five
table-14 verbs happen to align on UNI-O/MAP-O/MAP-E (they co-vary).
But K89 T11 (p. 95) and T12 use UNI-O and MAP-O *individually* as
antecedent conditions (not bundled as GRAD). A future formalization
of T11/T12 will need the unbundled version. 

inductive Krifka1989.K89ThematicClass : Type

• gradualEffectedPatient : K89ThematicClass
• gradualConsumedPatient : K89ThematicClass
• gradualPatient : K89ThematicClass
• affectedPatient : K89ThematicClass
• stimulus : K89ThematicClass

@[implicit_reducible]

instance Krifka1989.instDecidableEqK89ThematicClass : DecidableEq K89ThematicClass

Equations

• Krifka1989.instDecidableEqK89ThematicClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka1989.instReprK89ThematicClass.repr : K89ThematicClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka1989.instReprK89ThematicClass : Repr K89ThematicClass

Equations

• Krifka1989.instReprK89ThematicClass = { reprPrec := Krifka1989.instReprK89ThematicClass.repr }

structure Krifka1989.ThematicProfile : Type

Bool-tag profile of K89 §4 features. hasGRAD abbreviates hasUNI_O ∧ hasMAP_O ∧ hasMAP_E (K89 D35), faithful for table 14 rows where the three components co-vary; see the docstring caveat above.

• hasSUM : Bool
• hasGRAD : Bool
• hasUNI_E : Bool

def Krifka1989.instReprThematicProfile.repr : ThematicProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka1989.instReprThematicProfile : Repr ThematicProfile

Equations

• Krifka1989.instReprThematicProfile = { reprPrec := Krifka1989.instReprThematicProfile.repr }

@[implicit_reducible]

instance Krifka1989.instDecidableEqThematicProfile : DecidableEq ThematicProfile

Equations

• Krifka1989.instDecidableEqThematicProfile = Krifka1989.instDecidableEqThematicProfile.decEq

def Krifka1989.instDecidableEqThematicProfile.decEq (x✝ x✝¹ : ThematicProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Krifka1989.K89ThematicClass.profile : K89ThematicClass → ThematicProfile

K89 §4 table-14 feature profiles.

Equations

• Krifka1989.K89ThematicClass.gradualEffectedPatient.profile = { hasSUM := true, hasGRAD := true, hasUNI_E := true }
• Krifka1989.K89ThematicClass.gradualConsumedPatient.profile = { hasSUM := true, hasGRAD := true, hasUNI_E := true }
• Krifka1989.K89ThematicClass.gradualPatient.profile = { hasSUM := true, hasGRAD := true, hasUNI_E := false }
• Krifka1989.K89ThematicClass.affectedPatient.profile = { hasSUM := true, hasGRAD := false, hasUNI_E := false }
• Krifka1989.K89ThematicClass.stimulus.profile = { hasSUM := true, hasGRAD := false, hasUNI_E := false }

inductive Krifka1989.K89Verb : Type

The five K89 (1989) §4 verbs forming K89's table-14 classification. Used to derive verb strings in K89ThematicDatum.vp instead of storing the English form as a free String.

• write : K89Verb
• eat : K89Verb
• read : K89Verb
• touch : K89Verb
• see : K89Verb

@[implicit_reducible]

instance Krifka1989.instDecidableEqK89Verb : DecidableEq K89Verb

Equations

• Krifka1989.instDecidableEqK89Verb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Krifka1989.instReprK89Verb : Repr K89Verb

Equations

• Krifka1989.instReprK89Verb = { reprPrec := Krifka1989.instReprK89Verb.repr }

def Krifka1989.instReprK89Verb.repr : K89Verb → ℕ → Std.Format

Equations

• Krifka1989.instReprK89Verb.repr Krifka1989.K89Verb.write prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1989.K89Verb.write")).group prec✝
• Krifka1989.instReprK89Verb.repr Krifka1989.K89Verb.eat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1989.K89Verb.eat")).group prec✝
• Krifka1989.instReprK89Verb.repr Krifka1989.K89Verb.read prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1989.K89Verb.read")).group prec✝
• Krifka1989.instReprK89Verb.repr Krifka1989.K89Verb.touch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1989.K89Verb.touch")).group prec✝
• Krifka1989.instReprK89Verb.repr Krifka1989.K89Verb.see prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1989.K89Verb.see")).group prec✝

def Krifka1989.K89Verb.lemma : K89Verb → String

English lemma for each K89 §4 verb.

Equations

• Krifka1989.K89Verb.write.lemma = "write"
• Krifka1989.K89Verb.eat.lemma = "eat"
• Krifka1989.K89Verb.read.lemma = "read"
• Krifka1989.K89Verb.touch.lemma = "touch"
• Krifka1989.K89Verb.see.lemma = "see"

structure Krifka1989.K89ThematicDatum : Type

A K89 §4 verb-NP datum: the verb (enumerated), the thematic class K89 assigns it, and the NP it pairs with in K89's exemplars. The English vp string is derived from verb.lemma and npDatum.np rather than stored separately — making typos impossible.

• verb : K89Verb
• thematicClass : K89ThematicClass
• npDatum : NPDatum

@[implicit_reducible]

instance Krifka1989.instReprK89ThematicDatum : Repr K89ThematicDatum

Equations

• Krifka1989.instReprK89ThematicDatum = { reprPrec := Krifka1989.instReprK89ThematicDatum.repr }

def Krifka1989.instReprK89ThematicDatum.repr : K89ThematicDatum → ℕ → Std.Format

Equations

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

def Krifka1989.K89ThematicDatum.vp (d : K89ThematicDatum) : String

The English VP, derived from the verb lemma and NP.

Equations

• d.vp = d.verb.lemma ++ " " ++ d.npDatum.np

def Krifka1989.writeALetter : K89ThematicDatum

Equations

• Krifka1989.writeALetter = { verb := Krifka1989.K89Verb.write, thematicClass := Krifka1989.K89ThematicClass.gradualEffectedPatient, npDatum := Krifka1989.aLetterNP }

def Krifka1989.eatAnApple : K89ThematicDatum

Equations

• Krifka1989.eatAnApple = { verb := Krifka1989.K89Verb.eat, thematicClass := Krifka1989.K89ThematicClass.gradualConsumedPatient, npDatum := Krifka1989.anAppleNP }

def Krifka1989.readALetter : K89ThematicDatum

Equations

• Krifka1989.readALetter = { verb := Krifka1989.K89Verb.read, thematicClass := Krifka1989.K89ThematicClass.gradualPatient, npDatum := Krifka1989.aLetterNP }

def Krifka1989.touchACat : K89ThematicDatum

Equations

• Krifka1989.touchACat = { verb := Krifka1989.K89Verb.touch, thematicClass := Krifka1989.K89ThematicClass.affectedPatient, npDatum := Krifka1989.aCatNP }

def Krifka1989.seeAHorse : K89ThematicDatum

Equations

• Krifka1989.seeAHorse = { verb := Krifka1989.K89Verb.see, thematicClass := Krifka1989.K89ThematicClass.stimulus, npDatum := Krifka1989.aHorseNP }

def Krifka1989.k89Table14 : List K89ThematicDatum

Equations

• Krifka1989.k89Table14 = [Krifka1989.writeALetter, Krifka1989.eatAnApple, Krifka1989.readALetter, Krifka1989.touchACat, Krifka1989.seeAHorse]

theorem Krifka1989.k89Table14_vps : writeALetter.vp = "write a letter" ∧ eatAnApple.vp = "eat an apple" ∧ readALetter.vp = "read a letter" ∧ touchACat.vp = "touch a cat" ∧ seeAHorse.vp = "see a horse"

Derived VPs match the expected English exemplars from K89 (14).

theorem Krifka1989.all_classes_have_sum : (k89Table14.all fun (d : K89ThematicDatum) => d.thematicClass.profile.hasSUM) = true

Every K89 thematic class has SUM (cumulativity for thematic relations); K89 §4 treats SUM as the foundational property of thematic roles.

theorem Krifka1989.gradual_classes_have_grad : K89ThematicClass.gradualEffectedPatient.profile.hasGRAD = true ∧ K89ThematicClass.gradualConsumedPatient.profile.hasGRAD = true ∧ K89ThematicClass.gradualPatient.profile.hasGRAD = true

Gradual classes (effected, consumed, plain) all have GRAD; affected and stimulus do not. K89 §4 distinction.

theorem Krifka1989.nongradual_classes_lack_grad : K89ThematicClass.affectedPatient.profile.hasGRAD = false ∧ K89ThematicClass.stimulus.profile.hasGRAD = false

theorem Krifka1989.uni_e_distinguishes_effected_consumed : K89ThematicClass.gradualEffectedPatient.profile.hasUNI_E = true ∧ K89ThematicClass.gradualConsumedPatient.profile.hasUNI_E = true ∧ K89ThematicClass.gradualPatient.profile.hasUNI_E = false

Effected and consumed patients are distinguished from plain gradual patients by UNI-E (uniqueness of events): each subevent of writing or eating produces a unique consumed/produced sub-object. Read a letter allows the same letter-segment to be read multiple times, so it lacks UNI-E.

K89 → K98 refinement (sister-paper bridge)

K89 (1989) and K98 (*Origins of Telicity*, 1998) are the same
author refining the same theory at two stages. K98's `VerbIncClass`
(`sinc | inc | cumOnly`) is a coarsening of K89's table-14
five-class scheme. The mapping below makes the refinement explicit:
*gradual effected/consumed* → SINC (strict bijection between
object parts and event parts, K98 §3.2 eq. 51), *gradual patient*
(lacking UNI-E) → INC (general incrementality, K98 §3.6, allows
re-reading), *affected patient* and *stimulus* (lacking GRAD) →
cumOnly (no incremental theme, K98 §3.2). 

def Krifka1989.K89ThematicClass.toVerbIncClass : K89ThematicClass → Semantics.Aspect.Incremental.VerbIncClass

Refine K89's 5-class scheme to K98's 3-class enum. K89's 1989 paper distinguishes effected from consumed patients (creation vs. consumption), but they share the SINC profile in K98's coarser classification.

Equations

• Krifka1989.K89ThematicClass.gradualEffectedPatient.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.sinc
• Krifka1989.K89ThematicClass.gradualConsumedPatient.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.sinc
• Krifka1989.K89ThematicClass.gradualPatient.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.inc
• Krifka1989.K89ThematicClass.affectedPatient.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.cumOnly
• Krifka1989.K89ThematicClass.stimulus.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.cumOnly

theorem Krifka1989.toVerbIncClass_respects_grad (cls : K89ThematicClass) : cls.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.sinc ∨ cls.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.inc ↔ cls.profile.hasGRAD = true

The K89 → K98 refinement is consistent with K89's GRAD distinction: SINC verbs all have GRAD (consumption/creation gives bijection); cumOnly verbs all lack GRAD (no theme-event mapping); INC verbs have GRAD without UNI-E (re-reading allowed).

theorem Krifka1989.k89Table14_refines_k98_consistently : (k89Table14.all fun (d : K89ThematicDatum) => decide (d.thematicClass.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.sinc) || decide (d.thematicClass.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.inc) || decide (d.thematicClass.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.cumOnly)) = true

Every K89 verb-NP datum maps to a K98 VerbIncClass consistently.

Atomicity ≠ Quantization (K89 §5 eq. 19; K89 T4)

K89 §5 (around eq. 19, Ann drank wine in 0.43 seconds) makes a crucial point that a surface QUA → in-X / CUM → for-X classification papers over: time-span adverbials require atomicity (ATM), not quantization (QUA). The QUA → ATM direction is K89 T4 (§2 p. 78, listed among "easily checked" theorems); the lifted form for VPs via thematic relations is K89 T13 (§4 p. 95). The reverse (ATM → QUA) does not hold: a predicate can be ATM without being QUA.

Concretely: *Ann drank wine in 0.43 seconds* is acceptable because
the predicate `λ e. drink-wine(e) ∧ τ(e) ≤ 0.43sec` is atomic — no
shorter event is also a 0.43-second wine-drinking — even though
`wine` itself is CUM (mass noun, *not* QUA). The QUA-via-D28 chain
is one route to ATM, not the only route. 

def Krifka1989.AtomicForP {α : Type u_1} [PartialOrder α] (P : α → Prop) (y : α) : Prop

K89 D17: y is a P-atom — y satisfies P and has no proper part also satisfying P. Distinct from Mereology.Atom (which is the absolute no-proper-part predicate, ignoring P): K89's notion is P-relative.

Equations

• Krifka1989.AtomicForP P y = (P y ∧ ∀ z < y, ¬P z)

def Krifka1989.ATM {α : Type u_1} [PartialOrder α] (P : α → Prop) : Prop

K89 D18: ATM(P) — P has atomic reference: every P-instance has a P-atomic part. The licensing condition for time-span (in-X) adverbials per K89 §5.

Equations

• Krifka1989.ATM P = ∀ (x : α), P x → ∃ y ≤ x, Krifka1989.AtomicForP P y

theorem Krifka1989.qua_implies_atm {α : Type u_1} [PartialOrder α] {P : α → Prop} (hQua : Mereology.QUA P) : ATM P

K89 T4 (§2 p. 78, "easily checked"): every quantized predicate is atomic. Witness: any QUA-instance is itself a P-atom (QUA forbids proper P-parts), so it is its own atomic-part witness.

The ATM-but-not-QUA case is genuinely possible — that's this section's point. K89's Ann drank wine in 0.43 seconds shows that a bounded-duration predicate can be ATM (no shorter sub-event is also a 0.43-second wine-drinking) without being QUA on the underlying object NP (wine is CUM). The substrate-witness theorem requires event-CEM atom infrastructure beyond this file's scope; the Ann drank wine exemplar below stands as the linguistic motivation.

def Krifka1989.annDrankWineInSeconds : K89ThematicDatum

Ann drank wine in 0.43 seconds (K89 §5 eq. 19): a CUM-NP VP that accepts in-X. Listed as a thematic datum (K89 §4 eat-class) with the wine NP, flagged as the edge case where ATM and QUA come apart on the object NP.

Equations

• Krifka1989.annDrankWineInSeconds = { verb := Krifka1989.K89Verb.eat, thematicClass := Krifka1989.K89ThematicClass.gradualConsumedPatient, npDatum := Krifka1989.wineNP }

theorem Krifka1989.ann_drank_wine_object_is_cum : annDrankWineInSeconds.npDatum.refType = Core.Scale.MereoTag.cum

The wine NP in Ann drank wine in 0.43 seconds is CUM (mass noun). Without atomicity-not-quantization licensing (K89 §5), the §5 in-X acceptance would be unexplained.

theorem Krifka1989.aGlassOfWine_is_qua : aGlassOfWineNP.refType = Core.Scale.MereoTag.qua

The §5 contrast partner: drink a glass of wine in 0.43 seconds's object IS QUA (measure construction), so the K89 §3 D28 chain handles it via QMOD; the wine bare-mass case in annDrankWineInSeconds is the one that requires the ATM-not-QUA pathway formalized as ATM above.

Quantification (K89 §7)

K89 §7 introduces:

- definite NPs (eq. 35-36) via maximal-individual semantics;
- increasing/decreasing quantifiers (eq. 31-34) via maximal events
  + the `max` function (D46);
- cumulative readings (eq. 37-40) via summative thematic relations;
- distributive readings (eq. 41-42) via the ATP atomic-part operator.

This section registers the data items K89 builds his quantification
analysis on. Full formalization of `max` / MXE / MXT / cumulative-
distributive derivations is left to a successor file (e.g. a
`Phenomena/Quantification/Studies/Krifka1989Quant.lean`); the
chronological anchor is here, but the substrate work-product would
naturally cluster with Plurals/Quantification, where Champollion
2017 already engages cumulative readings. 

inductive Krifka1989.K89Reading : Type

The reading-type of a K89 §7 quantification datum, per the paper's eq. 31-32 (increasing/decreasing) and eq. 37/41-42 (cumulative, distributive).

• increasingProportional : K89Reading
• decreasing : K89Reading
• cumulative : K89Reading
• distributive : K89Reading

@[implicit_reducible]

instance Krifka1989.instDecidableEqK89Reading : DecidableEq K89Reading

Equations

• Krifka1989.instDecidableEqK89Reading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Krifka1989.instReprK89Reading : Repr K89Reading

Equations

• Krifka1989.instReprK89Reading = { reprPrec := Krifka1989.instReprK89Reading.repr }

def Krifka1989.instReprK89Reading.repr : K89Reading → ℕ → Std.Format

Equations

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

def Krifka1989.K89Reading.eqRef : K89Reading → String

Paper-internal reference for each K89 §7 reading.

Equations

• Krifka1989.K89Reading.increasingProportional.eqRef = "K89 §7 eq. 31"
• Krifka1989.K89Reading.decreasing.eqRef = "K89 §7 eq. 32"
• Krifka1989.K89Reading.cumulative.eqRef = "K89 §7 eq. 37"
• Krifka1989.K89Reading.distributive.eqRef = "K89 §7 eq. 42"

structure Krifka1989.K89QuantDatum : Type

A K89 §7 quantification datum: the English sentence + reading kind. Does NOT carry an NPDatum (the proportional/decreasing-quantifier NPs are not §3 CUM/QUA-classified; K89 §7 treats them via maximal-event semantics instead).

• sentence : String
• reading : K89Reading

def Krifka1989.instReprK89QuantDatum.repr : K89QuantDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka1989.instReprK89QuantDatum : Repr K89QuantDatum

Equations

• Krifka1989.instReprK89QuantDatum = { reprPrec := Krifka1989.instReprK89QuantDatum.repr }

def Krifka1989.mostGirlsSang : K89QuantDatum

Equations

• Krifka1989.mostGirlsSang = { sentence := "Most girls sang", reading := Krifka1989.K89Reading.increasingProportional }

def Krifka1989.lessThanThreeGirlsSang : K89QuantDatum

Equations

• Krifka1989.lessThanThreeGirlsSang = { sentence := "Less than three girls sang", reading := Krifka1989.K89Reading.decreasing }

def Krifka1989.twoGirlsAteSevenApples : K89QuantDatum

Equations

• Krifka1989.twoGirlsAteSevenApples = { sentence := "Two girls ate seven apples", reading := Krifka1989.K89Reading.cumulative }

def Krifka1989.twoGirlsAteSevenApplesEach : K89QuantDatum

Equations

• Krifka1989.twoGirlsAteSevenApplesEach = { sentence := "Two girls ate seven apples each", reading := Krifka1989.K89Reading.distributive }

def Krifka1989.k89Section7Data : List K89QuantDatum

Equations

• Krifka1989.k89Section7Data = [Krifka1989.mostGirlsSang, Krifka1989.lessThanThreeGirlsSang, Krifka1989.twoGirlsAteSevenApples, Krifka1989.twoGirlsAteSevenApplesEach]

Scope: predicate-level QUA/CUM ≠ carrier-level boundedness

@cite{krifka-1989} defines QUA and CUM (D 14, D 12, p. 78) as properties of predicates over a structured carrier — a complete join semilattice with a part relation. K89 makes no claim that these predicate-level properties entail bounds on the carrier itself (e.g. that it has Mathlib OrderTop / OrderBot instances).

This matters because downstream linglib code uses
`Core.Scale.MereoTag.qua = .closed` as a lexical-classification tag
that conflates the two levels. That conflation is convenient for
cross-framework gluing across @cite{krifka-1989}, @cite{kennedy-2007},
@cite{rouillard-2026} (see `Core/Scales/MereoDim.lean` for the
structural bridges that DO hold — e.g. `singleton_qua_closed`,
`qua_kennedy_licensed`), but it does not follow from K89's definitions.
The two examples below show the gap in both directions.

The defeasible cross-domain bridge `closed scale → telic verb` for
*degree achievements specifically* is @cite{hay-kennedy-levin-1999}'s
contribution (lengthen, cool, straighten); it is not K89's claim, and
even HKL restrict it to verbs derived from gradable adjectives.