Modification-time noun coercion (NVP + HPP)

Noun-extension widening under the Non-Vacuity and Head Primacy Principles of [KP95], used by [Par10] to reanalyse privative adjectives as subsective-after-coercion; both principles are anticipated in [Kam75] § 7.

Main definitions

• isNonVacuous P w d: NVP at world w within local domain d.
• LicensedCoercion N adj w: NVP-licensed widening of N.
• SubsectiveReanalysis adjClassical: reanalysis as subsective-after-coercion.

Implementation notes

This models the fake-fur widening of [Par10] § 4 (its formulae (18) and (20)); the constitutive-material case (stone lion) is bracketed there. isNonVacuous states the NVP bivalently, simplifying [KP95]'s partial setting. Not to be confused with complement coercion (Studies/Pustejovsky1995.lean), NP type-shifting (Semantics/Composition/TypeShifting.lean), or aspectual coercion (Semantics/Aspect/Composition.lean).

def Modification.isNonVacuous {W : Type u_1} {E : Type u_2} (P : Property W E) (w : W) (d : E → Prop) : Prop

Both the positive and the negative extension of P at w meet the local domain d.

Equations

• Modification.isNonVacuous P w d = ((∃ (x : E), d x ∧ P w x) ∧ ∃ (x : E), d x ∧ ¬P w x)

theorem Modification.isNonVacuous.mono {W : Type u_1} {E : Type u_2} {P : Property W E} {w : W} {d d' : E → Prop} (h : isNonVacuous P w d) (hdd' : d ≤ d') : isNonVacuous P w d'

isNonVacuous is monotone in the local domain.

theorem Modification.isNonVacuous_compl {W : Type u_1} {E : Type u_2} {P : Property W E} {w : W} {d : E → Prop} : isNonVacuous (fun (w : W) (x : E) => ¬P w x) w d ↔ isNonVacuous P w d

The NVP is self-dual: a predicate and its complement are non-vacuous in the same local domains.

structure Modification.LicensedCoercion {W : Type u_1} {E : Type u_2} (N : Property W E) (adj : Modifier (Property W E)) (w : W) : Type (max u_1 u_2)

A wider noun extension shift ⊇ N at w under which adj shift is non-vacuous in shift's extension (the HPP local domain). The shift is a full intension although licensing holds at the single world w: a non-extensional adj reads its values at other worlds.

• shift : Property W E
• le_shift : N w ≤ self.shift w
• satisfies_nvp : isNonVacuous (adj self.shift) w (self.shift w)

structure Modification.SubsectiveReanalysis {W : Type u_1} {E : Type u_2} (adjClassical : Modifier (Property W E)) : Type (max u_1 u_2)

Reanalysis of adjClassical as subsective-after-coercion. The coercion is NVP-conditional — [Par10]'s coercion-as-last-resort: shift_inert forbids widening whenever direct application is already non-vacuous (nounShift_eq_self derives the identity).

• nounShift : Property W E → Property W E
• adjSubsective : Modifier (Property W E)
• le_nounShift (N : Property W E) : N ≤ self.nounShift N
• is_subsective : self.adjSubsective.isSubsective
• shift_inert (N : Property W E) (w : W) : isNonVacuous (adjClassical N) w (N w) → self.nounShift N ≤ N

theorem Modification.SubsectiveReanalysis.nounShift_eq_self {W : Type u_1} {E : Type u_2} {adjClassical : Modifier (Property W E)} (R : SubsectiveReanalysis adjClassical) {N : Property W E} {w : W} (h : isNonVacuous (adjClassical N) w (N w)) : R.nounShift N = N

Where direct application is already non-vacuous, the shift is the identity.

def Modification.SubsectiveReanalysis.licensedCoercion {W : Type u_1} {E : Type u_2} {adjClassical : Modifier (Property W E)} (R : SubsectiveReanalysis adjClassical) {N : Property W E} {w : W} (h : isNonVacuous (R.adjSubsective (R.nounShift N)) w (R.nounShift N w)) : LicensedCoercion N R.adjSubsective w

A reanalysis licenses a coercion at every world where the shifted noun renders the reanalysed meaning non-vacuous — the positive counterpart of Partee2010.isPrivative_no_LicensedCoercion.

Equations

• R.licensedCoercion h = { shift := R.nounShift N, le_shift := ⋯, satisfies_nvp := h }