Modification-time coercion (NVP + HPP)

LicensedCoercion and ParteeReanalysis: type-level architecture for noun-extension shifts under the Non-Vacuity Principle and Head Primacy Principle of [KP95]. Consumed by Studies/Partee2010.lean.

Main definitions

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

References

• [KP95] formulae 18 (NVP), 20 (HPP), p. 161.
• [Par10] § 4.

def Semantics.Composition.Coercion.NonVacuous {W : Type u_1} {E : Type u_2} (P : Gradability.Classification.Property W E) (w : W) (d : Set E) : Prop

Both positive and negative extensions of P at w intersect d.

Equations

• Semantics.Composition.Coercion.NonVacuous P w d = (({x : E | P w x} ∩ d).Nonempty ∧ ({x : E | ¬P w x} ∩ d).Nonempty)

structure Semantics.Composition.Coercion.LicensedCoercion {W : Type u_1} {E : Type u_2} (N : Gradability.Classification.Property W E) (adj : Gradability.Classification.AdjMeaning 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).

• shift : Gradability.Classification.Property W E
• shift_supseteq : {x : E | N w x} ⊆ {x : E | self.shift w x}
• satisfies_nvp : NonVacuous (adj self.shift) w {x : E | self.shift w x}

structure Semantics.Composition.Coercion.ParteeReanalysis {W : Type u_1} {E : Type u_2} (adj_classical : Gradability.Classification.AdjMeaning W E) : Type (max u_1 u_2)

Reanalysis of adj_classical as subsective-after-coercion. The coercion is NVP-conditional: shift_inert requires noun_shift N = N whenever direct application is already non-vacuous, so the structure does not coerce gratuitously.

• noun_shift : Gradability.Classification.Property W E → Gradability.Classification.Property W E
• adj_subsective : Gradability.Classification.AdjMeaning W E
• shift_supseteq (N : Gradability.Classification.Property W E) (w : W) : {x : E | N w x} ⊆ {x : E | self.noun_shift N w x}
• is_subsective : Gradability.Classification.isSubsective self.adj_subsective
• shift_inert (N : Gradability.Classification.Property W E) (w : W) : NonVacuous (adj_classical N) w {x : E | N w x} → self.noun_shift N = N