Possessive Quantifiers

[PW06] [Bar11]

Poss Q₁ C Q₂ R composes a possessor quantifier Q₁ restricted by C ("every student's"), a possessee quantifier Q₂ (typically covert), and a possession relation R: "every student's cat sleeps" = Poss every student a own cat sleep. The possessor restrictor is narrowed by dom A R to those who possess an A-thing (narrowing: [Bar95b] p. 139); PossW is the variant for type ⟨1⟩ possessor NPs taken whole ("John's"), which keeps narrowing in the scope.

Main declarations

• dom, Poss, PossW: P&W (7.27), (7.30), (7.44)–(7.45)
• poss_conservative, possW_conservative: conservativity inherits from Q₂ (P&W (7.29))
• poss_scopeUpMono_of_up_up (and the three other sign combinations): scope monotonicity inheritance (P&W Proposition 5, §7.13)
• poss_eq_possW_restrict: narrowing is vacuous for symmetric conservative Q₁ (P&W Fact 1, §7.8.1)
• possW_individual_existential_import: "John's A B" entails John possesses an A-thing ([PW13])
• possessiveAsNPQ_iff_possW: [Bar11]'s type ⟨1⟩ possessive (Possessive.asNPQ) is PossW of a Montagovian individual with existential Q₂
• poss_not_quantityInvariant: possessive GQs with a fixed R are not isomorphism-invariant (P&W p. 256)

Domain narrowing

def Possessive.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 (the α → Prop-valued relative of Rel.preimage). [PW06] (7.27), p. 254.

Equations

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

Possessive operators

def Possessive.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)

where Rₓ y = R x y. Domain narrowing restricts the possessor domain to members of C who possess some A-thing. [PW06] (7.30), p. 256 — the CONSERV+EXT form of (7.28); on a fixed carrier the universe-extension clause is moot.

Equations

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

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

Possessive quantifier built from a type ⟨1⟩ possessor NP taken whole ("John's", "most students'" — the restrictor is not recoverable from Q):

PossW Q Q₂ R A B = Q (dom A R ∩ {a | Q₂ (A ∩ Rₐ) B})

Narrowing stays in the scope, preserving possessive existential import ("John's dogs bark" requires John to own a dog). [PW06] (7.44)–(7.45), pp. 259–260 (Possʷ).

Equations

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

Conservativity (P&W (7.29))

theorem Possessive.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 inheritance: if Q₂ is conservative, so is Poss Q₁ C Q₂ R, for any Q₁. [PW06] (7.29), p. 255.

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

Conservativity inheritance for the type ⟨1⟩ variant. [PW06] remark after (7.44).

Scope monotonicity (P&W Proposition 5, §7.13)

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

theorem Possessive.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 Possessive.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 Possessive.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 Possessive.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 (P&W Fact 1, §7.8.1)

theorem Possessive.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 agrees with PossW at Q₁ frozen to C. Narrowing only matters for non-intersective Q₁ (proportionals like "most students'"). [PW06] Fact 1, §7.8.1, p. 260.

Existential import

theorem Possessive.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). [PW13]'s headline thesis, at the individual instance.

Denoting a bundled carrier

A possessive carrier bundling a possessor and a possession relation (any HasPossessor + HasPossessionRelation instance, e.g. Possessive.Carrier) denotes, at a situation, as the PossW of its possessor taken whole. Routing every carrier through one operator is what makes the API unified: a carrier inherits narrowing and existential import with no bespoke proof.

def Possessive.carrierGQ {γ : Type u_2} {E : Type u_3} {S : Type u_4} [HasPossessor γ E] [HasPossessionRelation γ E S] (a : γ) (Q₂ : Quantification.GQ E) (s : S) : Quantification.GQ E

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

Equations

• Possessive.carrierGQ a Q₂ s = Possessive.PossW (Quantification.individual (HasPossessor.possessor a)) Q₂ fun (x y : E) => HasPossessionRelation.possessionRelation a x y s

theorem Possessive.carrierGQ_existential_import {γ : Type u_2} {E : Type u_3} {S : Type u_4} [HasPossessor γ E] [HasPossessionRelation γ E S] (a : γ) (Q₂ : Quantification.GQ E) (s : S) {A B : E → Prop} (h : carrierGQ a Q₂ s A B) : ∃ (b : E), A b ∧ HasPossessionRelation.possessionRelation a (HasPossessor.possessor a) b s

Every carrier inherits existential import: if its denotation holds of possessee class A and scope B, the possessor stands in the possession relation to some A-thing. Free from possW_individual_existential_import.

Bridge to Barker's type ⟨1⟩ possessive

theorem Possessive.possessiveAsNPQ_iff_possW {E : Type u_2} (a : E) (R : E → E → Bool) (P : E → Prop) : asNPQ a R P ↔ PossW (Quantification.individual a) Quantification.some_sem (fun (x y : E) => R x y = true) (fun (x : E) => True) P

[Bar11]'s possessive NPQ (⟦John's⟧ = fun P => ∃ y, R j y ∧ P y, Possessive.asNPQ) 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 Possessive.poss_not_quantityInvariant : ¬Quantification.QuantityInvariant (Poss Quantification.some_sem (fun (x : Bool) => True) Quantification.some_sem fun (x y : Bool) => x = true ∧ y = true)

Possessive GQs with a fixed possession relation are not isomorphism-invariant: permuting Bool by not flips some (· = true)'s (·) (⊤) from true to false, because R does not travel along the permutation. [PW06] p. 256 ("due to the presence of the fixed set C and relation R, Poss(Q₁,C,Q₂,R) is almost never Isom"; the four-argument operation Poss itself is Isom, Ch 9.2.3).