Myler 2016: Building and Interpreting Possession Sentences

@cite{myler-2016}

This study file connects the copula theory (Copula.lean) to empirical predictions and cross-linguistic data from @cite{myler-2016}.

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 (@cite{stassen-2009}), Barker's π (@cite{barker-2011}), and nominal structure (inalienable/alienable)

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.

@cite{myler-2016} §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?

@[implicit_reducible]

instance Myler2016.instDecidableEqIcelandicPossDP : DecidableEq IcelandicPossDP

Equations

• Myler2016.instDecidableEqIcelandicPossDP = Myler2016.instDecidableEqIcelandicPossDP.decEq

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.instReprIcelandicPossDP : Repr IcelandicPossDP

Equations

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

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

Equations

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

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 Minimalist.haveReading

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

@cite{myler-2016} (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) : Minimalist.copulaVI v = Minimalist.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?

@cite{myler-2016} (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

@cite{myler-2016}'s HAVE = BE + Voice_{D},φ provides the syntactic analysis underlying the have-verb predicative possession strategy from @cite{stassen-2009}.

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 = (Minimalist.copulaVI voice == Minimalist.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 ↔ Minimalist.copulaVI v = Minimalist.CopulaForm.have

isHaveVerbLanguage agrees with copulaVI by construction.

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

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 @cite{barker-2011}.

@cite{myler-2016}: "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 : Semantics.ArgumentStructure.Relational.NominalInterpType.pred1.canTakePossessor = false

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.