Possessive carriers and capabilities

The unified Possessive namespace for the semantics of possessive constructions, built on the general relational-noun substrate (ArgumentStructure.Relational: π, Ex, iotaPresupposition, …). The quantificational layer (Poss, PossW, narrowing, carrierGQ) is in Possessive/GQ.lean; the determiner that denotes through these carriers is Possessive.denote (Semantics/Definiteness/DeterminerDenotation.lean).

Main declarations

• Possessive.viaArgument, Possessive.viaModifier — the two ways a possessor combines with a noun: with a relational noun's own relation (the argument genitive) or with a free relation over a sortal restrictor (the modifier genitive, Barker's π).
• Possessive.Carrier — a possessor + relation + sortal restrictor; the possessee predicate is derived (viaModifier), never stored, so a carrier cannot be incoherent.
• Possessive.Definite — a possessive carrying a Russellian uniqueness presupposition.
• HasPossessor, HasPossesseePredicate, HasPossessionRelation, HasIotaWitness — composable capability mixins (root namespace, Add/Mul idiom); carriers opt into whichever axes they bear.
• possesseeSet, existsUnique_possessee — capability-polymorphic consumers.
• Possessive.PossessionRelationType — the four-way Vikner-Jensen possession taxonomy.

Combining a possessor with a noun

def Possessive.viaArgument {E : Type u_1} {S : Type u_2} (possessor : E) (nounRel : ArgumentStructure.Relational.Pred2 E S) : ArgumentStructure.Relational.Pred1 E S

Applying a possessor to a lexically relational noun — the argument genitive: ⟦John's teacher⟧ = λy. teacher(John)(y).

Equations

• Possessive.viaArgument possessor nounRel y s = nounRel possessor y s

def Possessive.viaModifier {E : Type u_1} {S : Type u_2} (possessor : E) (nounPred : ArgumentStructure.Relational.Pred1 E S) (R : ArgumentStructure.Relational.Pred2 E S) : ArgumentStructure.Relational.Pred1 E S

Applying a possessor to a sortal noun via Barker's π — the modifier genitive with a free relation R: ⟦John's team⟧ = λy. team(y) ∧ R(John)(y).

Equations

• Possessive.viaModifier possessor nounPred R y s = ArgumentStructure.Relational.π nounPred R possessor y s

theorem Possessive.viaArgument_eq_viaModifier_top {E : Type u_1} {S : Type u_2} (possessor : E) (R : ArgumentStructure.Relational.Pred2 E S) : viaArgument possessor R = viaModifier possessor (fun (x : E) (x_1 : S) => True) R

The argument genitive is the modifier genitive over a trivial restrictor.

Carriers

structure Possessive.Carrier (E : Type u_3) (S : Type u_4) : Type (max u_3 u_4)

A possessive carrier: a possessor, a possession relation, and a sortal restrictor (the noun predicate; ⊤ for a purely relational noun). The possessee predicate is derived (viaModifier), not stored — so a carrier cannot bundle a predicate unrelated to its relation.

• possessor : E

  The possessor entity.

• relation : ArgumentStructure.Relational.Pred2 E S

  The possession relation.

• restrictor : ArgumentStructure.Relational.Pred1 E S

  The sortal restrictor (the noun predicate).

def Possessive.Carrier.possesseePred {E : Type u_1} {S : Type u_2} (c : Carrier E S) : ArgumentStructure.Relational.Pred1 E S

The derived possessee predicate: the restrictor conjoined with the relation applied to the possessor.

Equations

• c.possesseePred = Possessive.viaModifier c.possessor c.restrictor c.relation

structure Possessive.Definite (E : Type u_3) (S : Type u_4) : Type (max u_3 u_4)

A definite possessive carrying its Russellian uniqueness presupposition ("the boy's cat", "my mother").

• possessor : E

  The possessor entity.

• predicate : ArgumentStructure.Relational.Pred1 E S

  The possessee predicate (a definite description's restrictor).

• presupposition (s : S) : ArgumentStructure.Relational.iotaPresupposition self.predicate s

  The possessee predicate has a unique witness at every situation.

Vikner-Jensen possession taxonomy

inductive Possessive.PossessionRelationType : Type

Four-way lexical taxonomy of possession relations from [VJ02] §3.1.2, reproduced in Fig 6.1 of [Bar11]. The separate "pragmatic" interpretation is not lexical and is not one of these.

• inherent : PossessionRelationType

  Inherent relation: lexically argument-structural (the teacher's class).

• partWhole : PossessionRelationType

  Part-whole relation (the girl's nose, the car's wheel).

• agentive : PossessionRelationType

  Agentive relation (the girl's poem = the poem the girl wrote).

• control : PossessionRelationType

  Control relation: ownership or legal control (the girl's car).

@[implicit_reducible]

instance Possessive.instDecidableEqPossessionRelationType : DecidableEq PossessionRelationType

Equations

• Possessive.instDecidableEqPossessionRelationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Possessive.instReprPossessionRelationType : Repr PossessionRelationType

Equations

• Possessive.instReprPossessionRelationType = { reprPrec := Possessive.instReprPossessionRelationType.repr }

def Possessive.instReprPossessionRelationType.repr : PossessionRelationType → ℕ → Std.Format

Equations

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

Bridge to type ⟨1⟩ quantifiers

def Possessive.asNPQ {E : Type u_3} (possessor : E) (R : E → E → Bool) : Quantification.NPQ E

Possessive as a type ⟨1⟩ quantifier (NPQ): ⟦John's⟧ = fun R P ↦ ∃ y, R possessor y ∧ P y. Not isomorphism-invariant: it depends on the identity of the possessor, not just cardinalities.

Equations

• Possessive.asNPQ possessor R P = ∃ (y : E), R possessor y = true ∧ P y

Composable carrier capabilities

Cross-cutting capability mixins for the long-run library where 20-30+ possessive carriers each implement a subset of the axes. Following the mathlib Add/Mul/Inv/Neg idiom: many small composable classes, each one operation; carriers opt in to whichever axes they bear.

Carrier	HasPossessor	HasPossesseePredicate	HasPossessionRelation	HasIotaWitness
Possessive.Carrier E S	✓	✓	✓	—
Possessive.Definite E S	✓	✓	—	✓

class HasPossessor (α : Type u_1) (E : outParam (Type u_2)) : Type (max u_1 u_2)

A carrier whose values bundle a possessor entity.

• possessor : α → E

  Project the bundled possessor entity.

class HasPossesseePredicate (α : Type u_1) (E : outParam (Type u_2)) (S : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

A carrier whose values bundle a possessee predicate Pred1 E S.

• possesseePredicate : α → ArgumentStructure.Relational.Pred1 E S

  Project the bundled possessee predicate.

class HasPossessionRelation (α : Type u_1) (E : outParam (Type u_2)) (S : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

A carrier whose values bundle a possession relation Pred2 E S. Distinct from HasPossesseePredicate: a relational noun's R is the noun denotation itself, while a sortal-with-π construction carries R separately.

• possessionRelation : α → ArgumentStructure.Relational.Pred2 E S

  Project the bundled possession relation.

class HasIotaWitness (α : Type u_1) (E : outParam (Type u_2)) (S : outParam (Type u_3)) [HasPossesseePredicate α E S] : Prop

Prop class: a possessive carrier whose possessee predicate has a unique witness at every situation. Definite possessives bear this; existential and quantificational ones do not.

• iotaWitness (a : α) (s : S) : ArgumentStructure.Relational.iotaPresupposition (HasPossesseePredicate.possesseePredicate a) s

  The possessee predicate has a unique witness at every situation.

@[implicit_reducible]

instance Possessive.instHasPossessorCarrier {E : Type u_1} {S : Type u_2} : HasPossessor (Carrier E S) E

Equations

• Possessive.instHasPossessorCarrier = { possessor := Possessive.Carrier.possessor }

@[implicit_reducible]

instance Possessive.instHasPossesseePredicateCarrier {E : Type u_1} {S : Type u_2} : HasPossesseePredicate (Carrier E S) E S

Equations

• Possessive.instHasPossesseePredicateCarrier = { possesseePredicate := Possessive.Carrier.possesseePred }

@[implicit_reducible]

instance Possessive.instHasPossessionRelationCarrier {E : Type u_1} {S : Type u_2} : HasPossessionRelation (Carrier E S) E S

Equations

• Possessive.instHasPossessionRelationCarrier = { possessionRelation := Possessive.Carrier.relation }

@[implicit_reducible]

instance Possessive.instHasPossessorDefinite {E : Type u_1} {S : Type u_2} : HasPossessor (Definite E S) E

Equations

• Possessive.instHasPossessorDefinite = { possessor := Possessive.Definite.possessor }

@[implicit_reducible]

instance Possessive.instHasPossesseePredicateDefinite {E : Type u_1} {S : Type u_2} : HasPossesseePredicate (Definite E S) E S

Equations

• Possessive.instHasPossesseePredicateDefinite = { possesseePredicate := Possessive.Definite.predicate }

instance Possessive.instHasIotaWitnessDefinite {E : Type u_1} {S : Type u_2} : HasIotaWitness (Definite E S) E S

Definite carries its iota-presupposition as a structure field; the typeclass instance just exposes it.

Consuming the capabilities

def possesseeSet {α : Type u_1} {E : Type u_2} {S : Type u_3} [HasPossessor α E] [HasPossessionRelation α E S] (a : α) : ArgumentStructure.Relational.Pred1 E S

The possessee set determined by any carrier bundling a possessor and a possession relation: the entities standing in the relation to the possessor.

Equations

• possesseeSet a y s = HasPossessionRelation.possessionRelation a (HasPossessor.possessor a) y s

theorem existsUnique_possessee {α : Type u_1} {E : Type u_2} {S : Type u_3} [HasPossesseePredicate α E S] [HasIotaWitness α E S] (a : α) (s : S) : ∃! y : E, HasPossesseePredicate.possesseePredicate a y s

Any carrier bearing a Russellian iota-witness denotes a unique possessee at every situation. Definite possessives inherit ∃!-reference with no carrier-specific reproof.