Myler 2016: Building and Interpreting Possession Sentences

[Myl16]

This study file connects the copula theory (Copula.lean) to empirical predictions and cross-linguistic data from [Myl16].

Contents

• Icelandic hafa/eiga (§4.3): two HAVE verbs with bidirectional VI conditioning, formalized as VocabItems
• The two puzzles: injectivity of haveReading (too-many-meanings) and vi_characterization (too-many-structures)
• Cross-module bridges: connections to possession typology ([Sta09b]), Barker's π ([Bar11]), and nominal structure (inalienable/alienable)

Formerly Syntax/Minimalist/Copula.lean, dissolved into its single consumer (the rest of that file — GratificationType, FreeHead, voiceAllosemeForComplement, haveThetaPrediction, … — was dead). The copula v is a semantically vacuous light verb (⟦v⟧ = λx.x); its PF form is HAVE in a transitive-Voice environment, BE elsewhere (HAVE = BE + transitivity).

inductive Myler2016.CopulaForm : Type

The surface realization of the copula, by Vocabulary Insertion.

• have : CopulaForm
• be : CopulaForm

@[implicit_reducible]

instance Myler2016.instDecidableEqCopulaForm : DecidableEq CopulaForm

Equations

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

@[implicit_reducible]

instance Myler2016.instReprCopulaForm : Repr CopulaForm

Equations

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

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

Equations

• Myler2016.instReprCopulaForm.repr Myler2016.CopulaForm.have prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Myler2016.CopulaForm.have")).group prec✝
• Myler2016.instReprCopulaForm.repr Myler2016.CopulaForm.be prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Myler2016.CopulaForm.be")).group prec✝

def Myler2016.copulaVI (voice : Minimalist.VoiceHead) : CopulaForm

[Myl16] (89): v ⇔ HAVE / __Voice{D},φ ; v ⇔ BE / elsewhere. The HAVE environment is transitive Voice — hasD with a thematic, non-passive flavor.

Equations

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

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

The copula VI as competing VocabItems (HAVE specificity 2, BE elsewhere).

Equations

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

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

The VocabItem formulation agrees with copulaVI.

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

HAVE ↔ Voice is transitive (external argument, not PF-only, not passive).

inductive Myler2016.HaveComplement : Type

The complement type of a HAVE sentence ([Myl16] §5).

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

@[implicit_reducible]

instance Myler2016.instDecidableEqHaveComplement : DecidableEq HaveComplement

Equations

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

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

Equations

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

@[implicit_reducible]

instance Myler2016.instReprHaveComplement : Repr HaveComplement

Equations

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

inductive Myler2016.HaveReading : Type

The reading of a HAVE sentence ([Myl16] table (100)).

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

@[implicit_reducible]

instance Myler2016.instDecidableEqHaveReading : DecidableEq HaveReading

Equations

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

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

Equations

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

@[implicit_reducible]

instance Myler2016.instReprHaveReading : Repr HaveReading

Equations

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

def Myler2016.haveReading : HaveComplement → HaveReading

The predicted reading per complement type. The too-many-meanings puzzle is that this is injective (haveReading_injective).

Equations

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

inductive Myler2016.IcelandicHaveVerb : Type

Icelandic has two HAVE verbs (hafa and eiga) that carve up the possession domain based on the DP-internal structure of the complement.

[Myl16] §4.3 / Myler, Sigurðsson & Wood 2014:

• v ⇔ hafa / __Voice{D},φ ___Pred (complement contains PredP)
• v ⇔ eiga / __Voice{D},φ (elsewhere in transitive context)

The distribution:

• eiga: concrete possession, kinship (Poss head mediates, no PP possessor)
• hafa: body parts, abstract (root-introduced relation, PP possessor possible)
• Both work for non-possessive small clause complements (hafa only)

Generalizations: (90a) Clausal possession with eiga only if DP-internal possession CANNOT be expressed with a PP. (90b) Clausal possession with hafa only if DP-internal possession CAN be expressed with a PP.

• hafa : IcelandicHaveVerb
• eiga : IcelandicHaveVerb

@[implicit_reducible]

instance Myler2016.instDecidableEqIcelandicHaveVerb : DecidableEq IcelandicHaveVerb

Equations

• Myler2016.instDecidableEqIcelandicHaveVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Myler2016.instReprIcelandicHaveVerb.repr : IcelandicHaveVerb → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Myler2016.instReprIcelandicHaveVerb : Repr IcelandicHaveVerb

Equations

• Myler2016.instReprIcelandicHaveVerb = { reprPrec := Myler2016.instReprIcelandicHaveVerb.repr }

structure Myler2016.IcelandicPossDP : Type

Does the DP-internal possession use a PP (preposition) to introduce the possessor? This is the bidirectional conditioning environment.

• hasPredP : Bool

  Is there a PredP (small clause) in the DP structure?

• hasPPPossessor : Bool

  Can the possessor be expressed with a PP inside the DP?

def Myler2016.instDecidableEqIcelandicPossDP.decEq (x✝ x✝¹ : IcelandicPossDP) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Myler2016.instDecidableEqIcelandicPossDP : DecidableEq IcelandicPossDP

Equations

• Myler2016.instDecidableEqIcelandicPossDP = Myler2016.instDecidableEqIcelandicPossDP.decEq

def Myler2016.instReprIcelandicPossDP.repr : IcelandicPossDP → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Myler2016.instReprIcelandicPossDP : Repr IcelandicPossDP

Equations

• Myler2016.instReprIcelandicPossDP = { reprPrec := Myler2016.instReprIcelandicPossDP.repr }

def Myler2016.icelandicHaveVI (dp : IcelandicPossDP) : IcelandicHaveVerb

Icelandic VI rule for HAVE verbs. Bidirectional conditioning: looks at both Voice above AND complement below.

Equations

• Myler2016.icelandicHaveVI dp = if dp.hasPredP = true then Myler2016.IcelandicHaveVerb.hafa else Myler2016.IcelandicHaveVerb.eiga

theorem Myler2016.bodyPart_hafa : icelandicHaveVI { hasPredP := true, hasPPPossessor := true } = IcelandicHaveVerb.hafa

Body parts and abstract nouns (PP possessor possible) → hafa.

theorem Myler2016.concrete_eiga : icelandicHaveVI { hasPredP := false, hasPPPossessor := false } = IcelandicHaveVerb.eiga

Concrete and kinship (no PP possessor) → eiga.

theorem Myler2016.eiga_iff_no_pp (dp : IcelandicPossDP) : icelandicHaveVI dp = IcelandicHaveVerb.eiga ↔ dp.hasPredP = false

Generalization (90a): eiga ↔ no PP possessor internally.

theorem Myler2016.hafa_iff_pred (dp : IcelandicPossDP) : icelandicHaveVI dp = IcelandicHaveVerb.hafa ↔ dp.hasPredP = true

Generalization (90b): hafa ↔ PP possessor available internally.

def Myler2016.icelandicHaveVIRules : List (Morphology.DM.VI.VocabItem IcelandicPossDP Unit)

Icelandic HAVE VI as proper VocabItems from the DM framework.

Two items compete via the Elsewhere Condition:

• hafa: specificity 1 (checks hasPredP = true)
• eiga: specificity 0 (elsewhere — matches any transitive context)

This parallels copulaVIRules for the English HAVE/BE alternation, but applies within the HAVE domain: both hafa and eiga realize transitive Voice, differing only in the DP-internal structure.

Equations

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

theorem Myler2016.icelandicVI_agrees_vocabItem (dp : IcelandicPossDP) : Morphology.DM.VI.vocabularyInsertSimple icelandicHaveVIRules dp = some (if icelandicHaveVI dp = IcelandicHaveVerb.hafa then "hafa" else "eiga")

The VocabItem formulation agrees with the direct icelandicHaveVI.

theorem Myler2016.too_many_meanings_solution : Function.Injective haveReading

The "too-many-meanings" puzzle: how can one construction (have) have so many different meanings?

[Myl16] (81): possession constructions can mean so many things because they involve sentencifying a meaning that comes from inside DP. The meanings are a syntactic natural class (all introduced by heads inside DP), not a semantic one. Since v = λx.x, ALL the thematic content comes from the complement and from Voice allosemy.

Formally: haveReading is injective — each complement type produces a distinct reading. This captures the claim that v contributes nothing: the complement alone determines the interpretation.

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

The "too-many-structures" puzzle: how can the same possessive meanings be realized in so many syntactically different ways across languages?

[Myl16] (93): possession relations originate inside DP (root-introduced or Poss-head-introduced). Since v is meaningless and makes no semantic demands, syntax alone decides where the possessor is first-merged. Combined with parametric variation in delayed gratification and the ±D property of functional heads, this generates the full typology from a small set of parameters.

Formally: the HAVE/BE distinction depends only on whether Voice is transitive, which is independent of the possession relation itself.

def Myler2016.isHaveVerbLanguage (voice : Minimalist.VoiceHead) : Bool

[Myl16]'s HAVE = BE + Voice_{D},φ provides the syntactic analysis underlying the have-verb predicative possession strategy from [Sta09b].

A language uses the have-verb strategy iff its possession construction has transitive Voice — exactly the copulaVI condition. Derived from copulaVI, not stipulated independently.

Equations

• Myler2016.isHaveVerbLanguage voice = (Myler2016.copulaVI voice == Myler2016.CopulaForm.have)

theorem Myler2016.haveVerb_from_transitive_voice : isHaveVerbLanguage Minimalist.voiceAgent = true

A language with transitive, θ-assigning Voice produces HAVE.

theorem Myler2016.be_from_intransitive_voice : isHaveVerbLanguage Minimalist.voiceAnticausative = false

A language with intransitive Voice produces BE (locational/existential).

theorem Myler2016.isHaveVerbLanguage_iff_copulaVI (v : Minimalist.VoiceHead) : isHaveVerbLanguage v = true ↔ copulaVI v = CopulaForm.have

isHaveVerbLanguage agrees with copulaVI by construction.

theorem Myler2016.relational_have_requires_pred2 : ArgumentStructure.Relational.NominalInterpType.pred2.hasRelatumSlot ∧ ArgumentStructure.Relational.NominalInterpType.pred2.canTakePossessor

The relational HAVE reading requires the complement DP to have a Pred2 interpretation (either lexically relational or via π-shift). This is exactly NominalInterpType.pred2 from [Bar11].

[Myl16]: "The meanings [of HAVE] are a syntactic natural class: all introduced by heads inside DP." For relational HAVE, the DP must supply a possessor slot — which is what Pred2 provides.

The bridge: relational HAVE ↔ possessedDP complement ↔ NominalInterpType.pred2 (has relatum slot for possessor).

theorem Myler2016.bare_sortal_blocks_relational : ¬ArgumentStructure.Relational.NominalInterpType.pred1.canTakePossessor

Bare sortals (Pred1, no π) cannot appear in relational HAVE: "I have a cloud" requires a contextually supplied relation (π). Without π, the DP has no possessor slot, so no possessive reading.

theorem Myler2016.both_possession_types_allow_have : Morphology.DM.PossessionType.inalienable.possessorPosition.isWithinNP = true ∧ Morphology.DM.PossessionType.alienable.possessorPosition.isWithinNP = false

Delayed gratification connects to the inalienable/alienable distinction from NominalStructure.lean:

• Inalienable possessor (Spec,nP): can undergo delayed gratification to Spec,VoiceP → yields relational HAVE with inalienable reading
• Alienable possessor (Spec,PossP): can undergo delayed gratification to Spec,VoiceP → yields relational HAVE with alienable reading

In both cases, the possessor starts DP-internally and percolates to Spec,VoiceP. The structural position inside DP determines the INTERPRETATION (kinship vs ownership), not whether HAVE surfaces.

theorem Myler2016.possession_type_orthogonal_to_copula : Morphology.DM.PossessionType.inalienable.canAffectGender = true ∧ Morphology.DM.PossessionType.alienable.canAffectGender = false

Inalienable possession is nP-internal (can affect gender under GLH); alienable possession is nP-external (cannot). This is orthogonal to whether the language spells out v as HAVE or BE.