Possessive descriptions 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, descriptionGQ) is in Possessive/GQ.lean; the determiner that denotes through these descriptions 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.Description — a possessor + relation + sortal restrictor; the possessee predicate is derived (viaModifier), never stored, so a description cannot be incoherent.
• Possessive.Definite — a possessive carrying a Russellian uniqueness presupposition.
• HasPossessor, HasPossesseePredicate, HasPossessionRelation, HasIotaWitness — composable capability mixins (root namespace, Add/Mul idiom); description types 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 : E → E → S → Prop) : E → S → Prop

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 : E → S → Prop) (R : E → E → S → Prop) : E → S → Prop

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 : E → E → S → Prop) : viaArgument possessor R = viaModifier possessor (fun (x : E) (x_1 : S) => True) R

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

Possessive descriptions

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

A possessive description ([Bar95]): 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 description cannot bundle a predicate unrelated to its relation.

• possessor : E

  The possessor entity.

• relation : E → E → S → Prop

  The possession relation.

• restrictor : E → S → Prop

  The sortal restrictor (the noun predicate).

def Possessive.Description.possesseePred {E : Type u_1} {S : Type u_2} (d : Description E S) : E → S → Prop

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

Equations

• d.possesseePred = Possessive.viaModifier d.possessor d.restrictor d.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 : E → S → Prop

  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 (their Table 1), reproduced in [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).

@[instance_reducible]

instance Possessive.instDecidableEqPossessionRelationType : DecidableEq PossessionRelationType

Equations

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

@[instance_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 → Prop) : Quantification.Quantifier E

Possessive as a type ⟨1⟩ quantifier (Quantifier): ⟦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 ∧ P y

Composable description capabilities

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

Type	HasPossessor	HasPossesseePredicate	HasPossessionRelation	HasIotaWitness
Possessive.Description E S	✓	✓	✓	—
Possessive.Definite E S	✓	✓	—	✓

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

A type 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 type whose values bundle a possessee predicate E → S → Prop.

• possesseePredicate : α → E → S → Prop

  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 type whose values bundle a possession relation E → E → S → Prop. Distinct from HasPossesseePredicate: a relational noun's R is the noun denotation itself, while a sortal-with-π construction carries R separately.

• possessionRelation : α → E → E → S → Prop

  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 description 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.

@[instance_reducible]

instance Possessive.instHasPossessorDescription {E : Type u_1} {S : Type u_2} : HasPossessor (Description E S) E

Equations

• Possessive.instHasPossessorDescription = { possessor := Possessive.Description.possessor }

@[instance_reducible]

instance Possessive.instHasPossesseePredicateDescription {E : Type u_1} {S : Type u_2} : HasPossesseePredicate (Description E S) E S

Equations

• Possessive.instHasPossesseePredicateDescription = { possesseePredicate := Possessive.Description.possesseePred }

@[instance_reducible]

instance Possessive.instHasPossessionRelationDescription {E : Type u_1} {S : Type u_2} : HasPossessionRelation (Description E S) E S

Equations

• Possessive.instHasPossessionRelationDescription = { possessionRelation := Possessive.Description.relation }

@[instance_reducible]

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

Equations

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

@[instance_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 : α) : E → S → Prop

The possessee set determined by any description 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 description bearing a Russellian iota-witness denotes a unique possessee at every situation. Definite possessives inherit ∃!-reference with no type-specific reproof.