Docs / Syntax / Minimalist / Verbal / Voice / Denotation

The denotation of Voice

import Linglib.Syntax.Minimalist.Verbal.Voice.Denotation · namespace Minimalist.Voice.Head

Source

Every Voice head has a denotation, read off its cell. Thematic Voice whose variable a specifier saturates denotes the relation its instruction names between the individual it introduces and an eventuality, of type ⟨e,⟨v,t⟩⟩; thematic Voice without a specifier, the passive, binds its variable existentially, a predicate of eventualities of type ⟨v,t⟩; and expletive Voice adds no semantics to the verb phrase it combines with, the identity on predicates of eventualities. The relations are a model's, one per instruction, so a study that interprets a Minimalist object supplies the model, not the head's meaning. Merged with a verb phrase that denotes a predicate P of eventualities, whatever P is, a thematic head adds its argument by Event Identification, the passive head conjoins the existentially bound relation with P, and an expletive head leaves P as it is: the external argument is not an argument of the verb.

References

Declarations

L43–50

A thematic head with its variable saturated, merged with a verb phrase that denotes the predicate P of eventualities, denotes its relation conjoined with P at the eventuality, by Event Identification.

theorem interp_toTree_leaf_mulL67–75
{E W : Type} {S : Montague.Sorts} (ρ : Instruction → E → S.eventuality → Prop) {L : Type} (ι : L → ℕ) {lex : L → Option (Montague.Denotation E W Id S)} {g : Assignment E} {v : L} {vp : LinearizedSyntacticObject L} {h : Head} {P : S.eventuality → Prop} {i : Instruction} (hv : lex v = some (denote ρ h)) (hi : h.thematic = some i) (hn : h.implicit = false) (hvp : PhraseStructure.Tree.interp lex g (LinearizedSyntacticObject.toTree ι vp) = some ⟨Montague.Ty.v.fn Montague.Ty.t, P⟩) :
PhraseStructure.Tree.interp lex g (LinearizedSyntacticObject.toTree ι (↑v * vp)) = some ⟨Montague.Ty.e.fn (Montague.Ty.v.fn Montague.Ty.t), ArgumentStructure.eventIdentification (ρ i) P⟩

Built from

A thematic head with its variable implicit, merged with a verb phrase that denotes the predicate P of eventualities, denotes the eventualities of P that its relation relates some individual to, by Predicate Modification.

theorem interp_toTree_leaf_mul_of_implicitL77–86
{E W : Type} {S : Montague.Sorts} (ρ : Instruction → E → S.eventuality → Prop) {L : Type} (ι : L → ℕ) {lex : L → Option (Montague.Denotation E W Id S)} {g : Assignment E} {v : L} {vp : LinearizedSyntacticObject L} {h : Head} {P : S.eventuality → Prop} {i : Instruction} (hv : lex v = some (denote ρ h)) (hi : h.thematic = some i) (hn : h.implicit = true) (hvp : PhraseStructure.Tree.interp lex g (LinearizedSyntacticObject.toTree ι vp) = some ⟨Montague.Ty.v.fn Montague.Ty.t, P⟩) :
PhraseStructure.Tree.interp lex g (LinearizedSyntacticObject.toTree ι (↑v * vp)) = some ⟨Montague.Ty.v.fn Montague.Ty.t, fun (e : Montague.Ty.Domain E W Montague.Ty.v S) => (∃ (x : E), ρ i x e) ∧ P e⟩

Built from

An expletive head merged with a verb phrase that denotes the predicate P of eventualities denotes P.

theorem interp_toTree_leaf_mul_of_expletiveL88–93
{E W : Type} {S : Montague.Sorts} (ρ : Instruction → E → S.eventuality → Prop) {L : Type} (ι : L → ℕ) {lex : L → Option (Montague.Denotation E W Id S)} {g : Assignment E} {v : L} {vp : LinearizedSyntacticObject L} {h : Head} {P : S.eventuality → Prop} (hv : lex v = some (denote ρ h)) (hi : h.thematic = none) (hvp : PhraseStructure.Tree.interp lex g (LinearizedSyntacticObject.toTree ι vp) = some ⟨Montague.Ty.v.fn Montague.Ty.t, P⟩) :
PhraseStructure.Tree.interp lex g (LinearizedSyntacticObject.toTree ι (↑v * vp)) = some ⟨Montague.Ty.v.fn Montague.Ty.t, P⟩

Built from