Argument Introduction by Functional Heads

[Kra96] [Pyl08] [WM17] [Par90] [Mol25] [Hop24]

Neo-Davidsonian substrate for argument-introducing heads (Voice, applicative, Cause), built on the canonical ThematicRel (Entity → Event Time → Prop, [Mol25]: "the preferred version of event semantics for syntacticians"). A verb/VP denotation is a predicate of events Event Time → Prop (this is Set (Event Time); used predicatively).

The central new object is VerbDenot: a verb denotation classified by the structure argument introduction is sensitive to (valence). [Pyl08]'s high/low contrast is the IntroMode parameter — whether the introduced participant is related to the event (high applicative / Voice, via Event Identification) or to the verb's internal theme (low applicative, via a transfer relation). The transitivity restriction then falls out of the denotations' types rather than being stipulated, and [WM17]'s contextually-interpreted single argument-introducer is its IntroMode reading.

Main definitions

• eventIdentification — [Kra96]'s Event Identification combinator
• RolesExclusive — thematic uniqueness (the principle behind eq. 103)
• VerbDenot — verb denotation classified by valence
• IntroMode / IntroMode.Licenses — high/low introduction and its licensing
• applToEvent / applToTheme — the high / low applicative denotations
• causeBieventive / causeThetaRole — the §3.2 Cause-is-not-a-θ-role contrast

Event Identification and thematic uniqueness

def ArgumentStructure.eventIdentification {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (f : ThematicRel Entity Time) (g : Event Time → Prop) : ThematicRel Entity Time

Event Identification ([Kra96]): combine an argument-introducer f (a thematic relation, awaiting its participant) with a VP predicate g, conjoining at the event. The result still awaits the introduced participant.

Equations

• ArgumentStructure.eventIdentification f g x e = (f x e ∧ g e)

theorem ArgumentStructure.eventIdentification_apply {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (f : ThematicRel Entity Time) (g : Event Time → Prop) (x : Entity) (e : Event Time) : eventIdentification f g x e ↔ f x e ∧ g e

def ArgumentStructure.RolesExclusive {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (r₁ r₂ : ThematicRel Entity Time) : Prop

Two thematic relations are role-exclusive when no participant bears both to the same event (thematic uniqueness). This is the principle behind [Pyl08]'s eq. 103: a participant cannot be both agent and theme.

Equations

• ArgumentStructure.RolesExclusive r₁ r₂ = ∀ (x : Entity) (e : Event Time), r₁ x e → ¬r₂ x e

Verb denotations classified by valence

inductive ArgumentStructure.VerbDenot (Entity : Type u_3) (Time : Type u_4) [LinearOrder Time] : Type (max u_3 u_4)

A verb/VP denotation, classified by the structure argument introduction is sensitive to. The valence distinction is a genuine type difference, which is why [Pyl08]'s transitivity restriction is a fact about this type rather than a stipulation.

• unergative — a saturated event predicate, no internal-argument slot (e.g. run). [Diagnostic 1 target]
• transitive — awaits its internal theme argument, carrying a theme relation (e.g. send a letter).
• kimianStative — a relation over individuals with no event argument (Kimian state, [Mol25] §1.4.1; e.g. own, owe). [Diagnostic 2]

• unergative {Entity : Type u_3} {Time : Type u_4} [LinearOrder Time] (body : Event Time → Prop) : VerbDenot Entity Time
• transitive {Entity : Type u_3} {Time : Type u_4} [LinearOrder Time] (theme body : ThematicRel Entity Time) : VerbDenot Entity Time
• kimianStative {Entity : Type u_3} {Time : Type u_4} [LinearOrder Time] (rel : Entity → Entity → Prop) : VerbDenot Entity Time

def ArgumentStructure.VerbDenot.IsTransitive {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] : VerbDenot Entity Time → Prop

Does this denotation supply an event-internal theme (Davidsonian transitive)? unergative (no participant slot) and kimianStative (no event argument) lack one, for two distinct structural reasons.

Equations

• (ArgumentStructure.VerbDenot.transitive theme body).IsTransitive = True
• x✝.IsTransitive = False

@[implicit_reducible]

instance ArgumentStructure.VerbDenot.instDecidablePredIsTransitive {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] : DecidablePred IsTransitive

Equations

• (ArgumentStructure.VerbDenot.transitive theme body).instDecidablePredIsTransitive = isTrue trivial
• (ArgumentStructure.VerbDenot.unergative body).instDecidablePredIsTransitive = isFalse ⋯
• (ArgumentStructure.VerbDenot.kimianStative rel).instDecidablePredIsTransitive = isFalse ⋯

Introduction mode and licensing

inductive ArgumentStructure.IntroMode : Type

The semantic mode of an argument introducer: whether it relates the introduced participant to the event (high applicative / Voice, via Event Identification) or to the verb's internal theme (low applicative, via a transfer relation). This is [Pyl08]'s high/low contrast at the denotational level, and [WM17]'s contextually-interpreted single argument-introducer.

• toEvent : IntroMode
• toTheme : IntroMode

@[implicit_reducible]

instance ArgumentStructure.instDecidableEqIntroMode : DecidableEq IntroMode

Equations

• ArgumentStructure.instDecidableEqIntroMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ArgumentStructure.instReprIntroMode.repr : IntroMode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ArgumentStructure.instReprIntroMode : Repr IntroMode

Equations

• ArgumentStructure.instReprIntroMode = { reprPrec := ArgumentStructure.instReprIntroMode.repr }

def ArgumentStructure.IntroMode.Licenses {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] : IntroMode → VerbDenot Entity Time → Prop

Which verb denotations an introducer of this mode can compose with, derived from the denotation's valence: an event-relating introducer composes with anything; a theme-relating one needs an event-internal theme.

Equations

• ArgumentStructure.IntroMode.toEvent.Licenses x✝ = True
• ArgumentStructure.IntroMode.toTheme.Licenses x✝ = x✝.IsTransitive

@[implicit_reducible]

instance ArgumentStructure.instDecidablePredVerbDenotLicenses {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (m : IntroMode) : DecidablePred m.Licenses

Equations

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

Applicative denotations

def ArgumentStructure.applToEvent {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (rel : ThematicRel Entity Time) (vp : Event Time → Prop) : ThematicRel Entity Time

High applicative / Voice denotation: introduce a participant related to the EVENT, via Event Identification. Total over any VP predicate — so it composes with unergatives.

Equations

• ArgumentStructure.applToEvent rel vp = ArgumentStructure.eventIdentification rel vp

def ArgumentStructure.applToTheme {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (themeRel : ThematicRel Entity Time) (transfer : Entity → Entity → Prop) (verb : ThematicRel Entity Time) (theme applied : Entity) : Event Time → Prop

Low applicative denotation: relate the applied argument to the THEME of a transitive verb via a transfer relation. Requires the verb's internal theme function ThematicRel Entity Time (type ⟨e,⟨s,t⟩⟩) — an unergative or Kimian state cannot supply it.

Equations

• ArgumentStructure.applToTheme themeRel transfer verb theme applied e = (verb theme e ∧ themeRel theme e ∧ transfer theme applied)

theorem ArgumentStructure.applToTheme_entails_theme {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (themeRel : ThematicRel Entity Time) (transfer : Entity → Entity → Prop) (verb : ThematicRel Entity Time) (theme applied : Entity) (e : Event Time) (h : applToTheme themeRel transfer verb theme applied e) : themeRel theme e

Any low-applicative denotation entails the theme bears the theme relation — the theme conjunct is present by construction.

The transitivity restriction, derived

theorem ArgumentStructure.toEvent_licenses_all {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (vd : VerbDenot Entity Time) : IntroMode.toEvent.Licenses vd

High introduction licenses any verb, including unergatives (Luganda/Venda/ Albanian high applicatives over unergatives, [Pyl08] §2.1.2).

theorem ArgumentStructure.toTheme_blocks_unergative {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (body : Event Time → Prop) : ¬IntroMode.toTheme.Licenses (VerbDenot.unergative body)

Diagnostic 1: low (theme-relating) introduction is blocked over an unergative — it has no event-internal theme. Derived from the valence type, not stipulated.

theorem ArgumentStructure.toTheme_blocks_kimian {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (rel : Entity → Entity → Prop) : ¬IntroMode.toTheme.Licenses (VerbDenot.kimianStative rel)

Diagnostic 2: low introduction is blocked over a Kimian stative — distinct reason from Diagnostic 1: no event argument at all ([Mol25]).

theorem ArgumentStructure.toTheme_licenses_transitive {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (themeRel body : ThematicRel Entity Time) : IntroMode.toTheme.Licenses (VerbDenot.transitive themeRel body)

Low introduction is licensed over a Davidsonian transitive (English DOC, Hebrew possessor datives).

theorem ArgumentStructure.low_external_arg_clash {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (agentRel themeRel : ThematicRel Entity Time) (excl : RolesExclusive agentRel themeRel) (x : Entity) (e : Event Time) (hAgent : agentRel x e) (hTheme : themeRel x e) : False

[Pyl08]'s eq. 103, as a theorem about the denotations: forcing a low (theme-relating) applicative onto an unergative binds the applied argument's theme relation to the external argument, yielding agentRel x e ∧ themeRel x e for one participant — contradictory under thematic uniqueness. The transitivity restriction is thus derived, not stipulated.

Cause is not a θ-role ([Pyl08] Ch. 3 §3.2)

def ArgumentStructure.causeBieventive {Time : Type u_2} [LinearOrder Time] (cause : Event Time → Event Time → Prop) (caused : Event Time → Prop) : Event Time → Prop

Bieventive Cause: the causative head relates the described event to a causing event, introducing NO individual. λf.λe. ∃e'. f e' ∧ cause e e'.

Equations

• ArgumentStructure.causeBieventive cause caused e = ∃ (e' : Event Time), caused e' ∧ cause e e'

def ArgumentStructure.causeThetaRole {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (cause : Event Time → Event Time → Prop) (causer : ThematicRel Entity Time) (caused : Event Time → Prop) : ThematicRel Entity Time

The θ-role analysis [Pyl08] argues against: Cause introduces a causer individual. λx.λe. causer x e ∧ ∃e'. f e' ∧ cause e e'.

Equations

• ArgumentStructure.causeThetaRole cause causer caused x e = (causer x e ∧ ∃ (e' : Event Time), caused e' ∧ cause e e')

theorem ArgumentStructure.causeThetaRole_forces_causer {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (cause : Event Time → Event Time → Prop) (causer : ThematicRel Entity Time) (caused : Event Time → Prop) (x : Entity) (e : Event Time) (h : causeThetaRole cause causer caused x e) : causer x e

The θ-role analysis forces an external (causer) participant: its denotation entails causer x e.

theorem ArgumentStructure.causeBieventive_no_external_arg {Time : Type u_2} [LinearOrder Time] (cause : Event Time → Event Time → Prop) (caused : Event Time → Prop) (e e' : Event Time) (hc : caused e') (hcause : cause e e') : causeBieventive cause caused e

The bieventive analysis admits a causative event with NO external participant: given only a causing relation to some caused event, causeBieventive holds without any causer. This is the Japanese adversity causative ([Pyl08] §3.2.2) the θ-role analysis cannot model.