Possessive descriptions

A possessive description ([barker-1995]) is a possessor, a possession relation, and a sortal restrictor; its possessee predicate π restrictor relation possessor is derived, never stored, so a description cannot pair a predicate with an unrelated relation. The determiner that denotes through descriptions is Possessive.denote (Semantics/Definiteness/Determiner.lean); the quantification over the possessed objects (Poss, PossW, Description.toGQ) is Semantics/Possession/Quantifier.lean. Whether a possessive is definite is not settled here: the determinate reading is one mode of quantification among those the quantifier layer parameterises ([PW06] §7.8.2, [coppock-beaver-2015] §4).

Main declarations

• Possession.Description, Description.possesseePred.
• Possession.asNPQ — [barker-2011]'s possessive as a type ⟨1⟩ quantifier.

References

• [barker-1995], [barker-2011]
• [PW06], [coppock-beaver-2015]

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

A possessive description ([barker-1995]): a possessor, a possession relation, and a sortal restrictor (the noun predicate; ⊤ for a purely relational noun).

• possessor : E

  The possessor entity.

• relation : E → E → S → Prop

  The possession relation.

• restrictor : E → S → Prop

  The sortal restrictor (the noun predicate).

def Possession.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 = Possession.π d.restrictor d.relation d.possessor

def Possession.asNPQ {E : Type u_1} (possessor : E) (R : E → E → Prop) : Quantification.Quantifier E

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

Equations

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