Krejci (2012): Causativization as Antireflexivization: A Study of Middle and Ingestive Verbs

Krejci explains why middle and ingestive verbs (wash, dress; eat, learn) causativize like intransitives in languages that mark causatives morphologically. The report orders verb classes on a hierarchy of causativizability, unaccusatives before middles and ingestives before unergatives before simple transitives, on which no language's causative process skips a tier. The simple forms of these verbs are lexically reflexive, with an already causative event structure whose causer and causee are coidentified, and the lexical causative (feed, teach) arises by antireflexivization, which delinks the two arguments; this is Koontz-Garboden's reflexivization read in the opposite direction. On a model of eat, feed and make eat, the entailments of the simple form split between causer and causee of the lexical causative but stay with the causee of the periphrastic one.

Main statements

• feed_not_makeEat: feeding is not making eat.
• not_eat_and_feed: denying the simple form while asserting the lexical causative is consistent.
• restitutive_not_repetitive: again has a restitutive reading on the result state.
• ofAttribute_reaches_le_iff: the hierarchy is the order of implication among the tiers in the survey, so that no surveyed language skips a tier (table_respectsHierarchy).

Implementation notes

• The model takes the verb's event to be the change of state and closes the causing event existentially, as KoontzGarboden2009.causative does; make eat adds a second causing event with its own effector.
• Of the report's three tests of event-structural complexity only again is formalized; re- and almost have the same scopal structure. States are times in the model, a change giving rise to the state at its end, so that again on the result state has earlier states to presuppose.
• The Marathi evidence and the twenty surveyed languages outside Table 2.8 are not formalized.

References

• [Kre12]
• [KG09]
• [Chi04b]
• [Dow79]

Antireflexivization

@[reducible, inline]

abbrev Krejci2012.feed {Entity : Type u_1} {State : Type u_2} {E : Type u_4} (M : ArgumentStructure.EventStructure.Interpretation Entity State E) (manip : Entity → E → Prop) (S : Entity → State → Prop) : Entity → Entity → E → Prop

In the lexical causative (38a) the causer's manipulation of food brings the causee to the state of potential digestion.

Equations

• Krejci2012.feed M manip S = KoontzGarboden2009.causative M manip S

@[reducible, inline]

abbrev Krejci2012.eat {Entity : Type u_1} {State : Type u_2} {E : Type u_4} (M : ArgumentStructure.EventStructure.Interpretation Entity State E) (manip : Entity → E → Prop) (S : Entity → State → Prop) : Entity → E → Prop

The simple form (37a) is the lexical causative on its diagonal, where the eater manipulates the food and comes to digest it. Antireflexivization ((96)–(97)) delinks the two arguments.

Equations

• Krejci2012.eat M manip S = KoontzGarboden2009.reflexivize (Krejci2012.feed M manip S)

def Krejci2012.makeEat {Entity : Type u_1} {State : Type u_2} {E : Type u_4} (M : ArgumentStructure.EventStructure.Interpretation Entity State E) (manip : Entity → E → Prop) (S : Entity → State → Prop) (z x : Entity) (e : E) : Prop

The periphrastic causative make eat adds a further causing event, with its own effector, of an eating.

Equations

• Krejci2012.makeEat M manip S z x e = ∃ (w : E), M.effector z w ∧ M.cause w e ∧ Krejci2012.eat M manip S x e

def Krejci2012.causerAddition {Entity : Type u_1} {State : Type u_2} {E : Type u_4} (M : ArgumentStructure.EventStructure.Interpretation Entity State E) (ingest : Entity → E → Prop) (y x : Entity) (e : E) : Prop

Causativization by causer addition ((94)) is the analysis the report rejects, on which the simple form is an activity ingest with no causing subevent and the causative adds a causer.

Equations

• Krejci2012.causerAddition M ingest y x e = ∃ (w : E), M.effector y w ∧ M.cause w e ∧ ingest x e

def Krejci2012.earlier {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] : SetRel E E

earlier relates an event to the events whose run time is before its own.

Equations

• Krejci2012.earlier = {(e, e') : E × E | (Event.τ e').IsBefore (Event.τ e)}

def Krejci2012.againState {Entity : Type u_1} {State : Type u_2} (R : SetRel State State) (S : Entity → State → Prop) (x : Entity) (s : State) : Prop

On the restitutive reading again modifies only the result state ((66a)), so the state predicate holds of a state that an earlier state of it preceded, whether or not a change brought that earlier state about ((65a)). R relates a state to the earlier states. The restitutive reading of a verb is the verb over this predicate.

Equations

• Krejci2012.againState R S x s = (Presupposition.again R (S x) s = 1)

def Krejci2012.Repetitive {Entity : Type u_1} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (P : Entity → E → Prop) (x : Entity) (e : E) : Prop

On the repetitive reading again modifies the whole predicate ((66b)), so the sentence presupposes that the whole event happened before.

Equations

• Krejci2012.Repetitive P x e = (Presupposition.again Krejci2012.earlier (P x) e = 1)

theorem Krejci2012.eat_eq_anticausative {Entity : Type u_1} {State : Type u_2} {E : Type u_4} {M : ArgumentStructure.EventStructure.Interpretation Entity State E} {manip : Entity → E → Prop} {S : Entity → State → Prop} : eat M manip S = KoontzGarboden2009.anticausative M manip S

The simple form is the derived inchoative of KoontzGarboden2009.

theorem Krejci2012.exists_manip_of_eat {Entity : Type u_1} {State : Type u_2} {E : Type u_4} {M : ArgumentStructure.EventStructure.Interpretation Entity State E} {manip : Entity → E → Prop} {S : Entity → State → Prop} {x : Entity} {e : E} (h : eat M manip S x e) : ∃ (w : E), manip x w ∧ M.cause w e

The eater manipulates food ((39a)).

theorem Krejci2012.exists_manip_of_feed {Entity : Type u_1} {State : Type u_2} {E : Type u_4} {M : ArgumentStructure.EventStructure.Interpretation Entity State E} {manip : Entity → E → Prop} {S : Entity → State → Prop} {x y : Entity} {e : E} (h : feed M manip S y x e) : ∃ (w : E), manip y w ∧ M.cause w e

The feeder manipulates food ((45)).

theorem Krejci2012.inchoative_of_feed {Entity : Type u_1} {State : Type u_2} {E : Type u_4} {M : ArgumentStructure.EventStructure.Interpretation Entity State E} {manip : Entity → E → Prop} {S : Entity → State → Prop} {x y : Entity} {e : E} (h : feed M manip S y x e) : M.vBecome S x e

Whoever is fed comes to potential digestion ((44c)).

theorem Krejci2012.exists_manip_of_makeEat {Entity : Type u_1} {State : Type u_2} {E : Type u_4} {M : ArgumentStructure.EventStructure.Interpretation Entity State E} {manip : Entity → E → Prop} {S : Entity → State → Prop} {x z : Entity} {e : E} (h : makeEat M manip S z x e) : ∃ (w : E), manip x w ∧ M.cause w e

Whoever is made to eat manipulates food ((47a)).

theorem Krejci2012.ingest_of_causerAddition {Entity : Type u_1} {State : Type u_2} {E : Type u_4} {M : ArgumentStructure.EventStructure.Interpretation Entity State E} {x y : Entity} {e : E} {ingest : Entity → E → Prop} (h : causerAddition M ingest y x e) : ingest x e

Under causer addition the causative entails the simple form, so denying the one while asserting the other is contradictory ((95)).

theorem Krejci2012.licensesBySelf_eat {Entity : Type u_1} {State : Type u_2} {E : Type u_4} {M : ArgumentStructure.EventStructure.Interpretation Entity State E} {manip : Entity → E → Prop} {S : Entity → State → Prop} (h : ∀ (x : Entity) (w : E), manip x w → M.effector x w) : KoontzGarboden2009.LicensesBySelf M (eat M manip S)

Eating licenses by itself ((114a)), having a causing subevent whose effector is the eater, once manipulating food makes one an effector.

Mary and John

inductive Krejci2012.Participant : Type

A Participant is Mary or John.

• mary : Participant
• john : Participant

@[instance_reducible]

instance Krejci2012.instDecidableEqParticipant : DecidableEq Participant

Equations

• Krejci2012.instDecidableEqParticipant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krejci2012.ev (s t : ℤ) (h : s ≤ t := by decide) : NonemptyInterval ℤ

ev s t is the event running from s to t.

Equations

• Krejci2012.ev s t h = { fst := s, snd := t, fst_le_snd := h }

def Krejci2012.At (w : NonemptyInterval ℤ) (s t : ℤ) : Prop

At w s t says that the event w runs from s to t.

Equations

• Krejci2012.At w s t = ((Event.τ w).toProd = (s, t))

def Krejci2012.w₀ : NonemptyInterval ℤ

Equations

• Krejci2012.w₀ = Krejci2012.ev 0 1 Krejci2012.w₀._proof_1

def Krejci2012.e₀ : NonemptyInterval ℤ

Equations

• Krejci2012.e₀ = Krejci2012.ev 1 2 Krejci2012.e₀._proof_1

def Krejci2012.w₁ : NonemptyInterval ℤ

Equations

• Krejci2012.w₁ = Krejci2012.ev 0 2 Krejci2012.w₁._proof_1

def Krejci2012.w₂ : NonemptyInterval ℤ

Equations

• Krejci2012.w₂ = Krejci2012.ev 3 4 Krejci2012.w₂._proof_1

def Krejci2012.e₁ : NonemptyInterval ℤ

Equations

• Krejci2012.e₁ = Krejci2012.ev 4 5 Krejci2012.e₁._proof_1

def Krejci2012.digesting (x : Participant) (s : ℤ) : Prop

The state of potential digestion holds of John after each meal of the scenarios below, the states at the times 2 and 5.

Equations

• Krejci2012.digesting x s = (x = Krejci2012.Participant.john ∧ (s = 2 ∨ s = 5))

def Krejci2012.eating (causing : NonemptyInterval ℤ → NonemptyInterval ℤ → Prop) (eff : Participant → NonemptyInterval ℤ → Prop) : ArgumentStructure.EventStructure.Interpretation Participant ℤ (NonemptyInterval ℤ)

eating causing eff is the model in which the events causing lists bring John to potential digestion, with eff the effectors of events. States are times, and a change gives rise to the state at its end.

Equations

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

def Krejci2012.spoonManip (y : Participant) (w : NonemptyInterval ℤ) : Prop

Mary manipulates the food.

Equations

• Krejci2012.spoonManip y w = (y = Krejci2012.Participant.mary ∧ Krejci2012.At w 0 1)

def Krejci2012.spoonFeeding : ArgumentStructure.EventStructure.Interpretation Participant ℤ (NonemptyInterval ℤ)

In spoon feeding ((44a)) Mary's manipulation of the food causes John's change.

Equations

• Krejci2012.spoonFeeding = Krejci2012.eating (fun (w e : NonemptyInterval ℤ) => Krejci2012.At w 0 1 ∧ Krejci2012.At e 1 2) Krejci2012.spoonManip

def Krejci2012.supManip (y : Participant) (w : NonemptyInterval ℤ) : Prop

John manipulates the food.

Equations

• Krejci2012.supManip y w = (y = Krejci2012.Participant.john ∧ Krejci2012.At w 0 1)

def Krejci2012.supervising : ArgumentStructure.EventStructure.Interpretation Participant ℤ (NonemptyInterval ℤ)

Under supervision ((48)) John's manipulation of the food and Mary's supervising action both cause John's change.

Equations

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

def Krejci2012.twoManip (y : Participant) (w : NonemptyInterval ℤ) : Prop

Mary manipulates the food the first time, John the second.

Equations

• Krejci2012.twoManip y w = (y = Krejci2012.Participant.mary ∧ Krejci2012.At w 0 1 ∨ y = Krejci2012.Participant.john ∧ Krejci2012.At w 3 4)

def Krejci2012.twoMeals : ArgumentStructure.EventStructure.Interpretation Participant ℤ (NonemptyInterval ℤ)

In the model of two meals Mary feeds John, and later John eats.

Equations

• Krejci2012.twoMeals = Krejci2012.eating (fun (w e : NonemptyInterval ℤ) => Krejci2012.At w 0 1 ∧ Krejci2012.At e 1 2 ∨ Krejci2012.At w 3 4 ∧ Krejci2012.At e 4 5) Krejci2012.twoManip

theorem Krejci2012.not_eat_and_feed : ¬eat spoonFeeding spoonManip digesting Participant.john e₀ ∧ feed spoonFeeding spoonManip digesting Participant.mary Participant.john e₀

I didn't eat pie; you fed pie to me ((92), (106)) is consistent, since John, fed by Mary, did not eat, having manipulated no food ((44a)).

theorem Krejci2012.feed_not_makeEat : feed spoonFeeding spoonManip digesting Participant.mary Participant.john e₀ ∧ ¬makeEat spoonFeeding spoonManip digesting Participant.mary Participant.john e₀

Feeding is not making eat, since John, fed, was not made to eat, as whoever is made to eat manipulates food ((47a)).

theorem Krejci2012.makeEat_not_feed : makeEat supervising supManip digesting Participant.mary Participant.john e₀ ∧ ¬feed supervising supManip digesting Participant.mary Participant.john e₀

Making eat is not feeding ((48)), since Mary made John eat without touching any food.

theorem Krejci2012.not_licensesBySelf_inchoative : ¬KoontzGarboden2009.LicensesBySelf spoonFeeding (spoonFeeding.vBecome digesting)

Being fed does not license by itself ((113d)), since John reaches the state but the effector of the causing event is Mary.

theorem Krejci2012.restitutive_not_repetitive : eat twoMeals twoManip (againState {p : ℤ × ℤ | p.2 < p.1} digesting) Participant.john e₁ ∧ ¬Repetitive (eat twoMeals twoManip digesting) Participant.john e₁

John ate again said after Mary had fed him, a second causer bringing about the result state as in the context of (70). The restitutive reading holds, again on the state of potential digestion ((66a)), which John had been in before, and the repetitive reading fails, since John had not eaten before.

The hierarchy of causativizability

inductive Krejci2012.Tier : Type

A Tier is a tier of the hierarchy (22), from the most readily causativized.

• unaccusative : Tier
• middleIngestive : Tier
• unergative : Tier
• simpleTransitive : Tier

@[instance_reducible]

instance Krejci2012.instDecidableEqTier : DecidableEq Tier

Equations

• Krejci2012.instDecidableEqTier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Krejci2012.instFintypeTier : Fintype Tier

Equations

• Krejci2012.instFintypeTier = { elems := { val := ↑Krejci2012.Tier.enumList, nodup := Krejci2012.Tier.enumList_nodup }, complete := Krejci2012.instFintypeTier._proof_1 }

@[instance_reducible]

instance Krejci2012.instReprTier : Repr Tier

Equations

• Krejci2012.instReprTier = { reprPrec := Krejci2012.instReprTier.repr }

def Krejci2012.instReprTier.repr : Tier → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krejci2012.instReprTier.repr Krejci2012.Tier.unaccusative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krejci2012.Tier.unaccusative")).group prec✝
• Krejci2012.instReprTier.repr Krejci2012.Tier.unergative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krejci2012.Tier.unergative")).group prec✝

def Krejci2012.Tier.rank : Tier → ℕ

t.rank is the position of the tier t on the hierarchy.

Equations

• Krejci2012.Tier.unaccusative.rank = 0
• Krejci2012.Tier.middleIngestive.rank = 1
• Krejci2012.Tier.unergative.rank = 2
• Krejci2012.Tier.simpleTransitive.rank = 3

@[instance_reducible]

instance Krejci2012.instLinearOrderTier : LinearOrder Tier

Equations

• Krejci2012.instLinearOrderTier = LinearOrder.lift' Krejci2012.Tier.rank Krejci2012.instLinearOrderTier._proof_1

structure Krejci2012.Causative : Type

A causative process of a language is the set of tiers whose verbs it applies to.

• language : String
• morpheme : String
• reach : Finset Tier

def Krejci2012.Causative.RespectsHierarchy (c : Causative) : Prop

A process respects the hierarchy when it reaches every tier before a tier it reaches.

Equations

• c.RespectsHierarchy = IsLowerSet ↑c.reach

@[instance_reducible]

instance Krejci2012.Causative.instDecidablePredRespectsHierarchy : DecidablePred RespectsHierarchy

Equations

• x✝.instDecidablePredRespectsHierarchy = { decide := decide (∀ a ∈ x✝.reach, ∀ b ≤ a, b ∈ x✝.reach), reflects_decide := ⋯ }

def Krejci2012.Causative.type (c : Causative) : WithBot Tier

The type of a process, (1) to (4) of Table 2.8, is the last tier it reaches.

Equations

• c.type = c.reach.max

theorem Krejci2012.Causative.mem_reach_iff {c : Causative} (h : c.RespectsHierarchy) (t : Tier) : t ∈ c.reach ↔ ↑t ≤ c.type

A process that respects the hierarchy reaches exactly the tiers up to its type.

def Krejci2012.table : List Causative

table lists the surveyed languages of Table 2.8, three of each type. Malayalam reaches transitives only with an instrumental causee and is listed with the third type.

Equations

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

def Krejci2012.Reaches (c : { c : Causative // c ∈ table }) (t : Tier) : Prop

The survey as a formal context, a surveyed process bearing the tiers it reaches.

Equations

• Krejci2012.Reaches c t = (t ∈ (↑c).reach)

theorem Krejci2012.ofAttribute_reaches_le_iff {t t' : Tier} : Concept.ofAttribute Reaches t' ≤ Concept.ofAttribute Reaches t ↔ t ≤ t'

The hierarchy is the order of implication among the tiers in the survey, one tier coming before another exactly when every surveyed process that reaches the second reaches the first.

theorem Krejci2012.table_respectsHierarchy (c : Causative) : c ∈ table → c.RespectsHierarchy

No surveyed language skips a tier.