Heine (1997): Possession — Cognitive Sources, Forces, and Grammaticalization

@cite{heine-1997}

Bernd Heine. Possession: Cognitive Sources, Forces, and Grammaticalization. Cambridge Studies in Linguistics 83. Cambridge University Press, 1997.

Core claims

1. Predicative possession constructions worldwide derive from a small set of eight cognitive event schemas (Table 2.1), each with a fixed propositional structure that predicts the resulting word order and case marking.

2. Each schema has characteristic contrastive properties (Table 2.3): whether its predicate nucleus is lexical (Action only) or non-lexical, whether its structure is basic or extended, and which participant (possessor or possessee) maps to clausal subject.

3. Schemas correlate with possessive notions (Table 2.4): Location invariably yields have-constructions; Equation invariably yields belong-constructions; Action and Goal can yield both.

4. Grammaticalization proceeds via the Overlap Model: Stage I (source meaning only) → Stage II (source + target overlap) → Stage III (target meaning only).

5. A 100-language survey (Table 2.2) shows schemas are distributed across all continents with Location (20.9%) and Goal (20.0%) as the most common sources, and Action (13.6%) less common than often assumed.

Connections

• Typology.Possession.PossessionSource: the eight schemas (substrate)
• Typology.Possession.PossessiveNotion: the seven target notions (substrate)
• Theories.Diachronic.Grammaticalization.GramStage: the verbal cline
• Theories.Semantics.ArgumentStructure.Relational: π operator and arity tracking — connects to which schemas have possessor-as-subject (Action, Companion = transitive/Pred2) vs possessee-as-subject (rest)

def Heine1997.schemaHasLexicalNucleus : Typology.Possession.PossessionSource → Bool

Whether the predicate nucleus of a schema retains lexical content. Action is unique: its predicate nucleus is a lexical verb ('take', 'seize', 'hold'). All other schemas have non-lexical nuclei (copulas, existentials, locative verbs).

Equations

• Heine1997.schemaHasLexicalNucleus Typology.Possession.PossessionSource.action = true
• Heine1997.schemaHasLexicalNucleus x✝ = false

inductive Heine1997.SourceStructure : Type

Whether the source structure is basic (two core arguments) or extended (basic structure + an additional oblique participant grafted on). Action and Location are basic; the remaining five involve extending a simpler structure with an additional case-marked participant.

• basic : SourceStructure
• extended : SourceStructure

@[implicit_reducible]

instance Heine1997.instDecidableEqSourceStructure : DecidableEq SourceStructure

Equations

• Heine1997.instDecidableEqSourceStructure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Heine1997.instReprSourceStructure : Repr SourceStructure

Equations

• Heine1997.instReprSourceStructure = { reprPrec := Heine1997.instReprSourceStructure.repr }

def Heine1997.instReprSourceStructure.repr : SourceStructure → ℕ → Std.Format

Equations

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

def Heine1997.schemaStructure : Typology.Possession.PossessionSource → SourceStructure

Equations

• Heine1997.schemaStructure Typology.Possession.PossessionSource.action = Heine1997.SourceStructure.basic
• Heine1997.schemaStructure Typology.Possession.PossessionSource.location = Heine1997.SourceStructure.basic
• Heine1997.schemaStructure Typology.Possession.PossessionSource.companion = Heine1997.SourceStructure.extended
• Heine1997.schemaStructure Typology.Possession.PossessionSource.genitive = Heine1997.SourceStructure.extended
• Heine1997.schemaStructure Typology.Possession.PossessionSource.goal = Heine1997.SourceStructure.extended
• Heine1997.schemaStructure Typology.Possession.PossessionSource.source = Heine1997.SourceStructure.extended
• Heine1997.schemaStructure Typology.Possession.PossessionSource.topic = Heine1997.SourceStructure.extended
• Heine1997.schemaStructure Typology.Possession.PossessionSource.equation = Heine1997.SourceStructure.extended

inductive Heine1997.SubjectParticipant : Type

Which participant of the source schema is encoded as the clausal subject. Action and Companion encode the possessor as subject; all others encode the possessee as subject.

• possessor : SubjectParticipant
• possessee : SubjectParticipant

@[implicit_reducible]

instance Heine1997.instDecidableEqSubjectParticipant : DecidableEq SubjectParticipant

Equations

• Heine1997.instDecidableEqSubjectParticipant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Heine1997.instReprSubjectParticipant.repr : SubjectParticipant → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Heine1997.instReprSubjectParticipant : Repr SubjectParticipant

Equations

• Heine1997.instReprSubjectParticipant = { reprPrec := Heine1997.instReprSubjectParticipant.repr }

def Heine1997.schemaSubject : Typology.Possession.PossessionSource → SubjectParticipant

Equations

• Heine1997.schemaSubject Typology.Possession.PossessionSource.action = Heine1997.SubjectParticipant.possessor
• Heine1997.schemaSubject Typology.Possession.PossessionSource.companion = Heine1997.SubjectParticipant.possessor
• Heine1997.schemaSubject Typology.Possession.PossessionSource.location = Heine1997.SubjectParticipant.possessee
• Heine1997.schemaSubject Typology.Possession.PossessionSource.genitive = Heine1997.SubjectParticipant.possessee
• Heine1997.schemaSubject Typology.Possession.PossessionSource.goal = Heine1997.SubjectParticipant.possessee
• Heine1997.schemaSubject Typology.Possession.PossessionSource.source = Heine1997.SubjectParticipant.possessee
• Heine1997.schemaSubject Typology.Possession.PossessionSource.topic = Heine1997.SubjectParticipant.possessee
• Heine1997.schemaSubject Typology.Possession.PossessionSource.equation = Heine1997.SubjectParticipant.possessee

theorem Heine1997.action_unique_lexical (s : Typology.Possession.PossessionSource) : schemaHasLexicalNucleus s = true → s = Typology.Possession.PossessionSource.action

Only Action has a lexical predicate nucleus.

theorem Heine1997.possessor_subject_iff_action_or_companion (s : Typology.Possession.PossessionSource) : schemaSubject s = SubjectParticipant.possessor ↔ s = Typology.Possession.PossessionSource.action ∨ s = Typology.Possession.PossessionSource.companion

Only Action and Companion have possessor-as-subject.

theorem Heine1997.basic_iff_action_or_location (s : Typology.Possession.PossessionSource) : schemaStructure s = SourceStructure.basic ↔ s = Typology.Possession.PossessionSource.action ∨ s = Typology.Possession.PossessionSource.location

Basic schemas are exactly Action and Location.

def Heine1997.schemaYieldsHave : Typology.Possession.PossessionSource → Bool

Whether a schema gives rise to a have-construction ('X has Y'), a belong-construction ('Y belongs to X'), or both. Location → have only. Equation → belong only. Action and Goal → both. Companion, Genitive, Topic → have only. Source → irrelevant for predicative possession (provides attributive possession source).

Equations

• Heine1997.schemaYieldsHave Typology.Possession.PossessionSource.action = true
• Heine1997.schemaYieldsHave Typology.Possession.PossessionSource.location = true
• Heine1997.schemaYieldsHave Typology.Possession.PossessionSource.companion = true
• Heine1997.schemaYieldsHave Typology.Possession.PossessionSource.genitive = true
• Heine1997.schemaYieldsHave Typology.Possession.PossessionSource.goal = true
• Heine1997.schemaYieldsHave Typology.Possession.PossessionSource.source = false
• Heine1997.schemaYieldsHave Typology.Possession.PossessionSource.topic = true
• Heine1997.schemaYieldsHave Typology.Possession.PossessionSource.equation = false

def Heine1997.schemaYieldsBelong : Typology.Possession.PossessionSource → Bool

Equations

• Heine1997.schemaYieldsBelong Typology.Possession.PossessionSource.action = true
• Heine1997.schemaYieldsBelong Typology.Possession.PossessionSource.location = false
• Heine1997.schemaYieldsBelong Typology.Possession.PossessionSource.companion = false
• Heine1997.schemaYieldsBelong Typology.Possession.PossessionSource.genitive = false
• Heine1997.schemaYieldsBelong Typology.Possession.PossessionSource.goal = true
• Heine1997.schemaYieldsBelong Typology.Possession.PossessionSource.source = false
• Heine1997.schemaYieldsBelong Typology.Possession.PossessionSource.topic = false
• Heine1997.schemaYieldsBelong Typology.Possession.PossessionSource.equation = true

theorem Heine1997.location_yields_have_only : schemaYieldsHave Typology.Possession.PossessionSource.location = true ∧ schemaYieldsBelong Typology.Possession.PossessionSource.location = false

Location invariably leads to have-constructions, never belong.

theorem Heine1997.equation_yields_belong_only : schemaYieldsHave Typology.Possession.PossessionSource.equation = false ∧ schemaYieldsBelong Typology.Possession.PossessionSource.equation = true

Equation invariably leads to belong-constructions, never have.

theorem Heine1997.dual_schemas (s : Typology.Possession.PossessionSource) : schemaYieldsHave s = true ∧ schemaYieldsBelong s = true ↔ s = Typology.Possession.PossessionSource.action ∨ s = Typology.Possession.PossessionSource.goal

Action and Goal are the only schemas that can yield both types.

inductive Heine1997.OverlapStage : Type

Grammaticalization from source schema to possessive target proceeds through three stages (the Overlap Model, Figure 2.1).

• sourceOnly : OverlapStage

  Stage I: the construction has source meaning only. (e.g., "The money is in his hand" = pure location)

• overlap : OverlapStage

  Stage II: source and target meanings overlap; the construction is ambiguous between source and possessive interpretations. (e.g., Russian "u Markovyx gripp" = "There is flu at the Markovs" or "The Markovs have the flu")

• targetOnly : OverlapStage

  Stage III: target meaning only; source meaning is no longer available. (e.g., Estonian "isal on raamat" = "Father has a book", not "A book is on the father")

@[implicit_reducible]

instance Heine1997.instDecidableEqOverlapStage : DecidableEq OverlapStage

Equations

• Heine1997.instDecidableEqOverlapStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Heine1997.instReprOverlapStage : Repr OverlapStage

Equations

• Heine1997.instReprOverlapStage = { reprPrec := Heine1997.instReprOverlapStage.repr }

def Heine1997.instReprOverlapStage.repr : OverlapStage → ℕ → Std.Format

Equations

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

def Heine1997.OverlapStage.degree : OverlapStage → ℕ

The Overlap Model is a monotonic progression: each stage is more grammaticalized than the previous.

Equations

• Heine1997.OverlapStage.sourceOnly.degree = 0
• Heine1997.OverlapStage.overlap.degree = 1
• Heine1997.OverlapStage.targetOnly.degree = 2

theorem Heine1997.overlap_ordered : OverlapStage.sourceOnly.degree < OverlapStage.overlap.degree ∧ OverlapStage.overlap.degree < OverlapStage.targetOnly.degree

Source-only precedes overlap, which precedes target-only.

theorem Heine1997.action_overlap_cline_covary : OverlapStage.sourceOnly.degree < OverlapStage.targetOnly.degree ∧ Diachronic.Grammaticalization.GramStage.fullVerb < Diachronic.Grammaticalization.GramStage.auxiliary

The Action Schema's grammaticalization path through the Overlap Model: a full lexical verb ('take', 'seize') at Stage I becomes a possessive auxiliary ('have') at Stage III. Both the Overlap Model and the verbal cline are monotonic, and they co-vary: advancing through overlap stages corresponds to advancing along the boundedness cline.

This parallels the general unidirectionality of grammaticalization: fullVerb → auxiliary is the path from source schema (action verb) to target schema (possessive marker).

structure Heine1997.SchemaDist : Type

Distribution of major source schemas across continents, from the 100-language sample. Each entry is (schema, counts by continent). Continents: Europe, Asia, Africa, America, Indian/Pacific Ocean.

• schema : Typology.Possession.PossessionSource
• europe : ℕ
• asia : ℕ
• africa : ℕ
• america : ℕ
• pacific : ℕ

@[implicit_reducible]

instance Heine1997.instDecidableEqSchemaDist : DecidableEq SchemaDist

Equations

• Heine1997.instDecidableEqSchemaDist = Heine1997.instDecidableEqSchemaDist.decEq

def Heine1997.instDecidableEqSchemaDist.decEq (x✝ x✝¹ : SchemaDist) : Decidable (x✝ = x✝¹)

Equations

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

def Heine1997.instReprSchemaDist.repr : SchemaDist → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Heine1997.instReprSchemaDist : Repr SchemaDist

Equations

• Heine1997.instReprSchemaDist = { reprPrec := Heine1997.instReprSchemaDist.repr }

def Heine1997.SchemaDist.total (d : SchemaDist) : ℕ

Equations

• d.total = d.europe + d.asia + d.africa + d.america + d.pacific

def Heine1997.actionDist : SchemaDist

Table 2.2 data: major schemas in 100 languages. Note: some languages have more than one major schema, so totals exceed 100.

Equations

• Heine1997.actionDist = { schema := Typology.Possession.PossessionSource.action, europe := 3, asia := 1, africa := 9, america := 1, pacific := 1 }

def Heine1997.locationDist : SchemaDist

Equations

• Heine1997.locationDist = { schema := Typology.Possession.PossessionSource.location, europe := 5, asia := 8, africa := 9, america := 1, pacific := 0 }

def Heine1997.companionDist : SchemaDist

Equations

• Heine1997.companionDist = { schema := Typology.Possession.PossessionSource.companion, europe := 0, asia := 0, africa := 7, america := 3, pacific := 4 }

def Heine1997.genitiveDist : SchemaDist

Equations

• Heine1997.genitiveDist = { schema := Typology.Possession.PossessionSource.genitive, europe := 0, asia := 2, africa := 4, america := 5, pacific := 5 }

def Heine1997.goalDist : SchemaDist

Equations

• Heine1997.goalDist = { schema := Typology.Possession.PossessionSource.goal, europe := 3, asia := 11, africa := 4, america := 1, pacific := 3 }

def Heine1997.topicDist : SchemaDist

Equations

• Heine1997.topicDist = { schema := Typology.Possession.PossessionSource.topic, europe := 0, asia := 4, africa := 1, america := 3, pacific := 3 }

def Heine1997.table2_2 : List SchemaDist

Equations

• Heine1997.table2_2 = [Heine1997.actionDist, Heine1997.locationDist, Heine1997.companionDist, Heine1997.genitiveDist, Heine1997.goalDist, Heine1997.topicDist]

theorem Heine1997.table2_2_total : actionDist.total + locationDist.total + companionDist.total + genitiveDist.total + goalDist.total + topicDist.total = 101

Total attestations across six identifiable schemas: 101 (> 100 because some languages use multiple schemas). The remaining 9 attestations are opaque or minor schemas not included here.

theorem Heine1997.location_and_goal_most_frequent : locationDist.total ≥ goalDist.total ∧ goalDist.total > actionDist.total

Location and Goal are the two most frequent schemas worldwide.

theorem Heine1997.action_not_dominant : actionDist.total * 100 / 110 < 15

Action accounts for only 13.6% of major schema attestations (15 out of 110 total) — less common than often assumed for European-centric linguistics. The denominator 110 includes opaque/other schemas.

theorem Heine1997.asia_goal_dominant : goalDist.asia > locationDist.asia ∧ goalDist.asia > actionDist.asia ∧ goalDist.asia > topicDist.asia

In Asia, Goal (via dative/benefactive) is the most common schema, exceeding Location (the runner-up): 11 vs 8 out of 26.

theorem Heine1997.africa_location_action_tie : locationDist.africa = actionDist.africa

In Africa, Location and Action tie as the most common sources (9 each).

def Heine1997.schemaTypicalNotions : Typology.Possession.PossessionSource → List Typology.Possession.PossessiveNotion

Probabilistic correlations between source schemas and the possessive notions they are most likely to express (§2.3, generalizations i-iv).

• Location: most likely physical/temporary possession
• Existence (Genitive, Goal, Topic): permanent/inalienable possession
• Companion: physical/temporary, or alienable possession
• Action: wide range (physical through permanent)
• Equation: permanent (ownership, "the book is mine")

Equations

• One or more equations did not get rendered due to their size.
• Heine1997.schemaTypicalNotions Typology.Possession.PossessionSource.location = [Typology.Possession.PossessiveNotion.physical, Typology.Possession.PossessiveNotion.temporary]
• Heine1997.schemaTypicalNotions Typology.Possession.PossessionSource.companion = [Typology.Possession.PossessiveNotion.physical, Typology.Possession.PossessiveNotion.temporary]
• Heine1997.schemaTypicalNotions Typology.Possession.PossessionSource.genitive = [Typology.Possession.PossessiveNotion.permanent, Typology.Possession.PossessiveNotion.inalienable]
• Heine1997.schemaTypicalNotions Typology.Possession.PossessionSource.source = []
• Heine1997.schemaTypicalNotions Typology.Possession.PossessionSource.topic = [Typology.Possession.PossessiveNotion.permanent, Typology.Possession.PossessiveNotion.inalienable]
• Heine1997.schemaTypicalNotions Typology.Possession.PossessionSource.equation = [Typology.Possession.PossessiveNotion.permanent, Typology.Possession.PossessiveNotion.inalienable]

theorem Heine1997.existence_not_physical : ¬(schemaTypicalNotions Typology.Possession.PossessionSource.genitive).contains Typology.Possession.PossessiveNotion.physical = true ∧ ¬(schemaTypicalNotions Typology.Possession.PossessionSource.goal).contains Typology.Possession.PossessiveNotion.physical = true ∧ ¬(schemaTypicalNotions Typology.Possession.PossessionSource.topic).contains Typology.Possession.PossessiveNotion.physical = true

Existence schemas (Genitive, Goal, Topic) are never recruited for physical possession.

theorem Heine1997.location_not_permanent : ¬(schemaTypicalNotions Typology.Possession.PossessionSource.location).contains Typology.Possession.PossessiveNotion.permanent = true ∧ ¬(schemaTypicalNotions Typology.Possession.PossessionSource.location).contains Typology.Possession.PossessiveNotion.inalienable = true

Location is most likely associated with physical/temporary; it is not typically recruited for permanent or inalienable possession.

def Heine1997.schemaArity : Typology.Possession.PossessionSource → Semantics.ArgumentStructure.Relational.SemType

Map each schema to its Barker 2011 semantic type, based on the argument structure of the resulting possessive predicate.

Possessor-as-subject schemas (Action, Companion) produce transitive constructions: the possessive verb takes two core arguments (possessor and possessee), corresponding to @cite{barker-2011}'s Pred2.

Possessee-as-subject schemas produce intransitive/existential constructions: the possessee is the sole core argument, and the possessor is an oblique adjunct. The possessive predicate is Pred1, with the possessor introduced by Ex closure or case marking.

Equations

• Heine1997.schemaArity Typology.Possession.PossessionSource.action = Semantics.ArgumentStructure.Relational.SemType.pred2
• Heine1997.schemaArity Typology.Possession.PossessionSource.companion = Semantics.ArgumentStructure.Relational.SemType.pred2
• Heine1997.schemaArity x✝ = Semantics.ArgumentStructure.Relational.SemType.pred1

theorem Heine1997.possessor_subject_iff_pred2 (s : Typology.Possession.PossessionSource) : schemaSubject s = SubjectParticipant.possessor ↔ schemaArity s = Semantics.ArgumentStructure.Relational.SemType.pred2

Possessor-as-subject correlates exactly with Pred2 (transitive).

theorem Heine1997.pred2_action_companion_only (s : Typology.Possession.PossessionSource) : schemaArity s = Semantics.ArgumentStructure.Relational.SemType.pred2 ↔ s = Typology.Possession.PossessionSource.action ∨ s = Typology.Possession.PossessionSource.companion

Pred2 schemas are exactly the basic-structure schemas where the possessor is a core argument (not grafted on). Companion is the exception: extended structure but still Pred2, because the comitative complement is reanalyzed as a core argument.

theorem Heine1997.pred1_possessee_subject (s : Typology.Possession.PossessionSource) : schemaArity s = Semantics.ArgumentStructure.Relational.SemType.pred1 → schemaSubject s = SubjectParticipant.possessee

The Pred1 schemas (Location, Genitive, Goal, Source, Topic, Equation) express possession via an existential predicate + oblique possessor. This matches Barker's ExProp closure: the possessor is introduced by existential quantification over a relation, not as a direct argument of the predicate.

Structural consequence: in these schemas, the possessor does NOT fill a relatum slot directly (as it would in Pred2). Instead, it is introduced via case morphology (locative, dative, genitive, etc.) — the morphological reflex of the oblique adjunct position.

theorem Heine1997.action_schema_on_cline : Diachronic.Grammaticalization.GramStage.fullVerb < Diachronic.Grammaticalization.GramStage.auxiliary

The Action Schema's grammaticalization path: full lexical verb ('take', 'seize') → have-verb (auxiliary-like). This places Action Schema verbs on the grammaticalization cline from fullVerb toward auxiliary.

structure Heine1997.SchemaPrediction : Type

A schema prediction bundle: the testable predictions Heine makes for any language that draws on a given source schema.

• schema : Typology.Possession.PossessionSource
• yieldsHave : Bool
• yieldsBelong : Bool
• possessorIsSubject : Bool
• arity : Semantics.ArgumentStructure.Relational.SemType

def Heine1997.predictionsFor (s : Typology.Possession.PossessionSource) : SchemaPrediction

Derive predictions from a schema.

Equations

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

theorem Heine1997.location_predictions : have p := predictionsFor Typology.Possession.PossessionSource.location; p.yieldsHave = true ∧ p.yieldsBelong = false ∧ p.possessorIsSubject = false ∧ p.arity = Semantics.ArgumentStructure.Relational.SemType.pred1

Location Schema predictions: have-only, possessee-as-subject, Pred1.

theorem Heine1997.companion_predictions : have p := predictionsFor Typology.Possession.PossessionSource.companion; p.yieldsHave = true ∧ p.yieldsBelong = false ∧ p.possessorIsSubject = true ∧ p.arity = Semantics.ArgumentStructure.Relational.SemType.pred2

Companion Schema predictions: have-only, possessor-as-subject, Pred2.

theorem Heine1997.genitive_predictions : have p := predictionsFor Typology.Possession.PossessionSource.genitive; p.yieldsHave = true ∧ p.yieldsBelong = false ∧ p.possessorIsSubject = false ∧ p.arity = Semantics.ArgumentStructure.Relational.SemType.pred1

Genitive Schema predictions: have-only, possessee-as-subject, Pred1.

def Heine1997.walsToSchema : Data.WALS.F117A.PredicativePossession → Typology.Possession.PossessionSource

@cite{stassen-2013b}'s WALS Ch 117 uses five categories for predicative possession that correspond to Heine's schemas:

• WALS locational ↔ Heine Location Schema
• WALS genitive ↔ Heine Genitive Schema
• WALS topic ↔ Heine Topic Schema
• WALS conjunctional ↔ Heine Companion Schema
• WALS have ↔ Heine Action Schema

Note: Stassen's "conjunctional" is his term for comitative-based possession (Heine's Companion Schema). Goal Schema languages are typically classified under WALS locational (since both use oblique possessors with existential predicates).

Equations

• Heine1997.walsToSchema Data.WALS.F117A.PredicativePossession.locational = Typology.Possession.PossessionSource.location
• Heine1997.walsToSchema Data.WALS.F117A.PredicativePossession.genitive = Typology.Possession.PossessionSource.genitive
• Heine1997.walsToSchema Data.WALS.F117A.PredicativePossession.topic = Typology.Possession.PossessionSource.topic
• Heine1997.walsToSchema Data.WALS.F117A.PredicativePossession.conjunctional = Typology.Possession.PossessionSource.companion
• Heine1997.walsToSchema Data.WALS.F117A.PredicativePossession.have = Typology.Possession.PossessionSource.action

theorem Heine1997.wals_agrees_with_predicativeSource : walsToSchema Data.WALS.F117A.PredicativePossession.have = Typology.Possession.predicativeSource Typology.Possession.PredicativePossession.haveVerb ∧ walsToSchema Data.WALS.F117A.PredicativePossession.locational = Typology.Possession.predicativeSource Typology.Possession.PredicativePossession.locational ∧ walsToSchema Data.WALS.F117A.PredicativePossession.topic = Typology.Possession.predicativeSource Typology.Possession.PredicativePossession.topic ∧ walsToSchema Data.WALS.F117A.PredicativePossession.conjunctional = Typology.Possession.predicativeSource Typology.Possession.PredicativePossession.comitative

The WALS-to-Heine mapping agrees with predicativeSource from Typology/Possession.lean for the five strategies they share.

Per-language verifications previously co-located in Fragment files. Moved here per CLAUDE.md "Fragments never import Phenomena" rule: paper-anchored predictions must live in the paper's study file.

Russian: Location Schema (primary) + Action Schema (imet', secondary).

theorem Heine1997.russian_primary_matches_heine : have p := predictionsFor Fragments.Slavic.Russian.Possession.sourceSchema; p.yieldsHave = true ∧ p.yieldsBelong = false ∧ p.possessorIsSubject = false

Russian's primary Location Schema matches Heine's predictions: have-construction (not belong), possessee as subject.

theorem Heine1997.russian_secondary_is_dual : schemaYieldsHave Fragments.Slavic.Russian.Possession.secondarySchema = true ∧ schemaYieldsBelong Fragments.Slavic.Russian.Possession.secondarySchema = true

Russian's secondary Action Schema can yield both have and belong, matching Table 2.4.

theorem Heine1997.russian_overlap_stages_ordered : OverlapStage.sourceOnly.degree < OverlapStage.overlap.degree ∧ OverlapStage.overlap.degree < OverlapStage.targetOnly.degree

The u construction coexists across all three Overlap stages in Russian, matching the paper's example (73a-d). Stage I and III are strictly ordered.

theorem Heine1997.russian_wals_consistent : walsToSchema Data.WALS.F117A.PredicativePossession.locational = Fragments.Slavic.Russian.Possession.sourceSchema

WALS F117A classifies Russian as locational, matching its primary Location Schema.

Finnish: Location Schema at Stage III.

theorem Heine1997.finnish_matches_heine_predictions : have p := predictionsFor Fragments.Finnish.Possession.sourceSchema; p.yieldsHave = true ∧ p.yieldsBelong = false ∧ p.possessorIsSubject = false

Finnish's Location Schema matches Heine's predictions: have-construction (not belong), possessee as subject, Pred1 arity.

theorem Heine1997.finnish_stage_III_grammaticalization : OverlapStage.targetOnly.degree > OverlapStage.overlap.degree

Finnish at Stage III: the adessive in possessive use is no longer interpreted as locative. This matches the Overlap Model prediction that fully grammaticalized schemas lose their source meaning.

theorem Heine1997.finnish_wals_consistent : walsToSchema Data.WALS.F117A.PredicativePossession.locational = Fragments.Finnish.Possession.sourceSchema

WALS F117A classifies Finnish as locational, which maps to Location Schema via walsToSchema.

Turkish: Genitive Schema (primary) + Location + Equation variants.

theorem Heine1997.turkish_genitive_matches_heine : have p := predictionsFor Fragments.Turkish.Possession.sourceSchema; p.yieldsHave = true ∧ p.yieldsBelong = false ∧ p.possessorIsSubject = false

Turkish's primary Genitive Schema matches Heine's predictions: have-construction (not belong), possessee as subject.

theorem Heine1997.turkish_genitive_notions_match_prediction : (schemaTypicalNotions Fragments.Turkish.Possession.sourceSchema).contains Typology.Possession.PossessiveNotion.permanent = true ∧ (schemaTypicalNotions Fragments.Turkish.Possession.sourceSchema).contains Typology.Possession.PossessiveNotion.inalienable = true

Heine predicts Genitive Schema correlates with permanent/inalienable notions. Turkish's genitive notions match this.

theorem Heine1997.turkish_location_notions_match_prediction : (schemaTypicalNotions Fragments.Turkish.Possession.locationVariant).contains Typology.Possession.PossessiveNotion.physical = true ∧ (schemaTypicalNotions Fragments.Turkish.Possession.locationVariant).contains Typology.Possession.PossessiveNotion.temporary = true

Heine predicts Location Schema correlates with physical/temporary notions. Turkish's location variant notions match this.

theorem Heine1997.turkish_wals_consistent : walsToSchema Data.WALS.F117A.PredicativePossession.genitive = Fragments.Turkish.Possession.sourceSchema

WALS F117A classifies Turkish as genitive, matching its primary Genitive Schema.

Swahili: Companion Schema (Bantu -na).

theorem Heine1997.swahili_companion_matches_heine : have p := predictionsFor Fragments.Swahili.Possession.sourceSchema; p.yieldsHave = true ∧ p.yieldsBelong = false ∧ p.possessorIsSubject = true ∧ p.arity = Semantics.ArgumentStructure.Relational.SemType.pred2

Swahili's Companion Schema matches Heine's predictions: have-construction (not belong), possessor as subject, Pred2.

theorem Heine1997.swahili_full_grammaticalization : Fragments.Swahili.Possession.expressibleNotions.length = 7 ∧ OverlapStage.targetOnly.degree = 2

Swahili is at Stage III: the -na marker is no longer decomposable into copula + comitative, so the source meaning (accompaniment) is no longer available. All seven notions expressible confirms full grammaticalization.

theorem Heine1997.swahili_wals_consistent : walsToSchema Data.WALS.F117A.PredicativePossession.conjunctional = Fragments.Swahili.Possession.sourceSchema

WALS F117A classifies Swahili as conjunctional (Stassen's term for comitative-based possession), which maps to Companion Schema via walsToSchema.