Kampanarou and Alexiadou (2026): Genitive Alternation in Possessives and Beyond

This file formalizes [KA26], on the Standard Modern Greek alternation between an inflectional genitive and a prepositional apo-phrase, with adnominal possessors and with the arguments of derived nominals. The paper argues that the alternation is structural rather than morphological: the apo-PP is not an alternative spell-out of the genitive but a complement with a partitive semantics, through which a possessive reading is coerced.

The possessive data of Sections 2, 3 and 5 are rows carrying the paper's classification of the relation and of the possessor nominal (Possessor). Part-whole and source relations alternate with a common-noun possessor, pronouns and proper names never do, and acceptability is monotone in the facilitation order on possessors, which adds plural marking, modification, or a paradigm gap of the genitive (facilitation_mono); a gap is neither sufficient nor necessary for the alternation.

For derived nominals (Sections 2 and 6), the complex-event reading of [Gri90] survives only under a genitive theme, an apo agent is a by-phrase only under that reading, and the nominal otherwise admits at most one argument (Nominal.WellFormed): the single argument restriction of Section 8, extending the single genitive restriction of [HS87] to PPs. Grevena Greek, which has lost the inflectional genitive ([MCS24]), stacks two apo-PPs. The scope data of Section 7 follow from the merge site of the possessor (Site): the genitive of an inalienable possessor and every apo-PP are complements ([Ale03]), and only a complement possessor admits surface scope (scope_rows_agree).

Implementation notes

The paper's markers are read on the Judgment scale, ? as marginal, ?? and ??? as questionable, # as unacceptable and * as ungrammatical; a row is Acceptable from marginal up, since ? marks speaker variation. The three syntactic analyses of Section 7 (selection by the possessee, a predicative small clause, a light p) share the consequence formalized here, that the apo-PP is a complement, and are not distinguished. The recursive possessives (25) to (27) record, as the paper does, that only the innermost possessor alternates; its footnote 14 offers no account.

References

• [KA26]
• [Ale03], [Gri90], [HS87]
• [MCS24]

def KampanarouAlexiadou2026.Acceptable (j : Judgment) : Prop

Acceptable from marginal, the paper's ?, up.

Equations

• KampanarouAlexiadou2026.Acceptable j = (Judgment.marginal ≤ j)

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidablePredJudgmentAcceptable : DecidablePred Acceptable

Equations

• KampanarouAlexiadou2026.instDecidablePredJudgmentAcceptable x✝ = { decide := (↑Judgment.marginal.rank).ble ↑x✝.rank, reflects_decide := ⋯ }

Possessive apo-PPs (Sections 2, 3 and 5)

inductive KampanarouAlexiadou2026.Relation : Type

The paper's classification of the relation between possessee and possessor: part-whole (5a), source (5b), kinship (6a), ownership (6b), and the mere association of a mat with its door (11).

• partWhole : Relation
• source : Relation
• kinship : Relation
• ownership : Relation
• association : Relation

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidableEqRelation : DecidableEq Relation

Equations

• KampanarouAlexiadou2026.instDecidableEqRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KampanarouAlexiadou2026.instReprRelation : Repr Relation

Equations

• KampanarouAlexiadou2026.instReprRelation = { reprPrec := KampanarouAlexiadou2026.instReprRelation.repr }

def KampanarouAlexiadou2026.instReprRelation.repr : Relation → ℕ → Std.Format

Equations

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

def KampanarouAlexiadou2026.Relation.IsPartitive (r : Relation) : Prop

The relations the paper reads as partitive: the possessee is a part of, or comes from, the possessor.

Equations

• r.IsPartitive = (r = KampanarouAlexiadou2026.Relation.partWhole ∨ r = KampanarouAlexiadou2026.Relation.source)

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidablePredRelationIsPartitive : DecidablePred Relation.IsPartitive

Equations

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

def KampanarouAlexiadou2026.Relation.IsInalienable (r : Relation) : Prop

Inalienable relations in the sense of [Ale03]: parts, body parts, and kin.

Equations

• r.IsInalienable = (r = KampanarouAlexiadou2026.Relation.partWhole ∨ r = KampanarouAlexiadou2026.Relation.kinship)

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidablePredRelationIsInalienable : DecidablePred Relation.IsInalienable

Equations

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

inductive KampanarouAlexiadou2026.Form : Type

How the possessor is presented.

• common : Form
• pronoun : Form
• properName : Form

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidableEqForm : DecidableEq Form

Equations

• KampanarouAlexiadou2026.instDecidableEqForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KampanarouAlexiadou2026.instReprForm : Repr Form

Equations

• KampanarouAlexiadou2026.instReprForm = { reprPrec := KampanarouAlexiadou2026.instReprForm.repr }

def KampanarouAlexiadou2026.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

structure KampanarouAlexiadou2026.Possessor : Type

The possessor nominal: its form, animacy, plural marking and modification, and whether its genitive is a paradigm gap (Section 3).

• form : Form
• animate : Bool
• plural : Bool
• modified : Bool
• gap : Bool

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidableEqPossessor : DecidableEq Possessor

Equations

• KampanarouAlexiadou2026.instDecidableEqPossessor = KampanarouAlexiadou2026.instDecidableEqPossessor.decEq

def KampanarouAlexiadou2026.instDecidableEqPossessor.decEq (x✝ x✝¹ : Possessor) : Decidable (x✝ = x✝¹)

Equations

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

def KampanarouAlexiadou2026.instReprPossessor.repr : Possessor → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KampanarouAlexiadou2026.instReprPossessor : Repr Possessor

Equations

• KampanarouAlexiadou2026.instReprPossessor = { reprPrec := KampanarouAlexiadou2026.instReprPossessor.repr }

@[instance_reducible]

instance KampanarouAlexiadou2026.instPartialOrderPossessor : PartialOrder Possessor

The facilitation order: p ≤ q when q is the same kind of nominal as p with plural marking, modification, or a paradigm gap only added, each of which the paper reports to raise the acceptability of the apo-PP.

Equations

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

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidableRelPossessorLe : DecidableRel fun (x1 x2 : Possessor) => x1 ≤ x2

Equations

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

structure KampanarouAlexiadou2026.Row : Type

A possessive row: the relation, the possessor, and the judgment on the apo-PP.

• relation : Relation
• possessor : Possessor
• judgment : Judgment

def KampanarouAlexiadou2026.relationOf : List (String × Relation)

Equations

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

def KampanarouAlexiadou2026.formOf : List (String × Form)

Equations

• KampanarouAlexiadou2026.formOf = [("common", KampanarouAlexiadou2026.Form.common), ("pronoun", KampanarouAlexiadou2026.Form.pronoun), ("properName", KampanarouAlexiadou2026.Form.properName)]

def KampanarouAlexiadou2026.Row.ofDatum (e : Datum) : Option Row

A row of the possessive group, from the paper's features.

Equations

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

def KampanarouAlexiadou2026.rows : List Row

The possessive data of Sections 2, 3 and 5.

Equations

• KampanarouAlexiadou2026.rows = List.filterMap KampanarouAlexiadou2026.Row.ofDatum KampanarouAlexiadou2026.Examples.all

theorem KampanarouAlexiadou2026.partitive_alternates (r : Row) : r ∈ rows → r.relation.IsPartitive → r.possessor.form = Form.common → Acceptable r.judgment

Part-whole and source relations alternate whenever the possessor is a common noun, (5), (14).

theorem KampanarouAlexiadou2026.individual_resists (r : Row) : r ∈ rows → r.possessor.form ≠ Form.common → r.judgment = Judgment.unacceptable

Pronouns and proper names resist the apo-PP whatever the relation, (9), (10).

theorem KampanarouAlexiadou2026.nonpartitive_resists (r : Row) : r ∈ rows → ¬r.relation.IsPartitive → ¬r.possessor.plural = true → ¬r.possessor.modified = true → ¬Acceptable r.judgment

Kinship, ownership and mere association resist the apo-PP unless the possessor is plural or modified, (6), (11a), (15).

theorem KampanarouAlexiadou2026.facilitation_mono (r : Row) : r ∈ rows → ∀ s ∈ rows, r.relation = s.relation → r.possessor ≤ s.possessor → r.judgment ≤ s.judgment

Acceptability is monotone in the facilitation order: plural marking (11), modification (fn. 5, (28)) and a paradigm gap (14) only raise the judgment.

theorem KampanarouAlexiadou2026.gap_not_sufficient : ∃ r ∈ rows, r.possessor.gap = true ∧ r.judgment = Judgment.unacceptable

A paradigm gap is not sufficient for the alternation, (15).

theorem KampanarouAlexiadou2026.gap_not_necessary : ∃ r ∈ rows, ¬r.possessor.gap = true ∧ Acceptable r.judgment

Nor is it necessary, (5).

theorem KampanarouAlexiadou2026.relation_matters : ∃ r ∈ rows, ∃ s ∈ rows, r.possessor = s.possessor ∧ r.judgment ≠ s.judgment

The relation matters on its own: the same possessor nominal, the door, yields an acceptable apo-PP for its handle (5a) and a questionable one for its mat (11a).

Recursive possessives (Section 5)

inductive KampanarouAlexiadou2026.Marking : Type

The realization of a possessor or of an argument.

• genitive : Marking
• apo : Marking

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidableEqMarking : DecidableEq Marking

Equations

• KampanarouAlexiadou2026.instDecidableEqMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KampanarouAlexiadou2026.instReprMarking : Repr Marking

Equations

• KampanarouAlexiadou2026.instReprMarking = { reprPrec := KampanarouAlexiadou2026.instReprMarking.repr }

def KampanarouAlexiadou2026.instReprMarking.repr : Marking → ℕ → Std.Format

Equations

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

def KampanarouAlexiadou2026.markingOf : List (String × Marking)

Equations

• KampanarouAlexiadou2026.markingOf = [("genitive", KampanarouAlexiadou2026.Marking.genitive), ("apo", KampanarouAlexiadou2026.Marking.apo)]

structure KampanarouAlexiadou2026.Stacked : Type

A recursive possessive, (25) to (27): the inner possessor, closest to the head, and the outer one it embeds.

• inner : Marking
• outer : Marking
• judgment : Judgment

def KampanarouAlexiadou2026.Stacked.ofDatum (e : Datum) : Option Stacked

A row of the stacking group.

Equations

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

def KampanarouAlexiadou2026.stacked : List Stacked

The recursive possessives of Section 5.

Equations

• KampanarouAlexiadou2026.stacked = List.filterMap KampanarouAlexiadou2026.Stacked.ofDatum KampanarouAlexiadou2026.Examples.all

theorem KampanarouAlexiadou2026.innermost_alternates (s : Stacked) : s ∈ stacked → (Acceptable s.judgment ↔ s.outer = Marking.genitive)

Only the innermost possessor alternates: the phrase is acceptable exactly when the outer possessor keeps its genitive.

Derived nominals (Sections 2 and 6) and the single argument restriction (Section 8)

structure KampanarouAlexiadou2026.Nominal : Type

A derived nominal with its theme and its agent, each genitive, apo-PP, or absent, and whether an aspectual modifier (for x time) is present.

• theme : Option Marking
• agent : Option Marking
• aspectual : Bool

def KampanarouAlexiadou2026.instDecidableEqNominal.decEq (x✝ x✝¹ : Nominal) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidableEqNominal : DecidableEq Nominal

Equations

• KampanarouAlexiadou2026.instDecidableEqNominal = KampanarouAlexiadou2026.instDecidableEqNominal.decEq

@[instance_reducible]

instance KampanarouAlexiadou2026.instReprNominal : Repr Nominal

Equations

• KampanarouAlexiadou2026.instReprNominal = { reprPrec := KampanarouAlexiadou2026.instReprNominal.repr }

def KampanarouAlexiadou2026.instReprNominal.repr : Nominal → ℕ → Std.Format

Equations

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

def KampanarouAlexiadou2026.Nominal.IsComplexEvent (n : Nominal) : Prop

The complex-event reading of [Gri90], with verbal argument structure, is available only under a genitive theme; an apo theme forces the result reading, diagnosed by the aspectual modifier (34), (35) and by pluralization (36).

Equations

• n.IsComplexEvent = (n.theme = some KampanarouAlexiadou2026.Marking.genitive)

@[instance_reducible]

instance KampanarouAlexiadou2026.Nominal.instDecidablePredIsComplexEvent : DecidablePred IsComplexEvent

Equations

• x✝.instDecidablePredIsComplexEvent = KampanarouAlexiadou2026.Nominal.instDecidablePredIsComplexEvent._aux_1 x✝

def KampanarouAlexiadou2026.Nominal.IsByPhrase (n : Nominal) : Prop

An apo agent is a by-phrase, adjoined to the verbal structure, only under the complex-event reading, (30).

Equations

• n.IsByPhrase = (n.agent = some KampanarouAlexiadou2026.Marking.apo ∧ n.IsComplexEvent)

@[instance_reducible]

instance KampanarouAlexiadou2026.Nominal.instDecidablePredIsByPhrase : DecidablePred IsByPhrase

Equations

• x✝.instDecidablePredIsByPhrase = { decide := decide (x✝.agent = some KampanarouAlexiadou2026.Marking.apo) && decide x✝.IsComplexEvent, reflects_decide := ⋯ }

def KampanarouAlexiadou2026.Nominal.arguments (n : Nominal) : List Marking

The DP-internal arguments: the theme, and the agent unless it is a by-phrase.

Equations

• n.arguments = n.theme.toList ++ if n.IsByPhrase then [] else n.agent.toList

def KampanarouAlexiadou2026.Nominal.SingleArgument (n : Nominal) : Prop

The single argument restriction: at most one argument inside the DP.

Equations

• n.SingleArgument = (n.arguments.length ≤ 1)

@[instance_reducible]

instance KampanarouAlexiadou2026.Nominal.instDecidablePredSingleArgument : DecidablePred SingleArgument

Equations

• x✝.instDecidablePredSingleArgument = { decide := x✝.arguments.length.ble 1, reflects_decide := ⋯ }

def KampanarouAlexiadou2026.Nominal.WellFormed (n : Nominal) : Prop

A single argument, and an aspectual modifier only under the complex-event reading.

Equations

• n.WellFormed = (n.SingleArgument ∧ (n.aspectual = true → n.IsComplexEvent))

@[instance_reducible]

instance KampanarouAlexiadou2026.Nominal.instDecidablePredWellFormed : DecidablePred WellFormed

Equations

• x✝.instDecidablePredWellFormed = { decide := decide x✝.SingleArgument && decide (x✝.aspectual = true → x✝.IsComplexEvent), reflects_decide := ⋯ }

theorem KampanarouAlexiadou2026.Nominal.not_isComplexEvent_of_theme_apo {n : Nominal} (h : n.theme = some Marking.apo) : ¬n.IsComplexEvent

An apo theme forces the result reading.

theorem KampanarouAlexiadou2026.Nominal.not_singleArgument_of_apo_apo {n : Nominal} (ht : n.theme = some Marking.apo) (ha : n.agent = some Marking.apo) : ¬n.SingleArgument

Two apo-PPs never satisfy the restriction: the theme forces the result reading, so the agent is a second argument rather than a by-phrase, (8d).

inductive KampanarouAlexiadou2026.Variety : Type

Standard Modern Greek, or Grevena Greek with no inflectional genitive.

• smg : Variety
• grevena : Variety

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidableEqVariety : DecidableEq Variety

Equations

• KampanarouAlexiadou2026.instDecidableEqVariety x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KampanarouAlexiadou2026.instReprVariety.repr : Variety → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KampanarouAlexiadou2026.instReprVariety : Repr Variety

Equations

• KampanarouAlexiadou2026.instReprVariety = { reprPrec := KampanarouAlexiadou2026.instReprVariety.repr }

structure KampanarouAlexiadou2026.DerivedRow : Type

A derived-nominal row: the variety, the nominal, and the judgment.

• variety : Variety
• nominal : Nominal
• judgment : Judgment

def KampanarouAlexiadou2026.varietyOf : List (String × Variety)

Equations

• KampanarouAlexiadou2026.varietyOf = [("smg", KampanarouAlexiadou2026.Variety.smg), ("grevena", KampanarouAlexiadou2026.Variety.grevena)]

def KampanarouAlexiadou2026.DerivedRow.ofDatum (e : Datum) : Option DerivedRow

A row of the derived group.

Equations

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

def KampanarouAlexiadou2026.derivedRows : List DerivedRow

The derived nominals of Sections 2, 4 and 6.

Equations

• KampanarouAlexiadou2026.derivedRows = List.filterMap KampanarouAlexiadou2026.DerivedRow.ofDatum KampanarouAlexiadou2026.Examples.all

theorem KampanarouAlexiadou2026.derived_rows_agree (r : DerivedRow) : r ∈ derivedRows → r.variety = Variety.smg → (Acceptable r.judgment ↔ r.nominal.WellFormed)

The Standard Modern Greek rows are acceptable exactly when well-formed: (7), (8), (30) and (33) to (36).

theorem KampanarouAlexiadou2026.grevena_stacks : ∃ r ∈ derivedRows, r.variety = Variety.grevena ∧ ¬r.nominal.SingleArgument ∧ Acceptable r.judgment

Grevena Greek stacks two apo-PPs on one nominal, (12).

Scope and the merge site of the possessor (Section 7)

inductive KampanarouAlexiadou2026.Site : Type

The merge site of a possessor: the complement of the possessee, or external to it.

• complement : Site
• external : Site

@[instance_reducible]

instance KampanarouAlexiadou2026.instDecidableEqSite : DecidableEq Site

Equations

• KampanarouAlexiadou2026.instDecidableEqSite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KampanarouAlexiadou2026.instReprSite.repr : Site → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KampanarouAlexiadou2026.instReprSite : Repr Site

Equations

• KampanarouAlexiadou2026.instReprSite = { reprPrec := KampanarouAlexiadou2026.instReprSite.repr }

def KampanarouAlexiadou2026.Relation.genitiveSite (r : Relation) : Site

[Ale03]: a genitive inalienable possessor is a complement, an alienable one is external.

Equations

• r.genitiveSite = if r.IsInalienable then KampanarouAlexiadou2026.Site.complement else KampanarouAlexiadou2026.Site.external

def KampanarouAlexiadou2026.Marking.site : Marking → Relation → Site

The site of a possessor realized as m: every apo-PP is a complement, the structural claim shared by the paper's three analyses.

Equations

• KampanarouAlexiadou2026.Marking.genitive.site x✝ = x✝.genitiveSite
• KampanarouAlexiadou2026.Marking.apo.site x✝ = KampanarouAlexiadou2026.Site.complement

structure KampanarouAlexiadou2026.ScopeRow : Type

A scope row, (38) and (39): an indefinite possessee under a universal possessor, and whether the surface-scope reading, one leg for all the tables, is available; the inverse reading always is.

• marking : Marking
• relation : Relation
• surface : Bool

def KampanarouAlexiadou2026.ScopeRow.ofDatum (e : Datum) : Option ScopeRow

A row of the scope group.

Equations

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

def KampanarouAlexiadou2026.scopeRows : List ScopeRow

The scope data of Section 7.

Equations

• KampanarouAlexiadou2026.scopeRows = List.filterMap KampanarouAlexiadou2026.ScopeRow.ofDatum KampanarouAlexiadou2026.Examples.all

theorem KampanarouAlexiadou2026.scope_rows_agree (r : ScopeRow) : r ∈ scopeRows → (r.surface = true ↔ r.marking.site r.relation = Site.complement)

Surface scope is available exactly for a complement possessor: the inalienable genitive (38a) and both apo-PPs (39), not the alienable genitive (38b).