Possessive quantifiers

The possessive determiner as a generalized quantifier, after [PW06] Chapter 7. Poss Q₁ C Q₂ R composes a possessor quantifier Q₁ restricted by C (every student's), a possessee quantifier Q₂ (implicit in John's bikes, explicit in several of John's CDs), and a possession relation R, narrowing the possessor domain by dom A R to those who possess an A-thing ([barker-1995]'s narrowing). PossW is the variant for a type ⟨1⟩ possessor taken whole (John's), with the narrowing conjunct inside the scope. Which Q₂ a bare possessive carries — the universal reading, the definite allei of the "definiteness account", an existential — is the parameter the definiteness debate turns on ([PW06] §7.8.2, [coppock-beaver-2015] §4); nothing here fixes it.

Main declarations

• dom, Poss, PossW — their (7.27), (7.30), (7.45).
• Description.toGQ — a description's possessor and relation, frozen at a situation, fed to PossW.

Main statements

• poss_conservative, possW_conservative — conservativity inherits from Q₂ alone (the CONSERV half of their (7.29), with no hypothesis on Q₁).
• poss_scopeUpMono_of_up_up and its three sign variants — Proposition 5 (§7.13): the right monotonicity of Poss is the product of the signs of Q₁ and Q₂.
• poss_eq_possW_restrict — Fact 1 (§7.8.1): for a symmetric conservative Q₁, narrowing is vacuous.
• possW_individual_existential_import, Description.toGQ_existential_import — John's A B entails that John possesses an A-thing: the dom conjunct of (7.45).
• asNPQ_iff_possW — [barker-2011]'s type ⟨1⟩ possessive is PossW at a Montagovian individual with existential Q₂.
• poss_not_quantityInvariant — with C and R fixed, Poss Q₁ C Q₂ R is "almost never Isom" (p. 256).

References

• [PW06], Chapter 7; [peters-westerstahl-2013] is the article-length treatment.
• [barker-1995], [barker-2011], [coppock-beaver-2015].

Domain narrowing

def Possession.dom {α : Type u_1} (A : α → Prop) (R : α → α → Prop) : α → Prop

dom A R = {a | ∃ b ∈ A, R a b}, the possessors of at least one A-thing — their (7.27), p. 254; Ex (π A R) at a fixed situation.

Equations

• Possession.dom A R a = ∃ (b : α), A b ∧ R a b

Possessive operators

def Possession.Poss {α : Type u_1} (Q₁ : Quantification.GQ α) (C : α → Prop) (Q₂ : Quantification.GQ α) (R : α → α → Prop) : Quantification.GQ α

Possessive quantifier built from a type ⟨1,1⟩ possessor quantifier: Poss Q₁ C Q₂ R A B = Q₁ (C ∩ dom A R) (fun x => Q₂ (A ∩ Rₓ) B) with Rₓ y = R x y; narrowing restricts the possessor domain to members of C who possess some A-thing. Their (7.30), p. 255 — the form of (7.28) for conservative, extensional Q₁ and Q₂, where the universe-extension clause is moot.

Equations

• Possession.Poss Q₁ C Q₂ R A B = Q₁ (fun (x : α) => C x ∧ Possession.dom A R x) fun (x : α) => Q₂ (fun (y : α) => A y ∧ R x y) B

def Possession.PossW {α : Type u_1} (Q : Quantification.Quantifier α) (Q₂ : Quantification.GQ α) (R : α → α → Prop) : Quantification.GQ α

Possessive quantifier built from a type ⟨1⟩ possessor NP taken whole (John's, most students', where the restrictor is not recoverable from Q): PossW Q Q₂ R A B = Q (dom A R ∩ {a | Q₂ (A ∩ Rₐ) B}). The narrowing conjunct sits in the scope, so John's dogs bark requires John to own a dog. Their (7.45), p. 260 — the form of (7.44) for extensional Q and conservative, extensional Q₂.

Equations

• Possession.PossW Q Q₂ R A B = Q fun (a : α) => Possession.dom A R a ∧ Q₂ (fun (y : α) => A y ∧ R a y) B

Conservativity

theorem Possession.poss_conservative {α : Type u_1} {Q₁ Q₂ : Quantification.GQ α} (C : α → Prop) (R : α → α → Prop) (h₂ : Quantification.Conservative Q₂) : Quantification.Conservative (Poss Q₁ C Q₂ R)

Conservativity inherits from Q₂, for any Q₁: the possessee restrictor A ∩ Rₓ refines A, so a conservative Q₂ cannot tell B from A ∩ B in the scope (the CONSERV half of their (7.29), p. 255).

theorem Possession.possW_conservative {α : Type u_1} {Q : Quantification.Quantifier α} {Q₂ : Quantification.GQ α} (R : α → α → Prop) (h₂ : Quantification.Conservative Q₂) : Quantification.Conservative (PossW Q Q₂ R)

Conservativity inheritance for the type ⟨1⟩ variant (their remark after (7.44)).

Scope monotonicity (Proposition 5, §7.13, p. 288)

B occurs only in Q₂'s scope, so monotonicity composes: same signs give Mon↑, opposite signs give Mon↓.

theorem Possession.poss_scopeUpMono_of_up_up {α : Type u_1} {Q₁ Q₂ : Quantification.GQ α} (C : α → Prop) (R : α → α → Prop) (h₁ : Quantification.ScopeUpwardMono Q₁) (h₂ : Quantification.ScopeUpwardMono Q₂) : Quantification.ScopeUpwardMono (Poss Q₁ C Q₂ R)

Q₁ Mon↑, Q₂ Mon↑ ⇒ Poss Mon↑ in scope.

theorem Possession.poss_scopeDownMono_of_up_down {α : Type u_1} {Q₁ Q₂ : Quantification.GQ α} (C : α → Prop) (R : α → α → Prop) (h₁ : Quantification.ScopeUpwardMono Q₁) (h₂ : Quantification.ScopeDownwardMono Q₂) : Quantification.ScopeDownwardMono (Poss Q₁ C Q₂ R)

Q₁ Mon↑, Q₂ Mon↓ ⇒ Poss Mon↓ in scope.

theorem Possession.poss_scopeUpMono_of_down_down {α : Type u_1} {Q₁ Q₂ : Quantification.GQ α} (C : α → Prop) (R : α → α → Prop) (h₁ : Quantification.ScopeDownwardMono Q₁) (h₂ : Quantification.ScopeDownwardMono Q₂) : Quantification.ScopeUpwardMono (Poss Q₁ C Q₂ R)

Q₁ Mon↓, Q₂ Mon↓ ⇒ Poss Mon↑ in scope.

theorem Possession.poss_scopeDownMono_of_down_up {α : Type u_1} {Q₁ Q₂ : Quantification.GQ α} (C : α → Prop) (R : α → α → Prop) (h₁ : Quantification.ScopeDownwardMono Q₁) (h₂ : Quantification.ScopeUpwardMono Q₂) : Quantification.ScopeDownwardMono (Poss Q₁ C Q₂ R)

Q₁ Mon↓, Q₂ Mon↑ ⇒ Poss Mon↓ in scope.

Narrowing vacuity (Fact 1, §7.8.1, p. 260)

theorem Possession.poss_eq_possW_restrict {α : Type u_1} {Q₁ : Quantification.GQ α} (hSym : Quantification.QSymmetric Q₁) (hCons : Quantification.Conservative Q₁) (C : α → Prop) (Q₂ : Quantification.GQ α) (R : α → α → Prop) : Poss Q₁ C Q₂ R = PossW (Quantification.restrict Q₁ C) Q₂ R

For a symmetric conservative possessor quantifier, domain narrowing is vacuous: Poss Q₁ C Q₂ R is PossW at Q₁ frozen to C. Narrowing only matters for non-intersective Q₁ (proportionals like most students').

Existential import

theorem Possession.possW_individual_existential_import {α : Type u_1} {Q₂ : Quantification.GQ α} {R : α → α → Prop} {a : α} {A B : α → Prop} (h : PossW (Quantification.individual a) Q₂ R A B) : ∃ (b : α), A b ∧ R a b

John's A B carries existential import: whatever Q₂ is, it entails that John possesses an A-thing — the dom conjunct of (7.45).

Denoting a description

def Possession.Description.toGQ {E : Type u_2} {S : Type u_3} (d : Description E S) (Q₂ : Quantification.GQ E) (s : S) : Quantification.GQ E

The quantificational denotation of a possessive description at a situation s: its possessor, as an individual NP, and its relation frozen at s, fed to PossW; Q₂ is the (usually covert) possessee quantifier.

Equations

• d.toGQ Q₂ s = Possession.PossW (Quantification.individual d.possessor) Q₂ fun (x y : E) => d.relation x y s

theorem Possession.Description.toGQ_existential_import {E : Type u_2} {S : Type u_3} (d : Description E S) (Q₂ : Quantification.GQ E) (s : S) {A B : E → Prop} (h : d.toGQ Q₂ s A B) : ∃ (b : E), A b ∧ d.relation d.possessor b s

A description's denotation carries existential import: if it holds of possessee class A and scope B, the possessor stands in the relation to some A-thing.

Barker's type ⟨1⟩ possessive

theorem Possession.asNPQ_iff_possW {α : Type u_1} (a : α) (R : α → α → Prop) (P : α → Prop) : asNPQ a R P ↔ PossW (Quantification.individual a) Quantification.some_sem R (fun (x : α) => True) P

[barker-2011]'s possessive quantifier asNPQ (⟦John's⟧ = fun P => ∃ y, R j y ∧ P y) is PossW at a Montagovian individual with existential Q₂ and trivial possessee restrictor — the possessee class is folded into R by Barker's π shift.

Non-logicality

theorem Possession.poss_not_quantityInvariant : ¬Quantification.QuantityInvariant (Poss Quantification.some_sem (fun (x : Bool) => True) Quantification.some_sem fun (x y : Bool) => x = true ∧ y = true)

With a fixed possession relation, possessive GQs are not isomorphism-invariant: permuting Bool by not flips some (· = true)'s (·) (⊤) from true to false, because R does not travel along the permutation. "Due to the presence of the fixed set C and relation R, Poss(Q₁, C, Q₂, R) is almost never Isom" (p. 256); an operation closely related to Poss itself is Isom (their Chapter 9.2).