Barker 1995: Possessive Descriptions

Paper-anchored consumer of the possessive substrate for [Bar95b]. Two of the dissertation's signature claims, tested against concrete models:

• Narrowing ([Bar95b] p. 139): a quantificational possessor restricts quantification to those possessors that stand in the possession relation to some possessee. Most planets' rings are made of ice is evaluated only over planets that have rings. The substrate operator Possessive.Poss builds this in via the domain restriction dom A R; here we exhibit a model where narrowing flips the truth value (demonstrated with every, since the dom restriction is independent of the choice of possessor quantifier; most is noncomputable cardinality).

• Definiteness and uniqueness: a definite possessive denotes a unique possessee. The HasIotaWitness capability of Possessive.Definite yields this via existsUnique_possessee with no bespoke proof — the payoff of the composable-mixin design.

Main statements

• narrowed_holds / unnarrowed_fails / narrowing_flips_truth_value: the narrowing contrast on the planets/rings model.
• theBoysCat_unique: a definite possessive inherits ∃!-reference from its capability instance.
• johnsSisters_possesseeSet: a relational possessive's possesseeSet is its lexical relation applied to the possessor.

References

• [Bar95b]: Possessive Descriptions. CSLI Publications.

Narrowing

Model over Fin 5: 0, 1, 2 are planets, 3, 4 are rings. Planet 0 has ring 3, planet 1 has ring 4, and planet 2 has no ring. Both rings are icy. Most/every planet's rings are made of ice should be evaluated only over the ring-having planets 0, 1 — planet 2 is narrowed away.

def Barker1995.isPlanet : Fin 5 → Prop

The planets {0, 1, 2}.

Equations

• Barker1995.isPlanet x = (↑x < 3)

def Barker1995.isRing : Fin 5 → Prop

The rings {3, 4}.

Equations

• Barker1995.isRing x = (3 ≤ ↑x)

def Barker1995.isIcy : Fin 5 → Prop

Both rings are icy.

Equations

• Barker1995.isIcy = Barker1995.isRing

def Barker1995.hasRing : Fin 5 → Fin 5 → Prop

Planet 0 has ring 3; planet 1 has ring 4; planet 2 has no ring.

Equations

• Barker1995.hasRing x y = (x = 0 ∧ y = 3 ∨ x = 1 ∧ y = 4)

theorem Barker1995.narrowed_holds : Possessive.Poss Quantification.every_sem isPlanet Quantification.some_sem hasRing isRing isIcy

With narrowing, every planet's rings are made of ice is true: the ring-less planet 2 is excluded by the dom isRing hasRing restriction.

theorem Barker1995.unnarrowed_fails : ¬Quantification.every_sem isPlanet fun (x : Fin 5) => Quantification.some_sem (fun (y : Fin 5) => isRing y ∧ hasRing x y) isIcy

Without narrowing, the naive reading for every planet, it has an icy ring is false: the ring-less planet 2 falsifies it.

theorem Barker1995.narrowing_flips_truth_value : Possessive.Poss Quantification.every_sem isPlanet Quantification.some_sem hasRing isRing isIcy ∧ ¬Quantification.every_sem isPlanet fun (x : Fin 5) => Quantification.some_sem (fun (y : Fin 5) => isRing y ∧ hasRing x y) isIcy

Narrowing is truth-conditionally active in this model: the narrowed reading is true exactly where the un-narrowed reading is false. This is Barker's narrowing — quantification ranges only over possessors with a possessee.

Definiteness and the capability mixins

A definite possessive ("the boy's cat") and a relational possessive ("John's sisters"), exercising the possessive-carrier capability mixins (HasIotaWitness, HasPossessor, HasPossessionRelation).

def Barker1995.theBoysCat : Possessive.Definite (Fin 3) Unit

"the boy's cat": possessor 0 (the boy), with a uniquely-identified cat 1. Entities are Fin 3 (boy, cat, dog); one situation.

Equations

• Barker1995.theBoysCat = { possessor := 0, predicate := fun (y : Fin 3) (x : Unit) => y = 1, presupposition := Barker1995.theBoysCat._proof_2 }

theorem Barker1995.theBoysCat_unique (s : Unit) : ∃! y : Fin 3, HasPossesseePredicate.possesseePredicate theBoysCat y s

The definite possessive denotes a unique possessee, inherited from its HasIotaWitness instance via existsUnique_possessee — no bespoke proof.

def Barker1995.sibling : Fin 3 → Fin 3 → Prop

The sibling relation: 0's siblings are 1 and 2.

Equations

• Barker1995.sibling x y = (x = 0 ∧ (y = 1 ∨ y = 2))

def Barker1995.johnsSisters : Possessive.Carrier (Fin 3) Unit

"John's sisters": possessor 0 (John), with the sibling relation as the possession relation (a relational noun, so the restrictor is trivial).

Equations

• Barker1995.johnsSisters = { possessor := 0, relation := fun (x y : Fin 3) (x_1 : Unit) => Barker1995.sibling x y, restrictor := fun (x : Fin 3) (x_1 : Unit) => True }

theorem Barker1995.johnsSisters_possesseeSet (y : Fin 3) (s : Unit) : possesseeSet johnsSisters y s ↔ sibling 0 y

The relational possessive's possesseeSet is its lexical possession relation applied to the possessor — derived through the HasPossessor and HasPossessionRelation instances.

Narrowing through a carrier

The same narrowing, now for a type ⟨1⟩ possessor ("planet 2's rings"). A carrier bundles a single possessor, so narrowing surfaces as existential import: routed through the unified carrierGQ denotation, planet 2's rings are icy is false because planet 2 has no ring. Reuses the planets/rings model above.

def Barker1995.planet2sRings : Possessive.Carrier (Fin 5) Unit

"planet 2's rings": possessor 2, with hasRing as the possession relation.

Equations

• Barker1995.planet2sRings = { possessor := 2, relation := fun (x y : Fin 5) (x_1 : Unit) => Barker1995.hasRing x y, restrictor := fun (y : Fin 5) (x : Unit) => Barker1995.isRing y }

theorem Barker1995.planet2sRings_no_icy_rings : ¬Possessive.carrierGQ planet2sRings Quantification.some_sem () isRing isIcy

Planet 2's rings are icy is false: via the unified carrier denotation, existential import (carrierGQ_existential_import) requires planet 2 to possess a ring, but it has none — narrowing at the individual level.