Coon 2019: building verbs in Chuj

Coon argues from the Chuj verb stem that the root decides whether there is an internal argument and the functional head v ~ Voice⁰ decides the rest. Roots fall into four classes that semantic type partly distinguishes, transitive and intransitive roots being event predicates over an entity, positional roots measure functions and nominal roots properties, and a verb stem is a root plus one of the heads Ø, -w, -ch and -j, the first doubling as the null head of intransitive roots, which merge an agent with inherent ergative case, an agent without it, an implicit agent, or no agent. Since finite Infl⁰ licenses one absolutive argument, an agent without ergative case takes it, so a transitive root under -w cannot realize its argument as a full DP and does so as a bare NP composed by Restrict or as an implicit argument bound by Existential Closure, the suffix -aj being the overt reflex of that binding in absolutive antipassives and in passives with an implicit agent, while an intransitive root, whose sole argument is a DP, admits no -w at all. Every stem of a transitive root thus composes with an internal argument, and a language without the head that merges an agent free of ergative case, Ch'ol, has no agentive intransitive stems.

Implementation notes

The heads are Minimalist Voice heads whose parametric semantics supplies two of the three properties the licensing count reads, an external argument and its implicitness; the third, inherent ergative case, is the transitive head's own, since the substrate's Case checking is the accusative of v. The count adopts the Obligatory Case Parameter of footnote 15, one of the two options the paper leaves open. The class of a root fixes which realizations its internal slot admits; that an intransitive root's argument is only ever a full DP encodes the absence of unaccusative subject incorporation, (48), which the paper leaves to typology, and no implicit option for such roots is attested. The event semantics of §3.2.2 records truth conditions; the locus of Existential Closure that separates the two antipassives lives in the -aj predicate. Status suffixes, derived transitives in -ej, word order, stative -an stems, the inanimate causer of (70a) and the isolated -j form (71) are recorded as data only.

References

• J. Coon, Building verbs in Chuj: Consequences for the nature of roots (2019)
• S. Chung and W. A. Ladusaw, Restriction and Saturation (2004)
• M. Diesing, Indefinites (1992)
• H. Harley, The 'bundling' hypothesis and the disparate functions of little v (2017)
• A. Kratzer, Severing the external argument from its verb (1996)
• H. Davis, Deep unaccusativity and zero syntax in St'át'imcets (1997)
• R. Henderson, The roots of measurement (2017)
• J. M. Maxwell, Chuj intransitives: Or when can an intransitive verb take an object? (1976)
• A. Alexiadou, E. Anagnostopoulou and F. Schäfer, The properties of anticausatives crosslinguistically (2006)
• J. Wood, Icelandic Morphosyntax and Argument Structure (2015)

Root classes

def Chuj.RootClass.toRoot : RootClass → Semantics.Root

[Coo19]'s coordinates for the four root classes, (3) and §3.3: transitive and intransitive roots are event predicates over an internal argument, only the former compatible with the agent-merging Voice head; positional roots are measure functions after [Hen17] and nominal roots properties, neither selecting an internal argument in the sense of (2).

Equations

• Chuj.RootClass.tv.toRoot = { valency := some {ArgumentStructure.ArgPosition.internal}, denotationType := some (Montague.Ty.e ⇒ Montague.Ty.s ⇒ Montague.Ty.t), licensesTransitiveVoice := true }
• Chuj.RootClass.itv.toRoot = { valency := some {ArgumentStructure.ArgPosition.internal}, denotationType := some (Montague.Ty.e ⇒ Montague.Ty.s ⇒ Montague.Ty.t) }
• Chuj.RootClass.pos.toRoot = { valency := some ∅, denotationType := some (Montague.Ty.e ⇒ Montague.Ty.s ⇒ Montague.Ty.d) }
• Chuj.RootClass.nom.toRoot = { valency := some ∅, denotationType := some (Montague.Ty.e ⇒ Montague.Ty.t) }

theorem Coon2019.tv_itv_differ_only_in_voice : Chuj.RootClass.tv.toRoot.denotationType = Chuj.RootClass.itv.toRoot.denotationType ∧ Chuj.RootClass.tv.toRoot.valency = Chuj.RootClass.itv.toRoot.valency ∧ Chuj.RootClass.tv.toRoot.licensesTransitiveVoice ≠ Chuj.RootClass.itv.toRoot.licensesTransitiveVoice

√TV and √ITV share type and valency, after [Dav97]; compatibility with external causation by an agent alone separates them, §3.3.

The v ~ Voice⁰ heads

inductive Coon2019.V : Type

The v ~ Voice⁰ heads of the verb stem ((6), (78)), the transitive Ø, the null intransitive head of §2.1, and the suffixes -w, -ch and -j.

• transitive : V
• intransitive : V
• w : V
• ch : V
• j : V

@[instance_reducible]

instance Coon2019.instDecidableEqV : DecidableEq V

Equations

• Coon2019.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Coon2019.instFintypeV : Fintype V

Equations

• Coon2019.instFintypeV = { elems := { val := ↑Coon2019.V.enumList, nodup := Coon2019.V.enumList_nodup }, complete := Coon2019.instFintypeV._proof_1 }

@[instance_reducible]

instance Coon2019.instReprV : Repr V

Equations

• Coon2019.instReprV = { reprPrec := Coon2019.instReprV.repr }

def Coon2019.instReprV.repr : V → ℕ → Std.Format

Equations

• Coon2019.instReprV.repr Coon2019.V.transitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.V.transitive")).group prec✝
• Coon2019.instReprV.repr Coon2019.V.intransitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.V.intransitive")).group prec✝
• Coon2019.instReprV.repr Coon2019.V.w prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.V.w")).group prec✝
• Coon2019.instReprV.repr Coon2019.V.ch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.V.ch")).group prec✝
• Coon2019.instReprV.repr Coon2019.V.j prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.V.j")).group prec✝

def Coon2019.V.head : V → Minimalist.Voice.Head

The Minimalist Voice head each realizes, a bundled v ~ Voice⁰ after [Har17] introducing the external argument as in [Kra96] and specified for whether and what it introduces as in [AAS06] and [Woo15]. The transitive head and -w both merge an agent, footnote 10; -ch merges an implicit, existentially bound agent in its specifier, (64), the impersonal cell with a specifier; -j and the null intransitive head introduce no external argument and project no specifier, (68), the expletive cell.

Equations

• One or more equations did not get rendered due to their size.
• Coon2019.V.transitive.head = Minimalist.Voice.agentive
• Coon2019.V.intransitive.head = Minimalist.Voice.middle
• Coon2019.V.w.head = Minimalist.Voice.agentive
• Coon2019.V.j.head = Minimalist.Voice.middle

def Coon2019.V.AssignsErgative (v : V) : Prop

The head assigns inherent ergative case to the agent in its specifier, as the transitive head alone does (78).

Equations

• v.AssignsErgative = (v = Coon2019.V.transitive)

@[instance_reducible]

instance Coon2019.instDecidablePredVAssignsErgative : DecidablePred V.AssignsErgative

Equations

• Coon2019.instDecidablePredVAssignsErgative v = Coon2019.instDecidablePredVAssignsErgative._aux_1 v

theorem Coon2019.w_head_eq : V.w.head = V.transitive.head ∧ ¬V.w.AssignsErgative ∧ V.transitive.AssignsErgative

The two agent-introducing heads are one Voice cell and differ in inherent ergative case alone, footnote 10.

theorem Coon2019.dCoherent : (∀ (v : V), v ≠ V.ch → v.head.DCoherent) ∧ ¬V.ch.head.DCoherent

Every head keeps its [D] feature in step with its cell except -ch, whose specifier hosts the implicit agent of (64) that the impersonal cell leaves specifierless.

theorem Coon2019.head_table : (∀ (v : V), v.head.IsThematic ↔ v ≠ V.intransitive ∧ v ≠ V.j) ∧ ∀ (v : V), v.head.ExternalImplicit ↔ v = V.ch

The head properties behind (78) are read off the substrate cells: every head but -j and the null intransitive head introduces an external argument, and -ch alone an implicit one.

Licensing

inductive Coon2019.Internal : Type

How the internal argument slot of a root is realized ((56), (78)), by a full DP saturating it, a bare NP restricting it, or an implicit argument saturating it as a variable to be bound, or else absent.

• dp : Internal
• np : Internal
• implicit : Internal
• absent : Internal

@[instance_reducible]

instance Coon2019.instDecidableEqInternal : DecidableEq Internal

Equations

• Coon2019.instDecidableEqInternal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Coon2019.instFintypeInternal : Fintype Internal

Equations

• Coon2019.instFintypeInternal = { elems := { val := ↑Coon2019.Internal.enumList, nodup := Coon2019.Internal.enumList_nodup }, complete := Coon2019.instFintypeInternal._proof_1 }

def Coon2019.instReprInternal.repr : Internal → ℕ → Std.Format

Equations

• Coon2019.instReprInternal.repr Coon2019.Internal.dp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.Internal.dp")).group prec✝
• Coon2019.instReprInternal.repr Coon2019.Internal.np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.Internal.np")).group prec✝
• Coon2019.instReprInternal.repr Coon2019.Internal.implicit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.Internal.implicit")).group prec✝
• Coon2019.instReprInternal.repr Coon2019.Internal.absent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.Internal.absent")).group prec✝

@[instance_reducible]

instance Coon2019.instReprInternal : Repr Internal

Equations

• Coon2019.instReprInternal = { reprPrec := Coon2019.instReprInternal.repr }

def Coon2019.internals : Chuj.RootClass → List Internal

The realizations a root class admits. A transitive root composes with its argument in every stem, §5; nominal and positional roots select nothing, (39); an intransitive root's argument is a full DP, a coordinate stipulated here, since nothing in the analysis rules out (48b) and the paper leaves the absence of unaccusative subject incorporation to typology, while no implicit option for such roots is attested.

Equations

• Coon2019.internals Chuj.RootClass.tv = [Coon2019.Internal.dp, Coon2019.Internal.np, Coon2019.Internal.implicit]
• Coon2019.internals Chuj.RootClass.itv = [Coon2019.Internal.dp]
• Coon2019.internals Chuj.RootClass.pos = [Coon2019.Internal.absent]
• Coon2019.internals Chuj.RootClass.nom = [Coon2019.Internal.absent]

inductive Coon2019.Licenser : Type

The licenser of an argument, (78).

• voice : Licenser
• infl : Licenser
• unlicensed : Licenser

@[instance_reducible]

instance Coon2019.instDecidableEqLicenser : DecidableEq Licenser

Equations

• Coon2019.instDecidableEqLicenser x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Coon2019.instReprLicenser : Repr Licenser

Equations

• Coon2019.instReprLicenser = { reprPrec := Coon2019.instReprLicenser.repr }

def Coon2019.instReprLicenser.repr : Licenser → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Coon2019.instReprLicenser.repr Coon2019.Licenser.voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.Licenser.voice")).group prec✝
• Coon2019.instReprLicenser.repr Coon2019.Licenser.infl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.Licenser.infl")).group prec✝

def Coon2019.licenser (v : V) (i : Internal) : ArgumentStructure.ArgPosition → Licenser

Who licenses each argument position of a stem (§3.2.1, §3.2.2). The head cases its own specifier when it assigns inherent ergative, finite Infl⁰ cases a DP the head does not, and a bare NP, an implicit argument and an absent one need no case.

Equations

• One or more equations did not get rendered due to their size.
• Coon2019.licenser v i ArgumentStructure.ArgPosition.internal = if i = Coon2019.Internal.dp then Coon2019.Licenser.infl else Coon2019.Licenser.unlicensed

def Coon2019.Licensed (v : V) (i : Internal) : Prop

A stem is licensed when Infl⁰ has exactly one argument to license: it licenses one absolutive argument, and must license one, the Obligatory Case Parameter that footnote 15 offers beside an economy condition to keep the transitive head off stems whose only DP it would case itself.

Equations

• Coon2019.Licensed v i = ({a : ArgumentStructure.ArgPosition | Coon2019.licenser v i a = Coon2019.Licenser.infl}.card = 1)

@[instance_reducible]

instance Coon2019.instDecidableLicensed (v : V) (i : Internal) : Decidable (Licensed v i)

Equations

• Coon2019.instDecidableLicensed v i = id inferInstance

def Coon2019.V.Selects : V → Semantics.Root → Prop

The selection each head imposes on the root ((78), §2.1). The transitive head and the passive -ch need a root whose event admits an external agent, and so does -j apart from isolated forms like (71); the null intransitive head needs an unaccusative root; -w needs only a root, its ban on intransitive roots following from licensing rather than selection, §3.3.

Equations

• Coon2019.V.transitive.Selects x✝ = (x✝.licensesTransitiveVoice = true)
• Coon2019.V.ch.Selects x✝ = (x✝.licensesTransitiveVoice = true)
• Coon2019.V.j.Selects x✝ = (x✝.licensesTransitiveVoice = true)
• Coon2019.V.intransitive.Selects x✝ = (x✝.valency = some {ArgumentStructure.ArgPosition.internal} ∧ x✝.licensesTransitiveVoice = false)
• Coon2019.V.w.Selects x✝ = True

@[instance_reducible]

instance Coon2019.instDecidableSelects (v : V) (r : Semantics.Root) : Decidable (v.Selects r)

Equations

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

def Coon2019.WellFormed (rc : Chuj.RootClass) (v : V) (i : Internal) : Prop

A well-formed stem from a root class: the head selects the root, the root admits the realization, and the arguments are licensed.

Equations

• Coon2019.WellFormed rc v i = (v.Selects rc.toRoot ∧ i ∈ Coon2019.internals rc ∧ Coon2019.Licensed v i)

@[instance_reducible]

instance Coon2019.instDecidableWellFormed (rc : Chuj.RootClass) (v : V) (i : Internal) : Decidable (WellFormed rc v i)

Equations

• Coon2019.instDecidableWellFormed rc v i = id inferInstance

def Coon2019.V.voice : V → Internal → Option Voice

The voice of the fragment a head derives with a realization of the internal argument, Section 4: the transitive stem under the transitive head, the passives under -ch and -j, the attested -chaj carrying the -aj that closes the implicit agent, and under -w the incorporation antipassive with a bare NP and, with -aj closing an implicit theme, the absolutive antipassive; none under the null intransitive head, whose stem is no voice.

Equations

• Coon2019.V.transitive.voice x✝ = some Chuj.transitive
• Coon2019.V.intransitive.voice x✝ = none
• Coon2019.V.ch.voice x✝ = some Chuj.passive
• Coon2019.V.j.voice x✝ = some Chuj.agentlessPassive
• Coon2019.V.w.voice Coon2019.Internal.implicit = some Chuj.absolutiveAntipassive
• Coon2019.V.w.voice x✝ = some Chuj.incorporationAntipassive

def Coon2019.Forms (rc : Chuj.RootClass) (v : V) : Prop

A root class forms a stem with a head when the head is well-formed on it under some realization; stems with other derivational suffixes, (11) and (15), are not in view.

Equations

• Coon2019.Forms rc v = ∃ (i : Coon2019.Internal), Coon2019.WellFormed rc v i

@[instance_reducible]

instance Coon2019.instDecidableForms (rc : Chuj.RootClass) (v : V) : Decidable (Forms rc v)

Equations

• Coon2019.instDecidableForms rc v = id inferInstance

theorem Coon2019.forms_iff : (∀ (v : V), Forms Chuj.RootClass.tv v ↔ v ≠ V.intransitive) ∧ (∀ (v : V), Forms Chuj.RootClass.itv v ↔ v = V.intransitive) ∧ (∀ (v : V), Forms Chuj.RootClass.pos v ↔ v = V.w) ∧ ∀ (v : V), Forms Chuj.RootClass.nom v ↔ v = V.w

The distribution of the heads over the root classes is derived. √TV takes every head but the null intransitive one, (45) and (59) to (60); √ITV only that one, (47); √POS and √NOM only -w, (45), apart from isolated forms like (71).

theorem Coon2019.voice_tv_iff (vo : Voice) : vo ∈ Chuj.voices ↔ ∃ (v : V) (i : Internal), WellFormed Chuj.RootClass.tv v i ∧ v.voice i = some vo

The stems of a transitive root are exactly the five voices of the fragment, (58).

theorem Coon2019.tv_stems : {p : V × Internal | WellFormed Chuj.RootClass.tv p.1 p.2} = {(V.transitive, Internal.dp), (V.ch, Internal.dp), (V.j, Internal.dp), (V.w, Internal.np), (V.w, Internal.implicit)}

The stems of a transitive root ((78), (79)) have a full DP under the transitive head and under both passives, and a bare NP or an implicit argument under -w.

theorem Coon2019.w_no_dp (rc : Chuj.RootClass) : ¬WellFormed rc V.w Internal.dp

No stem of -w has a full DP internal argument, (37): Infl⁰ is taken by the agent.

theorem Coon2019.w_complement : ¬WellFormed Chuj.RootClass.tv V.w Internal.absent ∧ ¬WellFormed Chuj.RootClass.nom V.w Internal.np

A transitive root under -w requires its complement, (38), and a nominal root rejects one, (39): the difference lies in the root.

theorem Coon2019.itv_no_w : (∀ (i : Internal), ¬WellFormed Chuj.RootClass.itv V.w i) ∧ V.w.Selects Chuj.RootClass.itv.toRoot

No -w on an intransitive root, (47): with the agent on Infl⁰ the root's DP argument goes unlicensed, §3.3, a consequence of licensing rather than selection, given that the argument is a DP.

theorem Coon2019.every_class_verbalizes (rc : Chuj.RootClass) : ∃ (v : V), Forms rc v

Every class forms a verb stem with some head, so root class is not surface category (§5).

theorem Coon2019.licenser_table : licenser V.transitive Internal.dp ArgumentStructure.ArgPosition.external = Licenser.voice ∧ licenser V.transitive Internal.dp ArgumentStructure.ArgPosition.internal = Licenser.infl ∧ licenser V.ch Internal.dp ArgumentStructure.ArgPosition.external = Licenser.unlicensed ∧ licenser V.j Internal.dp ArgumentStructure.ArgPosition.external = Licenser.unlicensed ∧ licenser V.w Internal.np ArgumentStructure.ArgPosition.external = Licenser.infl ∧ licenser V.w Internal.np ArgumentStructure.ArgPosition.internal = Licenser.unlicensed ∧ licenser V.w Internal.implicit ArgumentStructure.ArgPosition.internal = Licenser.unlicensed

Table (78) for the stems of a transitive root. The external argument is licensed by v ~ Voice⁰ in the transitive, absent or implicit in the passives, and licensed by Infl⁰ under -w; the internal argument is licensed by Infl⁰ except under -w.

def Coon2019.AgentiveIntransitive (v : V) (i : Internal) : Prop

A stem is agentive intransitive when Infl⁰ licenses its overt external argument, hence a single absolutive argument (§3).

Equations

• Coon2019.AgentiveIntransitive v i = (Coon2019.licenser v i ArgumentStructure.ArgPosition.external = Coon2019.Licenser.infl ∧ Coon2019.Licensed v i)

@[instance_reducible]

instance Coon2019.instDecidableAgentiveIntransitive (v : V) (i : Internal) : Decidable (AgentiveIntransitive v i)

Equations

• Coon2019.instDecidableAgentiveIntransitive v i = id inferInstance

theorem Coon2019.agentiveIntransitive_iff (v : V) (i : Internal) : AgentiveIntransitive v i ↔ v = V.w ∧ i ≠ Internal.dp

Only -w forms agentive intransitive stems, (49), the head that merges an agent without ergative case. A language lacking it, Ch'ol, has no agentive intransitive verb stems and forms its unergatives and antipassives on nominal stems under a light verb, §3.4.2.

Implicit arguments and -aj

def Coon2019.Implicit (v : V) (i : Internal) : ArgumentStructure.ArgPosition → Prop

The implicit arguments of a stem, the existentially bound agent of -ch and the implicit internal argument of the absolutive antipassive.

Equations

• Coon2019.Implicit v i ArgumentStructure.ArgPosition.external = v.head.ExternalImplicit
• Coon2019.Implicit v i ArgumentStructure.ArgPosition.internal = (i = Coon2019.Internal.implicit)

def Coon2019.Aj (v : V) (i : Internal) : Prop

The suffix -aj, an overt reflex of Existential Closure ([Die92]) binding an implicit argument above v ~ VoiceP, §4.2: present exactly when the stem has one.

Equations

• Coon2019.Aj v i = ∃ (a : ArgumentStructure.ArgPosition), Coon2019.Implicit v i a

@[instance_reducible]

instance Coon2019.instDecidableImplicit (v : V) (i : Internal) (a : ArgumentStructure.ArgPosition) : Decidable (Implicit v i a)

Equations

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

@[instance_reducible]

instance Coon2019.instDecidableAj (v : V) (i : Internal) : Decidable (Aj v i)

Equations

• Coon2019.instDecidableAj v i = id inferInstance

theorem Coon2019.aj_table : Aj V.ch Internal.dp ∧ Aj V.w Internal.implicit ∧ ¬Aj V.j Internal.dp ∧ ¬Aj V.w Internal.np ∧ ¬Aj V.transitive Internal.dp

Table (58) puts -aj on the -chaj passive and the -waj absolutive antipassive, and on neither the -j passive, whose agent is absent, nor the incorporation antipassive, whose argument is bound at once (footnote 28).

Agent diagnostics

inductive Coon2019.ObliqueReading : Type

The reading of an oblique -uj phrase adjoined to a passive: the agent when the head has an implicit agent to identify, (62) and (66a); otherwise a cause of any kind, an agent not excluded but not required, (65) and (66b).

• agent : ObliqueReading
• cause : ObliqueReading

@[instance_reducible]

instance Coon2019.instDecidableEqObliqueReading : DecidableEq ObliqueReading

Equations

• Coon2019.instDecidableEqObliqueReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Coon2019.instReprObliqueReading.repr : ObliqueReading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Coon2019.instReprObliqueReading : Repr ObliqueReading

Equations

• Coon2019.instReprObliqueReading = { reprPrec := Coon2019.instReprObliqueReading.repr }

def Coon2019.V.obliqueReading (v : V) : ObliqueReading

The reading of the -uj phrase under each head.

Equations

• v.obliqueReading = if v.head.ExternalImplicit then Coon2019.ObliqueReading.agent else Coon2019.ObliqueReading.cause

theorem Coon2019.passive_contrast : V.ch.head.IsThematic ∧ ¬V.j.head.IsThematic ∧ V.ch.obliqueReading = ObliqueReading.agent ∧ V.j.obliqueReading = ObliqueReading.cause

Agent-oriented adverbs and purpose clauses need an agent, overt or implicit, §4.1: -ch admits them and reads its oblique as the agent, (62) and (63); -j rejects them and reads its oblique as a cause, (65) and (67).

Composing the internal argument

def Coon2019.restrict {E : Type u_1} {S : Type u_2} (P : E → S → Prop) (Q : E → Prop) : E → S → Prop

Restrict, footnote 19 after [CL04]: a property complement narrows the root without saturating its argument, (44b).

Equations

• Coon2019.restrict P Q x e = (P x e ∧ Q x)

def Coon2019.close {E : Type u_1} {S : Type u_2} (P : E → S → Prop) : S → Prop

Existential Closure, footnote 19 after [CL04]: the open argument is bound at the event level, (44c).

Equations

• Coon2019.close P e = ∃ (x : E), P x e

def Coon2019.transitiveStem {E : Type u_1} {S : Type u_2} (P : E → S → Prop) (a : E) : S → Prop

The transitive stem (43), in which the DP saturates the root by Functional Application.

Equations

• Coon2019.transitiveStem P a = P a

def Coon2019.incorporationStem {E : Type u_1} {S : Type u_2} (P : E → S → Prop) (Q : E → Prop) : S → Prop

The incorporation antipassive (44), in which the bare NP restricts the root and Existential Closure applies at once, so nothing is left open above v ~ VoiceP, footnote 28.

Equations

• Coon2019.incorporationStem P Q = Coon2019.close (Coon2019.restrict P Q)

def Coon2019.absolutiveStem {E : Type u_1} {S : Type u_2} (P : E → S → Prop) : S → Prop

The absolutive antipassive (75), in which the implicit argument saturates the root as a variable that the closure -aj spells out binds; the truth conditions coincide with closing at the root, the difference of locus that footnote 28 draws being what aj records.

Equations

• Coon2019.absolutiveStem P = Coon2019.close P

theorem Coon2019.stems_close {E : Type u_1} {S : Type u_2} (P : E → S → Prop) (Q : E → Prop) (a : E) : (∀ (e : S), transitiveStem P a e → absolutiveStem P e) ∧ ∀ (e : S), incorporationStem P Q e → absolutiveStem P e

Every stem of a transitive root composes with an internal argument (§5). Each describes events in which the root relation holds of some entity, so the transitive and incorporation stems entail the absolutive one, a corollary the paper does not draw.

The rows

def Coon2019.rowRoot (row : Datum) : Option Chuj.ChujRoot

The root of a row, from the fragment lexicon by its form.

Equations

• Coon2019.rowRoot row = do let f ← row.feature? "rootForm" List.find? (fun (x : Chuj.ChujRoot) => x.form == f) Chuj.allRoots

def Coon2019.heads : List (String × V)

Equations

• Coon2019.heads = [("transitive", Coon2019.V.transitive), ("intransitive", Coon2019.V.intransitive), ("w", Coon2019.V.w), ("ch", Coon2019.V.ch), ("j", Coon2019.V.j)]

structure Coon2019.Stem : Type

A stem row, with the root class, the head, the realization of the internal slot, and whether -aj appears.

• root : Chuj.RootClass

  The root class.

• head : V

  The head.

• internal : Internal

  The realization of the internal slot.

• hasAj : Bool

  Whether -aj appears.

def Coon2019.Stem.ofRow (row : Datum) : Option Stem

The stem a row records.

Equations

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

theorem Coon2019.stem_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "stem" → ∃ s ∈ Stem.ofRow row, (row.judgment ≠ Judgment.ungrammatical ↔ WellFormed s.root s.head s.internal) ∧ (row.judgment ≠ Judgment.ungrammatical → (s.hasAj = true ↔ Aj s.head s.internal))

For the stems of §2 to §4 and (79), a row is grammatical exactly when its stem is well-formed, and a grammatical row bears -aj exactly when its stem has an implicit argument.

def Coon2019.diagnosticHead (row : Datum) : Option V

The head a diagnostic row tests.

Equations

• Coon2019.diagnosticHead row = do guard (row.feature? "construction" = some "diagnostic") row.parse? "head" Coon2019.heads

theorem Coon2019.diagnostic_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "diagnostic" → ∃ v ∈ diagnosticHead row, row.judgment ≠ Judgment.ungrammatical ↔ v.head.IsThematic

Agent-oriented adverbs and purpose clauses are admitted exactly under a head with an agent ((63), (67)).

def Coon2019.obliqueRow (row : Datum) : Option (V × ObliqueReading)

The head and the recorded reading of an oblique row.

Equations

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

theorem Coon2019.oblique_rows (row : Datum) : row ∈ Examples.all → (row.feature? "oblique").isSome = true → ∃ p ∈ obliqueRow row, p.2 = p.1.obliqueReading

The -uj phrase names the agent under -ch and a cause under -j ((62), (65), (66), (70), (73)).