Modifier-meaning classification at the intensional carrier #
We instantiate the order-theoretic modifier classes of
Modification/Basic.lean at intensional properties. The classification
goes back to [Par70] and [Kam75] (definitions (4)–(7)) and
was consolidated in [KP95]; the modern labels are Partee's.
Main definitions #
Property W E: intensional properties,Intensional.Intension W (E → Prop).isIntersective_iff,isPrivative_iff: pointwise forms of the order-theoretic classes at this carrier.isExtensional_of_isIntersective: intersective modifier meanings areIntensional.IsExtensional.not_isSubsective_of_isPrivative: privative meanings with non-empty extension are not subsective.RevisedClass: [Par10]'s three-class hierarchy after the privative collapse.
Implementation notes #
Extensionality is orthogonal to the entailment hierarchy; the
independence witnesses are in Studies/Kamp1975.lean. Whether
adjectives uniformly denote Modifier (Property W E) is a
theoretical claim (Studies/Elbourne2026.lean); the carrier is named
for the denotation type, not the word class.
An intensional property: an Intensional.Intension valued in
characteristic predicates over entities (a function from worlds to
predicates).
Equations
- Modification.Property W E = Intensional.Intension W (E → Prop)
Instances For
Pointwise forms of the order-theoretic classes #
Pointwise form of Modifier.isIntersective at the intensional
carrier: the extension at each world is the intersection of the
noun's extension with some fixed property Q ([Kam75]
definition (4), "predicative").
Examples: "gray", "French", "carnivorous", "four-legged".
Pointwise form of Modifier.isPrivative at the intensional carrier:
the extension is always disjoint from the noun's extension
([Kam75] definition (5)).
Examples: "fake", "counterfeit". [Par10] argues this class should be eliminated.
Implication structure #
Intersective → subsective holds at any carrier
(`Modifier.isIntersective.isSubsective`); intersective → extensional
and the privative/subsective incompatibility are stated here. The
order-theoretic core of the latter is `Modifier.isPrivative.eq_bot`.
Intersective modifier meanings are extensional: meet with a fixed property reads the noun only through its extension at each world.
Privative modifier meanings are not subsective (when the modifier has non-empty extension for some noun).
Revised hierarchy ([Par10]) #
The post-collapse 3-class hierarchy after eliminating "privative" via
noun coercion. Per [Par10] footnote 1, the hierarchy is
subset-ordered (intersective ⊂ subsective ⊂ unrestricted), not linear;
the enum picks the narrowest fit per adjective. The licensing
mechanism (NVP + HPP) is in
Semantics/Modification/Coercion.lean.
Adjective hierarchy after [Par10]'s collapse: the privative class is eliminated in favor of subsective + noun coercion.
- intersective : RevisedClass
⟦A N⟧ = ⟦Q⟧ ∩ ⟦N⟧(Kamp's intersective). - subsective : RevisedClass
⟦A N⟧ ⊆ ⟦N*⟧— includes former "privatives" via coercion. - nonSubsective : RevisedClass
No entailment: alleged, potential, putative (the plain/modal non-subsective class).
Instances For
Equations
- Modification.instDecidableEqRevisedClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Predicate-level interpretation of RevisedClass. Per the subset
ordering, intersective and subsective are not disjoint: every
intersective modifier meaning satisfies Modifier.isSubsective
(Modifier.isIntersective.isSubsective).
Caveat on .nonSubsective: the membership condition ¬ isSubsective adj is necessary but coarse — it also holds of Kamp-privatives,
which under Partee's reanalysis are not supposed to exist as a
natural class. Read .nonSubsective as Partee's intended "modal"
class (alleged, potential, putative); the bare predicate
¬ isSubsective over-generates.