{W : Type u_1} {E : Type u_2} (Q N : W → E → Prop) (w : W) (x : E) :
intersective Q N w x ↔ Q w x ∧ N w x
Docs / Semantics / Modification / Classification
Modifiers of intensional properties
import Linglib.Semantics.Modification.Classification · namespace Modifier
An intensional property is a function from worlds to predicates of entities, and attributive
adjectives denote modifiers of intensional properties. At these modifiers Kamp's order-theoretic
classes (Semantics/Modification/Basic.lean) take their familiar pointwise form, an intersective
modifier is extensional, and a privative modifier that holds of something is not subsective. The
classification descends from Parsons and Kamp through Kamp and Partee; the labels are Partee's.
Main results
Modifier.isIntersective_iff_exists_forall,Modifier.isPrivative_iff_forall: the classes stated pointwise for modifiers of intensional properties,W → E → Prop.Modifier.IsIntersective.isExtensional: intersective modifiers are extensional.Modifier.IsPrivative.not_isSubsective: a privative modifier that holds of something is not subsective.
Implementation notes
Extensionality is independent of the classes; Studies/Kamp1975.lean gives the witnesses.
Whether adjectives uniformly denote Modifier (W → E → Prop) is a theoretical claim
(Studies/Elbourne2026.lean).
References
- Parsons 1970, Some Problems Concerning the Logic of Grammatical Modifiers
- Kamp 1975, Two theories about adjectives formalized
- Kamp & Partee 1995, Prototype theory and compositionality
Declarations
A modifier of intensional properties is intersective if and only if it conjoins every noun with one fixed property, as gray does.
A modifier of intensional properties is privative if and only if nothing it yields from a noun falls under the noun, as with fake.
Intersective modifiers are extensional, since the meet with a fixed property reads the noun only through its extension at each world.
A privative modifier that holds of something is not subsective.
{W : Type u_1} {E : Type u_2} {adj : Modifier (W → E → Prop)} (hp : adj.IsPrivative) (hne : ∃ (N : W → E → Prop) (w : W) (x : E), adj N w x) :
¬adj.IsSubsective