Little v

[Cue03]'s event introducers: the three flavors of little v that verbalize a root and fix its event type. vDO builds activities, vGO events of change, movement and happening, vBE states. A sentence's event structure is the list of its verbal heads from the highest down; a complex structure embeds one vP under another, and the possible combinations of the dissertation's table (17) and its footnote are the chains of LittleV.Embeds: vDO embeds any event, vGO only a state, vBE nothing.

Causatives and inchoatives are the two complex structures: an event or state embedded under vDO, and a state embedded under vGO. There is no CAUSE head: "being causative is the property of the configuration as a whole", and the two alternants of cerrar share the lower stative event and differ in the dynamic head that embeds it, [vDO, vBE] against [vGO, vBE]. Only a vDO-headed structure combines with Voice and so licenses an external argument.

Main definitions

• LittleV, LittleV.Embeds, LittleV.IsWellFormed
• LittleV.Activity, LittleV.Change, LittleV.State, LittleV.Causative, LittleV.Inchoative, LittleV.LicensesVoice

Main results

• LittleV.Inchoative.eq_of_isWellFormed: a well-formed inchoative is exactly [vGO, vBE]
• LittleV.Causative.not_inchoative: causatives do not include inchoatives
• LittleV.causative_cons, LittleV.inchoative_cons: the alternation over a shared lower event

Implementation notes

The head-driven rivals, [Pyl08]'s Cause head and the v_CAUSE that [AAS06] and [Woo15] keep in both alternants so that Voice alone distinguishes them, are not encodable here: every Causative is BiEventive, and the alternation changes the higher head rather than Voice (Causative.not_inchoative). A study of those programs states its claims about Minimalist.Voice directly.

References

• [Cue03]
• [AAS06]
• [Pyl08]
• [Woo15]

inductive Minimalist.LittleV : Type

[Cue03]'s flavors of v, the event introducers that verbalize a root.

• vDO : LittleV

  Dynamic activity: the root names a manner of acting; the only head Voice combines with.

• vGO : LittleV

  Dynamic change, movement or happening; unaccusative.

• vBE : LittleV

  State; unaccusative.

@[instance_reducible]

instance Minimalist.instDecidableEqLittleV : DecidableEq LittleV

Equations

• Minimalist.instDecidableEqLittleV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.instReprLittleV.repr : LittleV → ℕ → Std.Format

Equations

• Minimalist.instReprLittleV.repr Minimalist.LittleV.vDO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.LittleV.vDO")).group prec✝
• Minimalist.instReprLittleV.repr Minimalist.LittleV.vGO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.LittleV.vGO")).group prec✝
• Minimalist.instReprLittleV.repr Minimalist.LittleV.vBE prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.LittleV.vBE")).group prec✝

@[instance_reducible]

instance Minimalist.instReprLittleV : Repr LittleV

Equations

• Minimalist.instReprLittleV = { reprPrec := Minimalist.instReprLittleV.repr }

def Minimalist.LittleV.Dynamic (v : LittleV) : Prop

Dynamic heads, vDO and vGO, against stative vBE.

Equations

• v.Dynamic = (v ≠ Minimalist.LittleV.vBE)

@[instance_reducible]

instance Minimalist.LittleV.instDecidablePredDynamic : DecidablePred Dynamic

Equations

• x✝.instDecidablePredDynamic = { decide := !decide (x✝ = Minimalist.LittleV.vBE), reflects_decide := ⋯ }

def Minimalist.LittleV.Embeds (v w : LittleV) : Prop

Which event a head may embed, [Cue03]'s table (17) with its footnote: vDO embeds any event, vGO only a state, and vBE nothing, since events have to "become" states before they combine with vBE.

Equations

• v.Embeds w = (v = Minimalist.LittleV.vDO ∨ v = Minimalist.LittleV.vGO ∧ w = Minimalist.LittleV.vBE)

@[instance_reducible]

instance Minimalist.LittleV.instDecidableRelEmbeds : DecidableRel Embeds

Equations

• x✝¹.instDecidableRelEmbeds x✝ = { decide := decide (x✝¹ = Minimalist.LittleV.vDO) || decide (x✝¹ = Minimalist.LittleV.vGO ∧ x✝ = Minimalist.LittleV.vBE), reflects_decide := ⋯ }

theorem Minimalist.LittleV.Embeds.dynamic {v w : LittleV} (h : v.Embeds w) : v.Dynamic

@[simp]

theorem Minimalist.LittleV.not_vBE_embeds (w : LittleV) : ¬vBE.Embeds w

@[simp]

theorem Minimalist.LittleV.vGO_embeds_iff {w : LittleV} : vGO.Embeds w ↔ w = vBE

@[simp]

theorem Minimalist.LittleV.vDO_embeds (w : LittleV) : vDO.Embeds w

def Minimalist.LittleV.IsWellFormed (l : List LittleV) : Prop

A well-formed event structure: a nonempty top-down chain of heads, each embedding the next.

Equations

• Minimalist.LittleV.IsWellFormed l = (l ≠ [] ∧ List.IsChain Minimalist.LittleV.Embeds l)

@[instance_reducible]

instance Minimalist.LittleV.instDecidablePredListIsWellFormed : DecidablePred IsWellFormed

Equations

• Minimalist.LittleV.instDecidablePredListIsWellFormed x✝ = { decide := decide (x✝ ≠ []) && decide (List.IsChain Minimalist.LittleV.Embeds x✝), reflects_decide := ⋯ }

theorem Minimalist.LittleV.IsWellFormed.not_infix_vBE {l : List LittleV} (hw : IsWellFormed l) (w : LittleV) : ¬[vBE, w] <:+: l

Nothing is embedded under vBE.

theorem Minimalist.LittleV.IsWellFormed.eq_vBE_of_infix_vGO {l : List LittleV} {w : LittleV} (hw : IsWellFormed l) (h : [vGO, w] <:+: l) : w = vBE

vGO embeds only a state.

Event types ([Cue03] §1.3)

def Minimalist.LittleV.Activity (l : List LittleV) : Prop

A simple activity: a root verbalized by vDO alone.

Equations

• Minimalist.LittleV.Activity l = (l = [Minimalist.LittleV.vDO])

def Minimalist.LittleV.Change (l : List LittleV) : Prop

A simple predicate of change, movement or happening: vGO alone.

Equations

• Minimalist.LittleV.Change l = (l = [Minimalist.LittleV.vGO])

def Minimalist.LittleV.State (l : List LittleV) : Prop

A simple state, existential or predicational: vBE alone.

Equations

• Minimalist.LittleV.State l = (l = [Minimalist.LittleV.vBE])

def Minimalist.LittleV.BiEventive (l : List LittleV) : Prop

A complex, bi-eventive event: at least two sub-events.

Equations

• Minimalist.LittleV.BiEventive l = (2 ≤ l.length)

def Minimalist.LittleV.Causative (l : List LittleV) : Prop

A causative: an event or result embedded under vDO; the causative reading is the interpretation of this configuration, not of a CAUSE head.

Equations

• Minimalist.LittleV.Causative l = (l.head? = some Minimalist.LittleV.vDO ∧ Minimalist.LittleV.BiEventive l)

def Minimalist.LittleV.Inchoative (l : List LittleV) : Prop

An inchoative: a result embedded under vGO.

Equations

• Minimalist.LittleV.Inchoative l = (l.head? = some Minimalist.LittleV.vGO ∧ Minimalist.LittleV.BiEventive l)

def Minimalist.LittleV.LicensesVoice (l : List LittleV) : Prop

Combines with Voice, and so licenses an external argument: vDO-headed structures only, predicates of change and states being unaccusative.

Equations

• Minimalist.LittleV.LicensesVoice l = (l.head? = some Minimalist.LittleV.vDO)

@[instance_reducible]

instance Minimalist.LittleV.instDecidablePredListActivity : DecidablePred Activity

Equations

• Minimalist.LittleV.instDecidablePredListActivity x✝ = Minimalist.LittleV.instDecidablePredListActivity._aux_1 x✝

@[instance_reducible]

instance Minimalist.LittleV.instDecidablePredListChange : DecidablePred Change

Equations

• Minimalist.LittleV.instDecidablePredListChange x✝ = Minimalist.LittleV.instDecidablePredListChange._aux_1 x✝

@[instance_reducible]

instance Minimalist.LittleV.instDecidablePredListState : DecidablePred State

Equations

• Minimalist.LittleV.instDecidablePredListState x✝ = Minimalist.LittleV.instDecidablePredListState._aux_1 x✝

@[instance_reducible]

instance Minimalist.LittleV.instDecidablePredListBiEventive : DecidablePred BiEventive

Equations

• Minimalist.LittleV.instDecidablePredListBiEventive x✝ = { decide := Nat.ble 2 x✝.length, reflects_decide := ⋯ }

@[instance_reducible]

instance Minimalist.LittleV.instDecidablePredListCausative : DecidablePred Causative

Equations

• Minimalist.LittleV.instDecidablePredListCausative x✝ = { decide := decide (x✝.head? = some Minimalist.LittleV.vDO) && decide (Minimalist.LittleV.BiEventive x✝), reflects_decide := ⋯ }

@[instance_reducible]

instance Minimalist.LittleV.instDecidablePredListInchoative : DecidablePred Inchoative

Equations

• Minimalist.LittleV.instDecidablePredListInchoative x✝ = { decide := decide (x✝.head? = some Minimalist.LittleV.vGO) && decide (Minimalist.LittleV.BiEventive x✝), reflects_decide := ⋯ }

@[instance_reducible]

instance Minimalist.LittleV.instDecidablePredListLicensesVoice : DecidablePred LicensesVoice

Equations

• Minimalist.LittleV.instDecidablePredListLicensesVoice x✝ = Minimalist.LittleV.instDecidablePredListLicensesVoice._aux_1 x✝

theorem Minimalist.LittleV.Causative.biEventive {l : List LittleV} (h : Causative l) : BiEventive l

theorem Minimalist.LittleV.Inchoative.biEventive {l : List LittleV} (h : Inchoative l) : BiEventive l

theorem Minimalist.LittleV.Causative.licensesVoice {l : List LittleV} (h : Causative l) : LicensesVoice l

theorem Minimalist.LittleV.Inchoative.not_licensesVoice {l : List LittleV} (h : Inchoative l) : ¬LicensesVoice l

theorem Minimalist.LittleV.Causative.not_inchoative {l : List LittleV} (h : Causative l) : ¬Inchoative l

Causatives do not include inchoatives: the two differ in the higher head.

theorem Minimalist.LittleV.Change.not_licensesVoice {l : List LittleV} (h : Change l) : ¬LicensesVoice l

theorem Minimalist.LittleV.State.not_licensesVoice {l : List LittleV} (h : State l) : ¬LicensesVoice l

theorem Minimalist.LittleV.Inchoative.eq_of_isWellFormed {l : List LittleV} (hi : Inchoative l) (hw : IsWellFormed l) : l = [vGO, vBE]

A well-formed inchoative is exactly [vGO, vBE]: vGO embeds only a state, under which nothing is embedded.

The causative alternation ([Cue03] §§1.3.4–1.3.5)

Over a shared lower event, vDO gives the causative and vGO the inchoative: Vicki cerró la puerta is [vDO, vBE] under Voice, se cerró la puerta is [vGO, vBE] with se spelling out vGO.

theorem Minimalist.LittleV.causative_cons {lower : List LittleV} (h : lower ≠ []) : Causative (vDO :: lower)

theorem Minimalist.LittleV.inchoative_cons {lower : List LittleV} (h : lower ≠ []) : Inchoative (vGO :: lower)

theorem Minimalist.LittleV.possible_combinations : IsWellFormed [vDO, vDO] ∧ IsWellFormed [vDO, vGO] ∧ IsWellFormed [vDO, vBE] ∧ IsWellFormed [vGO, vBE] ∧ Causative [vDO, vDO] ∧ Causative [vDO, vGO] ∧ Causative [vDO, vBE] ∧ Inchoative [vGO, vBE]

The four possible combinations of table (17) are well formed, the three under vDO causative and the one under vGO inchoative.

theorem Minimalist.LittleV.impossible_combinations : ¬IsWellFormed [vBE, vDO] ∧ ¬IsWellFormed [vBE, vGO] ∧ ¬IsWellFormed [vGO, vGO] ∧ ¬IsWellFormed [vGO, vDO]

The combinations the footnote to (17) excludes: nothing under vBE, nothing dynamic under vGO.