Modifiers

[Par70] [Kam75]

A modifier of τ is a function on the modificand's denotation ([Par70]: modifiers as functions on predicates). Adjectives, adverbs, and relative clauses are all modifiers — of different τ (nominal e ⇒ t, event Event → Prop, …) — unified by being this type, not by implementing an interface.

The [Kam75] meaning-postulate classification is order-theoretic and is stated here at that generality: over an ordered carrier, subsective modifiers are deflationary (m x ≤ x), privative modifiers have output disjoint from the modificand, and intersective modifiers are meet-translations (m x = q ⊓ x; at α → Prop, pointwise conjunction). The intensional hierarchy (Modification/Classification.lean) and its single-world specializations (Studies/Kamp1975.lean § 1) are these classes at the carriers W → E → Prop and E → Prop.

Main declarations

• Modifier — a modifier of τ is an endofunction τ → τ.
• Modifier.intersective — the intersective modifier built from q: meet the modificand with q.
• Modifier.isIntersective / .isSubsective / .isPrivative — the [Kam75] classification over an ordered carrier.

@[reducible, inline]

abbrev Modifier (τ : Type u_1) : Type u_1

A modifier of τ is a function on the modificand's denotation ([Par70]). Adjectives, adverbs, and relative clauses are modifiers of different τ; they compose as endofunctions (modifier stacking).

Equations

• Modifier τ = (τ → τ)

def Modifier.isSubsective {α : Type u_1} [LE α] (m : Modifier α) : Prop

A modifier over an ordered carrier is subsective if its output lies below the modificand: a skillful surgeon is a surgeon.

Equations

• m.isSubsective = ∀ (x : α), m x ≤ x

theorem Modifier.isSubsective_iff_le_id {α : Type u_1} [LE α] {m : Modifier α} : m.isSubsective ↔ m ≤ id

Subsectivity is the deflationary condition in the pointwise order on modifiers.

def Modifier.isPrivative {α : Type u_1} [PartialOrder α] [OrderBot α] (m : Modifier α) : Prop

A modifier is privative if its output is disjoint from the modificand: a fake gun is not a gun.

Equations

• m.isPrivative = ∀ (x : α), Disjoint (m x) x

theorem Modifier.isPrivative.eq_bot {α : Type u_1} [PartialOrder α] [OrderBot α] {m : Modifier α} (hp : m.isPrivative) (hs : m.isSubsective) (x : α) : m x = ⊥

A modifier that is both privative and subsective sends every modificand to ⊥ — the order-theoretic core of "privative is incompatible with subsective".

def Modifier.isIntersective {α : Type u_1} [SemilatticeInf α] (m : Modifier α) : Prop

A modifier is intersective if it is meet with some fixed element.

Equations

• m.isIntersective = ∃ (q : α), ∀ (x : α), m x = q ⊓ x

theorem Modifier.isIntersective.isSubsective {α : Type u_1} [SemilatticeInf α] {m : Modifier α} (h : m.isIntersective) : m.isSubsective

Intersective ⟹ subsective ([Kam75]'s implication structure).

def Modifier.intersective {α : Type u_1} [SemilatticeInf α] (q : α) : Modifier α

The intersective modifier built from q: meet the modificand with q. At α → Prop this is pointwise conjunction; at conjoinable Denot domains (Intensional/Algebra.lean instances) it is Partee-Rooth generalized conjunction with the head. The well-behaved special case (restrictive relative clauses, intersective adjectives, manner adverbs).

Equations

• Modifier.intersective q x✝ = q ⊓ x✝

@[simp]

theorem Modifier.intersective_apply {β : Type u_2} (P Q : β → Prop) (x : β) : intersective P Q x = (P x ∧ Q x)

theorem Modifier.intersective_comm {α : Type u_1} [SemilatticeInf α] (q r : α) : intersective q r = intersective r q

Modificand and modifier meet symmetrically.

theorem Modifier.intersective_isIntersective {α : Type u_1} [SemilatticeInf α] (q : α) : (intersective q).isIntersective