Copula Theory: HAVE, BE, and Delayed Gratification

@cite{myler-2016} @cite{freeze-1992} @cite{kayne-1993} @cite{wood-2015}

@cite{myler-2016} proposes that the copula verb (v) is a semantically vacuous light verb: ⟦v⟧ = λx.x. The PF realization of v is determined by Vocabulary Insertion sensitive to the syntactic environment:

• v ⇔ HAVE / __Voice{D},φ (transitive Voice with a DP specifier)
• v ⇔ BE / elsewhere

This captures HAVE = BE + transitivity: have is the spell-out of v in the environment of transitive, external-argument-introducing Voice.

Delayed Gratification

A DP can satisfy a θ-role introduced by a head X without being merged in Spec,XP. Instead, the DP merges higher in the structure and the θ-role percolates up via λ-abstraction until it finds its argument. This is delayed gratification — distinct from both raising (which involves a syntactic copy/trace in the lower position) and control (which involves PRO). In delayed gratification, there is no syntactic representation of the argument in the lower position at all.

This mechanism is the key to the "too-many-structures" puzzle: since possession relations originate inside DP and the possessor role can be gratified at any position in the clausal spine, the cross-linguistic variation in possession constructions reduces to where in the structure the possessor is first-merged.

FreeP (@cite{myler-2016} §4.1.1.3)

The Free head introduces an experiencer θ-role in eventive have constructions. Like Voice, Free varies cross-linguistically in whether it requires a specifier:

• Free_{} (English): cannot project a specifier → experiencer role must be gratified higher (delayed gratification → experiencer HAVE)
• Free_{D} (Spanish): must project a specifier → free datives exist, but eventive experiencer HAVE is blocked (specifier consumes the role)

inductive Minimalist.CopulaForm : Type

The surface realization of the copula, determined by Vocabulary Insertion.

• have : CopulaForm
• be : CopulaForm

@[implicit_reducible]

instance Minimalist.instDecidableEqCopulaForm : DecidableEq CopulaForm

Equations

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

@[implicit_reducible]

instance Minimalist.instReprCopulaForm : Repr CopulaForm

Equations

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

def Minimalist.instReprCopulaForm.repr : CopulaForm → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.instReprCopulaForm.repr Minimalist.CopulaForm.be prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.CopulaForm.be")).group prec✝

def Minimalist.copulaVI (voice : VoiceHead) : CopulaForm

Vocabulary Insertion rule for the copula.

@cite{myler-2016} (89):

• v ⇔ HAVE / __Voice{D},φ
• v ⇔ BE / elsewhere

The conditioning environment is transitive Voice: Voice that introduces an external argument (has a DP specifier with φ-features). This is exactly the hasD property of VoiceHead.

Equations

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

def Minimalist.copulaVIRules : List (Morphology.DM.VI.VocabItem VoiceHead Unit)

The copula VI rule as a proper VocabItem from the DM VI framework.

Two items compete via the Elsewhere Condition:

• HAVE: specificity 2 (checks hasD = true AND flavor ∉ {nonThematic, passive})
• BE: specificity 0 (elsewhere — matches any context)

vocabularyInsertSimple copulaVIRules voice agrees with copulaVI voice.

Equations

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

theorem Minimalist.copulaVI_agrees_vocabItem (v : VoiceHead) : Morphology.DM.VI.vocabularyInsertSimple copulaVIRules v = some (if copulaVI v = CopulaForm.have then "have" else "be")

The VocabItem formulation agrees with the direct copulaVI function: "have" is inserted iff copulaVI returns .have.

theorem Minimalist.vi_agent_have : copulaVI voiceAgent = CopulaForm.have

HAVE in the environment of agentive Voice.

theorem Minimalist.vi_causer_have : copulaVI voiceCauser = CopulaForm.have

HAVE in the environment of causer Voice.

theorem Minimalist.vi_experiencer_have : copulaVI voiceExperiencer = CopulaForm.have

HAVE in the environment of experiencer Voice.

theorem Minimalist.vi_middle_be : copulaVI voiceMiddle = CopulaForm.be

BE in the environment of middle/expletive Voice.

theorem Minimalist.vi_anticausative_be : copulaVI voiceAnticausative = CopulaForm.be

BE in the environment of non-thematic Voice (anticausative).

theorem Minimalist.vi_passive_be : copulaVI voicePassive = CopulaForm.be

BE in the environment of passive Voice.

theorem Minimalist.vi_characterization (v : VoiceHead) : copulaVI v = CopulaForm.have ↔ v.hasD = true ∧ v.flavor ≠ VoiceFlavor.nonThematic ∧ v.flavor ≠ VoiceFlavor.passive

The VI rule is equivalent to: HAVE ↔ Voice is transitive (has external argument that is not a PF-only marker and not a passive).

inductive Minimalist.GratificationType : Type

How a θ-role introduced by a head X is satisfied.

@cite{myler-2016} §1.3 (69–73) distinguishes three mechanisms:

• Instant: the DP merges in Spec,XP — the standard case. The DP is both the syntactic and semantic argument of X.
• Delayed: the DP merges higher in the structure (e.g., Spec,YP where Y ≠ X). The θ-role of X percolates up via λ-abstraction and is eventually saturated. There is NO syntactic representation of the argument in the lower Spec,XP position.
• Raising: the DP is base-generated in Spec,XP (or a copy/trace is left there) and moves to a higher position. Unlike delayed gratification, there IS a syntactic reflex in the lower position.

Delayed gratification is the key to Myler's account: possession relations originate DP-internally (in Spec,nP for inalienable, in Spec,PossP for alienable), but the possessor can be gratified at any point in the clausal spine — Spec,PredP, Spec,ApplP, Spec,VoiceP. The variation in WHERE gratification occurs generates the cross-linguistic typology of possession constructions.

• instant : GratificationType
• delayed : GratificationType
• raising : GratificationType

@[implicit_reducible]

instance Minimalist.instDecidableEqGratificationType : DecidableEq GratificationType

Equations

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

def Minimalist.instReprGratificationType.repr : GratificationType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprGratificationType : Repr GratificationType

Equations

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

def Minimalist.GratificationType.hasSyntacticReflexBelow : GratificationType → Bool

Does this gratification type leave a syntactic reflex in the lower (base) position? This is the key difference between delayed gratification and raising/control.

Equations

• Minimalist.GratificationType.instant.hasSyntacticReflexBelow = true
• Minimalist.GratificationType.delayed.hasSyntacticReflexBelow = false
• Minimalist.GratificationType.raising.hasSyntacticReflexBelow = true

def Minimalist.GratificationType.argumentMovesUp : GratificationType → Bool

Does the argument end up higher than the θ-assigning head?

Equations

• Minimalist.GratificationType.instant.argumentMovesUp = false
• Minimalist.GratificationType.delayed.argumentMovesUp = true
• Minimalist.GratificationType.raising.argumentMovesUp = true

theorem Minimalist.delayed_unique : GratificationType.delayed.argumentMovesUp = true ∧ GratificationType.delayed.hasSyntacticReflexBelow = false

Delayed gratification is unique: the argument moves up but leaves no syntactic reflex. This has consequences for agreement, scope, and intervention — none of the effects triggered by a DP in the lower position arise.

theorem Minimalist.raising_has_both : GratificationType.raising.argumentMovesUp = true ∧ GratificationType.raising.hasSyntacticReflexBelow = true

Raising has BOTH syntactic reflex and upward movement. This is what distinguishes it from delayed gratification.

structure Minimalist.FreeHead : Type

The Free head introduces an experiencer θ-role above an embedded VoiceP.

@cite{myler-2016} §4.1.1.3: Free is a functional head that merges above the embedded VoiceP inside have's complement. It is related to but distinct from Appl:

• Like high Appl, Free relates an individual to an event
• Unlike Appl, Free introduces specifically an experiencer role
• Free's specifier behavior varies cross-linguistically (±D)

The ±D parameter on Free generates the English/Spanish asymmetry:

• Free_{} (English): no specifier → delayed gratification → experiencer HAVE exists, free datives do not
• Free_{D} (Spanish): specifier required → instant gratification → free datives exist, eventive experiencer HAVE does not

@cite{myler-2016} table (35): | Free heads | Phenomena | Languages | |-------------|-------------------------------------|--------------| | Free_{} | Eventive Exp HAVE, No free datives | English | | Free_{D} | No Eventive Exp HAVE, Free datives | Spanish | | Both | Both | None known | | None | Neither | None known |

• hasD : Bool

  Does Free require a specifier (DP)?

@[implicit_reducible]

instance Minimalist.instDecidableEqFreeHead : DecidableEq FreeHead

Equations

• Minimalist.instDecidableEqFreeHead = Minimalist.instDecidableEqFreeHead.decEq

def Minimalist.instDecidableEqFreeHead.decEq (x✝ x✝¹ : FreeHead) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqFreeHead.decEq { hasD := a } { hasD := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Minimalist.instReprFreeHead.repr : FreeHead → ℕ → Std.Format

Equations

• Minimalist.instReprFreeHead.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "hasD" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.hasD)).group) " }"

@[implicit_reducible]

instance Minimalist.instReprFreeHead : Repr FreeHead

Equations

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

def Minimalist.freeNoSpec : FreeHead

English-type Free: cannot take a specifier. The experiencer role introduced by Free must be gratified higher, via delayed gratification to Spec,VoiceP → yields experiencer HAVE.

Equations

• Minimalist.freeNoSpec = { hasD := false }

def Minimalist.freeWithSpec : FreeHead

Spanish-type Free: must take a specifier. The experiencer role is gratified instantly in Spec,FreeP → yields free datives. But delayed gratification to Spec,VoiceP is blocked (the role is already consumed) → no eventive experiencer HAVE.

Equations

• Minimalist.freeWithSpec = { hasD := true }

def Minimalist.FreeHead.allowsDelayedGratification (f : FreeHead) : Bool

Does this Free head allow delayed gratification of its experiencer role to a higher position?

If Free has a specifier ({D}), the role is gratified instantly and cannot percolate further. If Free lacks a specifier ({}), the role remains unsaturated and percolates up.

Equations

• f.allowsDelayedGratification = !f.hasD

def Minimalist.FreeHead.yieldsFreeOrDative (f : FreeHead) : Bool

Does this Free head yield free datives? Free datives arise when the experiencer merges in Spec,FreeP.

Equations

• f.yieldsFreeOrDative = f.hasD

def Minimalist.FreeHead.yieldsEventiveExpHave (f : FreeHead) : Bool

Does this Free head yield eventive experiencer HAVE? Eventive experiencer HAVE arises when the experiencer role percolates to Spec,VoiceP via delayed gratification.

Derived from allowsDelayedGratification: experiencer HAVE exists iff Free's θ-role can percolate (not consumed locally).

Equations

• f.yieldsEventiveExpHave = f.allowsDelayedGratification

theorem Minimalist.english_free_pattern : freeNoSpec.yieldsEventiveExpHave = true ∧ freeNoSpec.yieldsFreeOrDative = false

English: eventive experiencer HAVE, no free datives.

theorem Minimalist.spanish_free_pattern : freeWithSpec.yieldsEventiveExpHave = false ∧ freeWithSpec.yieldsFreeOrDative = true

Spanish: free datives, no eventive experiencer HAVE.

theorem Minimalist.free_complementarity (f : FreeHead) : f.yieldsEventiveExpHave = !f.yieldsFreeOrDative

The complementarity: for any Free head, exactly one of eventive experiencer HAVE and free datives is available.

inductive Minimalist.HaveComplement : Type

The complement of have (= the complement of v_BE).

@cite{myler-2016} table (100): the interpretation of a HAVE sentence depends on the interaction between the complement type and the Voice alloseme selected. The complement types are:

• possessedDP: a DP containing a possession relation (relational noun or Poss head). Voice is expletive → relational HAVE.
• eventDP: a DP denoting an event (light-verb HAVE: "had a bath"). Voice assigns agent/holder.
• saturatedEventiveVoiceP: a full VoiceP with an agent and event (engineer HAVE: "had John bathe the dog"). Voice selects engineer alloseme.
• stativeSC: a stative small clause — PredP, AP, PP (causer HAVE: "had me angry"; locative HAVE: "has nests in it"). Voice selects holder/causer.
• freeP: a FreeP embedding a VoiceP (experiencer HAVE: "had Johnny run off on us"). Voice is expletive; Free introduces the experiencer role.
• modalBase: a DP/set of worlds (modal HAVE: "has to leave"). Semantics is world-containment, not individual-event.

• possessedDP : HaveComplement
• eventDP : HaveComplement
• saturatedEventiveVoiceP : HaveComplement
• stativeSC : HaveComplement
• freeP : HaveComplement
• modalBase : HaveComplement

@[implicit_reducible]

instance Minimalist.instDecidableEqHaveComplement : DecidableEq HaveComplement

Equations

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

@[implicit_reducible]

instance Minimalist.instReprHaveComplement : Repr HaveComplement

Equations

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

def Minimalist.instReprHaveComplement.repr : HaveComplement → ℕ → Std.Format

Equations

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

def Minimalist.HaveComplement.IsEventive : HaveComplement → Prop

Is the complement eventive? This conditions Voice alloseme selection.

Equations

• Minimalist.HaveComplement.saturatedEventiveVoiceP.IsEventive = True
• Minimalist.HaveComplement.eventDP.IsEventive = True
• Minimalist.HaveComplement.freeP.IsEventive = True
• Minimalist.HaveComplement.possessedDP.IsEventive = False
• Minimalist.HaveComplement.stativeSC.IsEventive = False
• Minimalist.HaveComplement.modalBase.IsEventive = False

@[implicit_reducible]

instance Minimalist.instDecidablePredHaveComplementIsEventive : DecidablePred HaveComplement.IsEventive

Equations

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

def Minimalist.HaveComplement.IsStativePredicate (c : HaveComplement) : Prop

Is the complement a stative predication (small clause)? This is the condition for the holder/causer Voice alloseme: Voice assigns a holder role when it combines with a stative predicate (AP, PP, PredP).

Crucially, possessedDP and modalBase are NOT stative predicates from Voice's perspective — the possession relation originates DP-internally and Voice is vacuous (expletive).

Equations

• c.IsStativePredicate = (c = Minimalist.HaveComplement.stativeSC)

@[implicit_reducible]

instance Minimalist.instDecidablePredHaveComplementIsStativePredicate : DecidablePred HaveComplement.IsStativePredicate

Equations

• Minimalist.instDecidablePredHaveComplementIsStativePredicate x✝ = Minimalist.instDecidablePredHaveComplementIsStativePredicate._aux_1 x✝

def Minimalist.HaveComplement.IsSaturatedEventiveVoiceP (c : HaveComplement) : Prop

Is the complement a saturated eventive VoiceP? This is the most specific environment: a full clause with its own agent and event, triggering the engineer alloseme.

Equations

• c.IsSaturatedEventiveVoiceP = (c = Minimalist.HaveComplement.saturatedEventiveVoiceP)

@[implicit_reducible]

instance Minimalist.instDecidablePredHaveComplementIsSaturatedEventiveVoiceP : DecidablePred HaveComplement.IsSaturatedEventiveVoiceP

Equations

• Minimalist.instDecidablePredHaveComplementIsSaturatedEventiveVoiceP x✝ = Minimalist.instDecidablePredHaveComplementIsSaturatedEventiveVoiceP._aux_1 x✝

def Minimalist.HaveComplement.IsEventDP (c : HaveComplement) : Prop

Is the complement an eventive DP (not a full VoiceP)? Event-denoting DPs (light-verb HAVE: "had a bath") trigger agentive Voice, unlike FreeP (which triggers expletive Voice).

Equations

• c.IsEventDP = (c = Minimalist.HaveComplement.eventDP)

@[implicit_reducible]

instance Minimalist.instDecidablePredHaveComplementIsEventDP : DecidablePred HaveComplement.IsEventDP

Equations

• Minimalist.instDecidablePredHaveComplementIsEventDP x✝ = Minimalist.instDecidablePredHaveComplementIsEventDP._aux_1 x✝

inductive Minimalist.HaveReading : Type

The reading (interpretation) of a HAVE sentence.

• relational : HaveReading
• lightVerb : HaveReading
• engineer : HaveReading
• causer : HaveReading
• experiencerEventive : HaveReading
• experiencerStative : HaveReading
• locative : HaveReading
• temporaryPossession : HaveReading
• modal : HaveReading

@[implicit_reducible]

instance Minimalist.instDecidableEqHaveReading : DecidableEq HaveReading

Equations

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

def Minimalist.instReprHaveReading.repr : HaveReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprHaveReading : Repr HaveReading

Equations

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

def Minimalist.voiceAllosemeForComplement (c : HaveComplement) : Morphology.DM.Allosemy.VoiceAlloseme

@cite{myler-2016} table (100): Which Voice alloseme is selected given a particular complement type.

Derived from complement properties via VoiceAlloseme.fromComplement (Allosemy.lean), with one extension: event-denoting DPs (light-verb HAVE) trigger the agent alloseme, which fromComplement does not cover (it only distinguishes saturated VoiceP from stative from elsewhere).

The cascade:

1. Saturated eventive VoiceP → engineer (most specific)
2. Event-denoting DP → agent (eventive but not a VoiceP)
3. Stative SC → holder (stative predicate)
4. Elsewhere (possessedDP, FreeP, modalBase) → expletive (Voice is vacuous)

Equations

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

theorem Minimalist.voiceAlloseme_agrees_fromComplement (c : HaveComplement) (hNotEventDP : ¬c.IsEventDP) : voiceAllosemeForComplement c = Morphology.DM.Allosemy.VoiceAlloseme.fromComplement c.IsSaturatedEventiveVoiceP c.IsStativePredicate

The non-eventDP cases agree with VoiceAlloseme.fromComplement: when the complement is not an event-denoting DP, the alloseme can be derived purely from the IsSaturatedEventiveVoiceP and IsStativePredicate properties — which is exactly what fromComplement does.

def Minimalist.haveReading : HaveComplement → HaveReading

The predicted reading for each complement type.

Equations

• Minimalist.haveReading Minimalist.HaveComplement.possessedDP = Minimalist.HaveReading.relational
• Minimalist.haveReading Minimalist.HaveComplement.eventDP = Minimalist.HaveReading.lightVerb
• Minimalist.haveReading Minimalist.HaveComplement.saturatedEventiveVoiceP = Minimalist.HaveReading.engineer
• Minimalist.haveReading Minimalist.HaveComplement.stativeSC = Minimalist.HaveReading.causer
• Minimalist.haveReading Minimalist.HaveComplement.freeP = Minimalist.HaveReading.experiencerEventive
• Minimalist.haveReading Minimalist.HaveComplement.modalBase = Minimalist.HaveReading.modal

theorem Minimalist.relational_have_expletive : voiceAllosemeForComplement HaveComplement.possessedDP = Morphology.DM.Allosemy.VoiceAlloseme.expletive

Relational HAVE: Voice is expletive; meaning = complement's meaning.

theorem Minimalist.lightVerb_have_agentive : voiceAllosemeForComplement HaveComplement.eventDP = Morphology.DM.Allosemy.VoiceAlloseme.agent

Light-verb HAVE: Voice is agentive; meaning = complement + agent.

theorem Minimalist.engineer_have_from_voiceP : voiceAllosemeForComplement HaveComplement.saturatedEventiveVoiceP = Morphology.DM.Allosemy.VoiceAlloseme.engineer

Engineer HAVE: saturated eventive VoiceP triggers engineer alloseme.

theorem Minimalist.causer_have_from_stativeSC : voiceAllosemeForComplement HaveComplement.stativeSC = Morphology.DM.Allosemy.VoiceAlloseme.holder

Causer HAVE: stative SC triggers holder alloseme.

theorem Minimalist.experiencer_have_from_freeP : voiceAllosemeForComplement HaveComplement.freeP = Morphology.DM.Allosemy.VoiceAlloseme.expletive

Experiencer HAVE: FreeP triggers expletive Voice (Free does the θ-work).

theorem Minimalist.modal_have_expletive : voiceAllosemeForComplement HaveComplement.modalBase = Morphology.DM.Allosemy.VoiceAlloseme.expletive

Modal HAVE: modal base triggers expletive Voice.

theorem Minimalist.agent_blocked_by_stativeSC : voiceAllosemeForComplement HaveComplement.stativeSC ≠ Morphology.DM.Allosemy.VoiceAlloseme.agent

Agent + stative SC = * : agentive Voice requires a dynamic event, but a stative SC does not provide one.

theorem Minimalist.engineer_only_from_voiceP (c : HaveComplement) : voiceAllosemeForComplement c = Morphology.DM.Allosemy.VoiceAlloseme.engineer → c = HaveComplement.saturatedEventiveVoiceP

Engineer is ONLY available with saturated eventive VoiceP. All other complement types yield a different alloseme.

theorem Minimalist.expletive_voice_complement_determines_meaning (c : HaveComplement) : voiceAllosemeForComplement c = Morphology.DM.Allosemy.VoiceAlloseme.expletive → c = HaveComplement.possessedDP ∨ c = HaveComplement.freeP ∨ c = HaveComplement.modalBase

When Voice is expletive (relational, experiencer, modal HAVE), the meaning comes entirely from the complement — Voice contributes nothing. This is the "meaning = complement's meaning" generalization.

def Minimalist.haveThetaPrediction (c : HaveComplement) : Option ThetaRole

The complete theta-role prediction chain for HAVE sentences:

HaveComplement → VoiceAlloseme → VoiceFlavor → Option ThetaRole

This composes three independently motivated mappings:

1. Complement type determines Voice alloseme (§5, table (100))
2. Alloseme maps to syntactic VoiceFlavor (Allosemy.lean)
3. VoiceFlavor.thetaRole determines theta role (Voice.lean)

The result: each HAVE reading predicts a specific external θ-role (or none, for expletive Voice).

Equations

• Minimalist.haveThetaPrediction c = (Minimalist.voiceAllosemeForComplement c).toFlavor.thetaRole

theorem Minimalist.lightVerb_assigns_agent : haveThetaPrediction HaveComplement.eventDP = some ThetaRole.agent

Light-verb HAVE assigns agent.

theorem Minimalist.engineer_assigns_agent : haveThetaPrediction HaveComplement.saturatedEventiveVoiceP = some ThetaRole.agent

Engineer HAVE assigns agent (to the "engineer" orchestrator).

theorem Minimalist.causer_assigns_experiencer : haveThetaPrediction HaveComplement.stativeSC = some ThetaRole.experiencer

Causer HAVE assigns experiencer (holder alloseme → experiencer flavor).

theorem Minimalist.relational_no_theta : haveThetaPrediction HaveComplement.possessedDP = none

Relational HAVE assigns no theta role (expletive Voice).

theorem Minimalist.experiencer_theta_from_free_not_voice : haveThetaPrediction HaveComplement.freeP = none

Experiencer HAVE (FreeP) assigns no theta role from Voice (the experiencer role comes from Free, not Voice).

theorem Minimalist.modal_no_theta : haveThetaPrediction HaveComplement.modalBase = none

Modal HAVE assigns no theta role.

def Minimalist.nominalAllowsDelayedGratification (v : Morphology.DM.Allosemy.VAlloseme) : Bool

Whether a nominal (DP complement of HAVE) can undergo delayed gratification — i.e., can its possessor role percolate up to be gratified at Spec,VoiceP?

@cite{myler-2016} §4.1.2.1 observes that complex event nominals (CENs) resist delayed gratification and thus cannot appear in relational have constructions:

• • John had a/the destruction of the city.
• • The city had a/the destruction.

The reason: CENs contain a v head (verbal substructure), and v forces instant gratification — the possessor must be realized DP-internally. In contrast, simplex event nominals (SENs) and relational nouns lack v, so their possessor role can percolate.

Derived from v allosemy (Allosemy.lean): VAlloseme.introducesEvent is the independently motivated property that determines whether v contributes an event variable. When v is eventive, the DP has verbal substructure that blocks delayed gratification. When v is zero (identity), delayed gratification is available.

Equations

• Minimalist.nominalAllowsDelayedGratification v = !v.introducesEvent

theorem Minimalist.relational_allows_delayed : nominalAllowsDelayedGratification Morphology.DM.Allosemy.VAlloseme.zero = true

Relational nouns (v = zero, no event variable) allow delayed gratification.

theorem Minimalist.cen_blocks_delayed : nominalAllowsDelayedGratification Morphology.DM.Allosemy.VAlloseme.eventive = false

CENs (v = eventive, introduces event variable) block delayed gratification.

theorem Minimalist.delayed_gratification_iff_no_event (v : Morphology.DM.Allosemy.VAlloseme) : nominalAllowsDelayedGratification v = !v.introducesEvent

The bridge: delayed gratification is blocked iff v introduces an event. This derives the CEN restriction from the allosemy framework rather than stipulating it as a separate parameter.