Docs / Semantics / Modification / Coercion

Noun coercion licensed by non-vacuity

import Linglib.Semantics.Modification.Coercion

Kamp and Partee's non-vacuity principle asks that a predicate have both a positive and a negative extension in its local domain, and their head primacy principle makes the extension of the head noun the local domain of its modifier. A privative adjective is never non-vacuous within its head, and neither is a tautologous one such as real. Partee's proposal is that the head is then shifted, as a last resort, to include the adjective's value, fur to real or fake fur, so that the compound becomes non-vacuous.

Main definitions

IsNonVacuous P w d: P has a positive and a negative extension within d at w.
Modifier.ShiftsHead adj N w: adj N is vacuous within N and non-vacuous within N widened by the adjective's value, so Partee's rule shifts the head.

Main statements

Modifier.IsPrivative.not_isNonVacuous, not_isNonVacuous_self: privative and tautologous modifiers are vacuous within their head.
Modifier.IsPrivative.shiftsHead_iff: a privative adjective shifts its head exactly when there are both things in its value and things in the noun.
Modifier.not_shiftsHead_of_isNonVacuous: a compound already non-vacuous within its head is not shifted.

Implementation notes

The principles are Kamp and Partee's (NVP) and (HPP), Partee's (18) and (20), with head primacy in its simplest form, which makes the local domain the positive extension of the head. IsNonVacuous is bivalent, simplifying the partial setting of Kamp and Partee. Complement coercion (Studies/Pustejovsky1995.lean) and the type shifts of noun phrases (Semantics/Quantification/Individual.lean) are different notions.

References

Kamp & Partee 1995, Prototype theory and compositionality
Partee 2010, Privative adjectives: Subsective plus coercion formalized

Declarations

P is non-vacuous within d at w when both its positive and its negative extension at w meet d.

def IsNonVacuous L48–51

{W : Type u_1} {E : Type u_2} (P : W → E → Prop) (w : W) (d : E → Prop) :

Prop

IsNonVacuous P w d = ((∃ (x : E), d x ∧ P w x) ∧ ∃ (x : E), d x ∧ ¬P w x)

Used by IsNonVacuous.mono, isNonVacuous_of_disjoint, not_isNonVacuous_self, isNonVacuous_sup_self_iff, Modifier.IsPrivative.not_isNonVacuous, Modifier.ShiftsHead, Modifier.not_shiftsHead_of_isNonVacuous

Used in DelPinal2015, Partee2010

L53–55

L57–59

No predicate is non-vacuous within its own extension, so a tautologous modifier such as real, whose value is the noun, is vacuous within its head.

theorem not_isNonVacuous_self L61–64

{W : Type u_1} {E : Type u_2} (P : W → E → Prop) (w : W) :

¬IsNonVacuous P w (P w)

Built from

L66–69

A privative modifier is never non-vacuous within the extension of its noun, the local domain that head primacy assigns.

theorem Modifier.IsPrivative.not_isNonVacuous L73–77

{W : Type u_1} {E : Type u_2} {adj : Modifier (W → E → Prop)} (hp : adj.IsPrivative) (N : W → E → Prop) (w : W) :

¬IsNonVacuous (adj N) w (N w)

Built from

adj shifts the head N at w when adj N is vacuous within N, the local domain that head primacy assigns, and non-vacuous within N widened to include the adjective's value.

def Modifier.ShiftsHead L79–82

{W : Type u_1} {E : Type u_2} (adj : Modifier (W → E → Prop)) (N : W → E → Prop) (w : W) :

Prop

adj.ShiftsHead N w = (¬IsNonVacuous (adj N) w (N w) ∧ IsNonVacuous (adj N) w (N w ⊔ adj N w))

Built from

Used by Modifier.not_shiftsHead_of_isNonVacuous, Modifier.IsPrivative.shiftsHead_iff

Used in DelPinal2015, Partee2010

A compound already non-vacuous within its head does not shift the head.

theorem Modifier.not_shiftsHead_of_isNonVacuous L86–89

{W : Type u_1} {E : Type u_2} {adj : Modifier (W → E → Prop)} {N : W → E → Prop} {w : W} (h : IsNonVacuous (adj N) w (N w)) :

¬adj.ShiftsHead N w

Built from ,

A privative adjective shifts its head exactly when there are things in its value and things in the noun, so fake fur widens fur just when there are fake furs and real furs.

theorem Modifier.IsPrivative.shiftsHead_iff L91–97

{W : Type u_1} {E : Type u_2} {adj : Modifier (W → E → Prop)} {N : W → E → Prop} {w : W} (hp : adj.IsPrivative) :

adj.ShiftsHead N w ↔ (∃ (x : E), adj N w x) ∧ ∃ (x : E), N w x

Built from