Krifka (1989): Nominal Reference, Temporal Constitution and Quantification in Event Semantics

Krifka relates the reference of nominal predicates to the temporal constitution of verbal predicates. Objects, events and times form join semilattices, and a predicate is cumulative when it is closed under join and quantized when no instance is a proper part of another. Measure phrases and count nouns are quantized because their measure functions are extensive. A thematic relation transfers the reference type of its nominal argument to the verbal predicate: summativity carries cumulativity across, and uniqueness and mapping properties carry quantization across when the relation is not iterative.

Implementation notes

The paper's relations are stated with the library's object-first thematic relations, so its uniqueness of objects is UP, uniqueness of events GUE, mapping to objects MO, mapping to events ME, and summativity SUM. Its part structures satisfy relative complementarity (D 9), which the measure theorems assume as Mereology.HasRemainders. Theorem (T 3) needs a nonempty predicate, since the empty predicate is both quantized and strictly cumulative. The proof of (T 13) shows that every verbal event has a part outside the predicate; its conclusion that the event contains an atom holds when the part order on events is well founded (atm_of_wellFoundedLT). The sections on negation (§6) and quantification (§7) are prose.

References

• [Kri89]
• [Lin83], [Kri98]

Reference types (§2)

def Krifka1989.SNG {α : Type u_1} (P : α → Prop) : Prop

A predicate has singular reference (D 11) if it holds of exactly one element.

Equations

• Krifka1989.SNG P = ∃ (x : α), P x ∧ ∀ (y : α), P y → x = y

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

A predicate has strictly cumulative reference (D 13) if it is cumulative and not singular.

Equations

• Krifka1989.SCUM P = (Mereology.CUM P ∧ ¬Krifka1989.SNG P)

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

A predicate has strictly quantized reference (D 15) if it is quantized and every instance has a proper part.

Equations

• Krifka1989.SQUA P = (Mereology.QUA P ∧ ∀ (x : α), P x → ∃ (y : α), y < x)

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

A predicate has atomic reference (D 18) if every instance has a part that is a P-atom (D 17).

Equations

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

theorem Krifka1989.qua_of_sng {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (h : SNG P) : Mereology.QUA P

Singular predicates are quantized (T 1).

theorem Krifka1989.cum_of_sng {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (h : SNG P) : Mereology.CUM P

Singular predicates are cumulative (T 2).

theorem Krifka1989.not_scum_of_qua {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hne : ∃ (x : α), P x) (h : Mereology.QUA P) : ¬SCUM P

A nonempty quantized predicate is not strictly cumulative (T 3).

theorem Krifka1989.atm_of_qua {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (h : Mereology.QUA P) : ATM P

Quantized reference is atomic (T 4), each instance being its own atom.

theorem Krifka1989.qua_of_isExtensiveMeasure {α : Type u_1} [SemilatticeSup α] [Mereology.HasRemainders α] {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [AddLeftStrictMono M] (μ : α → M) [Mereology.IsExtensiveMeasure μ] (n : M) : Mereology.QUA fun (x : α) => μ x = n

A predicate restricted by an extensive measure function to a value is quantized (T 6), by additivity (D 24), positivity (T 5) and relative complementarity (D 9).

theorem Krifka1989.atm_of_wellFoundedLT {α : Type u_1} [SemilatticeSup α] [WellFoundedLT α] (P : α → Prop) : ATM P

With a well-founded part order every predicate has atomic reference, since the minimal instances below any instance are its atoms.

Nominal predicates (§3)

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

A bare plural is the algebraic closure of the count noun under join, which is cumulative.

theorem Krifka1989.measure_qmod {α : Type u_1} {M : Type u_2} [SemilatticeSup α] [Mereology.HasRemainders α] [AddCommMonoid M] [PartialOrder M] [AddLeftStrictMono M] {P : α → Prop} (hP : Mereology.CUM P) {x y : α} (hx : P x) (hy : P y) (hxy : x ≠ y) (μ : α → M) [Mereology.IsExtensiveMeasure μ] (n : M) : ¬Mereology.QUA P ∧ Mereology.QUA (Mereology.QMOD P μ n)

The measure construction (4) is a quantizing modifier (D 28) on a cumulative noun with two distinct instances, since the noun is not quantized and the measure phrase is. Since its output is quantized, a measure phrase cannot apply to another (3c).

theorem Krifka1989.countNoun_qua {α : Type u_1} {M : Type u_2} [SemilatticeSup α] [Mereology.HasRemainders α] [AddCommMonoid M] [PartialOrder M] [AddLeftStrictMono M] (P : α → Prop) (NU : α → M) [Mereology.IsExtensiveMeasure NU] (n : M) : Mereology.QUA (Mereology.QMOD P NU n)

A count noun (6) is a classifier construction with the natural unit built in, so it denotes the noun's predicate restricted by the natural-unit measure to a number, which is quantized.

Transfer of reference from objects to events (§4)

def Krifka1989.ofTheta {O : Type u_1} {E : Type u_2} (α : E → Prop) (δ : O → Prop) (θ : O → E → Prop) : E → Prop

The verbal predicate (12) conjoins a verb with the verb phrase of a thematic relation and a nominal predicate.

Equations

• Krifka1989.ofTheta α δ θ e = (α e ∧ Aspect.VP θ δ e)

def Krifka1989.ITER {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] (θ : O → E → Prop) (e : E) (x : O) : Prop

An event is iterative on an object (D 34) if some part of the object is subjected to two parts of the event.

Equations

• Krifka1989.ITER θ e x = (θ x e ∧ ∃ (e' : E) (e'' : E) (x' : O), e' ≤ e ∧ e'' ≤ e ∧ e' ≠ e'' ∧ x' ≤ x ∧ θ x' e' ∧ θ x' e'')

def Krifka1989.GRAD {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] (θ : O → E → Prop) : Prop

A relation is gradual (D 35) if it has uniqueness of objects and both mappings.

Equations

• Krifka1989.GRAD θ = (Mereology.UP θ ∧ Mereology.MO θ ∧ Mereology.ME θ)

theorem Krifka1989.cum_ofTheta {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {α : E → Prop} {δ : O → Prop} {θ : O → E → Prop} (hα : Mereology.CUM α) (hδ : Mereology.CUM δ) (hθ : Mereology.SUM θ) : Mereology.CUM (ofTheta α δ θ)

A cumulative verb, a cumulative nominal predicate, and a summative relation give a cumulative verbal predicate (T 7).

theorem Krifka1989.exists_iter {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {α : E → Prop} {δ : O → Prop} {θ : O → E → Prop} (hδ : SNG δ) (hθ : Mereology.SUM θ) (hne : ∃ (e : E), ofTheta α δ θ e) (hs : SCUM (ofTheta α δ θ)) : ∃ (e : E) (x : O), ITER θ e x

A singular nominal predicate, a summative relation, and a strictly cumulative verbal predicate force an iterative event (T 8), since two distinct events with the one object sum to an event subjecting it twice.

theorem Krifka1989.not_scum_of_not_iter {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {α : E → Prop} {δ : O → Prop} {θ : O → E → Prop} (hδ : SNG δ) (hθ : Mereology.SUM θ) (hne : ∃ (e : E), ofTheta α δ θ e) (hi : ∀ (e : E) (x : O), ¬ITER θ e x) : ¬SCUM (ofTheta α δ θ)

Without iteration the verbal predicate of a singular nominal predicate is not strictly cumulative (T 9).

theorem Krifka1989.not_iter_of_gue {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {θ : O → E → Prop} (h : Mereology.GUE θ) (e : E) (x : O) : ¬ITER θ e x

Uniqueness of events excludes iteration (T 10).

theorem Krifka1989.mso_of_not_iter {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {θ : O → E → Prop} (hm : Mereology.MO θ) (hi : ∀ (e : E) (x : O), ¬ITER θ e x) : Mereology.MSO θ

Without iteration, mapping to objects maps proper subevents to proper parts of the object, since the whole object, subjected to a proper subevent, would be subjected to two parts of the event.

theorem Krifka1989.qua_ofTheta {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {α : E → Prop} {δ : O → Prop} {θ : O → E → Prop} (hδ : Mereology.QUA δ) (hu : Mereology.UP θ) (hm : Mereology.MO θ) (hi : ∀ (e : E) (x : O), ¬ITER θ e x) : Mereology.QUA (ofTheta α δ θ)

A quantized nominal predicate transfers quantization to the verbal predicate (T 11) when the relation has uniqueness of objects, mapping to objects, and no iteration.

theorem Krifka1989.qua_ofTheta_of_gue {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {α : E → Prop} {δ : O → Prop} {θ : O → E → Prop} (hδ : Mereology.QUA δ) (hu : Mereology.UP θ) (hm : Mereology.MO θ) (hg : Mereology.GUE θ) : Mereology.QUA (ofTheta α δ θ)

Quantization transfers under uniqueness of events (T 12), as for effected and consumed objects.

theorem Krifka1989.exists_le_not_ofTheta {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {α : E → Prop} {δ : O → Prop} {θ : O → E → Prop} (hδ : SQUA δ) (hm : Mereology.ME θ) (hu : Mereology.UP θ) (e : E) (he : ofTheta α δ θ e) : ∃ e' ≤ e, ¬ofTheta α δ θ e'

With a strictly quantized nominal predicate, mapping to events, and uniqueness of objects, every verbal event has a part outside the verbal predicate, the step of (T 13).

The classification of thematic relations (14)

inductive Krifka1989.ThematicClass : Type

The five classes of (14) are gradual effected patient (write a letter), gradual consumed patient (eat an apple), gradual patient (read a letter), affected patient (touch a cat), and stimulus (see a horse).

• gradualEffectedPatient : ThematicClass
• gradualConsumedPatient : ThematicClass
• gradualPatient : ThematicClass
• affectedPatient : ThematicClass
• stimulus : ThematicClass

@[instance_reducible]

instance Krifka1989.instDecidableEqThematicClass : DecidableEq ThematicClass

Equations

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

@[instance_reducible]

instance Krifka1989.instReprThematicClass : Repr ThematicClass

Equations

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

def Krifka1989.instReprThematicClass.repr : ThematicClass → ℕ → Std.Format

Equations

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

def Krifka1989.ThematicClass.Gradual : ThematicClass → Prop

The gradual classes.

Equations

• Krifka1989.ThematicClass.gradualEffectedPatient.Gradual = True
• Krifka1989.ThematicClass.gradualConsumedPatient.Gradual = True
• Krifka1989.ThematicClass.gradualPatient.Gradual = True
• Krifka1989.ThematicClass.affectedPatient.Gradual = False
• Krifka1989.ThematicClass.stimulus.Gradual = False

def Krifka1989.ThematicClass.UniqueEvents : ThematicClass → Prop

The classes with uniqueness of events.

Equations

• Krifka1989.ThematicClass.gradualEffectedPatient.UniqueEvents = True
• Krifka1989.ThematicClass.gradualConsumedPatient.UniqueEvents = True
• Krifka1989.ThematicClass.gradualPatient.UniqueEvents = False
• Krifka1989.ThematicClass.affectedPatient.UniqueEvents = False
• Krifka1989.ThematicClass.stimulus.UniqueEvents = False

def Krifka1989.ThematicClass.Requires {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] (c : ThematicClass) (θ : O → E → Prop) : Prop

c.Requires θ holds when θ meets what (14) requires of the class c, namely summativity throughout, graduality for the gradual classes, and uniqueness of events for effected and consumed patients.

Equations

• c.Requires θ = (Mereology.SUM θ ∧ (c.Gradual → Krifka1989.GRAD θ) ∧ (c.UniqueEvents → Mereology.GUE θ))

theorem Krifka1989.qua_of_uniqueEvents {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {α : E → Prop} {δ : O → Prop} {θ : O → E → Prop} {c : ThematicClass} (hc : c.UniqueEvents) (h : c.Requires θ) (hδ : Mereology.QUA δ) : Mereology.QUA (ofTheta α δ θ)

Effected and consumed patients make a quantized object into a quantized verbal predicate (T 12), so write a letter and eat an apple are telic.

theorem Krifka1989.gradualPatient_transfer {O : Type u_1} {E : Type u_2} [SemilatticeSup O] [SemilatticeSup E] {α : E → Prop} {δ : O → Prop} {θ : O → E → Prop} (h : ThematicClass.gradualPatient.Requires θ) : (Mereology.CUM α → Mereology.CUM δ → Mereology.CUM (ofTheta α δ θ)) ∧ (SQUA δ → ∀ (e : E), ofTheta α δ θ e → ∃ e' ≤ e, ¬ofTheta α δ θ e')

A gradual patient transfers cumulativity (T 7) and, with a strictly quantized object, leaves every event a part outside the predicate (T 13), the atomicity behind read a letter in an hour even where the letter may be reread.

Temporal adverbials (§5)

theorem Krifka1989.durative_qua {E : Type u_1} {M : Type u_3} [SemilatticeSup E] [Mereology.HasRemainders E] [AddCommMonoid M] [PartialOrder M] [AddLeftStrictMono M] (P : E → Prop) (μ' : E → M) [Mereology.IsExtensiveMeasure μ'] (n : M) : Mereology.QUA (Mereology.QMOD P μ' n)

A durative adverbial (15) is the quantizing modifier on events through the measure of the temporal trace (D 41); the result is quantized once that derived measure is extensive.

def Krifka1989.inSpan {E : Type u_1} {T : Type u_2} {M : Type u_3} [SemilatticeSup T] (P : E → Prop) (τ : E → T) (Conv : T → Prop) (μ : T → M) (n : M) : E → Prop

A time-span adverbial (16) holds of an event that lies within a convex time of the given measure.

Equations

• Krifka1989.inSpan P τ Conv μ n e = (P e ∧ ∃ (t : T), Conv t ∧ μ t = n ∧ τ e ≤ t)

theorem Krifka1989.inSpan_mono {E : Type u_1} {T : Type u_2} {M : Type u_3} [SemilatticeSup T] (P : E → Prop) (τ : E → T) (Conv : T → Prop) (μ : T → M) {n n' : M} (h : ∀ (t : T), Conv t → μ t = n → ∃ (t' : T), Conv t' ∧ μ t' = n' ∧ t ≤ t') (e : E) : inSpan P τ Conv μ n e → inSpan P τ Conv μ n' e

Time-span adverbials are upward entailing in their number (17). If every convex time of one measure lies within a convex time of a larger measure, the adverbial with the larger number holds of every event the smaller one holds of.