Modifiers

A modifier of τ is a function from τ to itself, as Parsons treats adjectives and adverbs as functions on the predicates they modify; adjectives, adverbs and relative clauses are modifiers of different types τ, and modifiers stack by composition. Kamp's classification of adjective meanings is order-theoretic: over an ordered type, a modifier is subsective when it maps each argument below itself, privative when its value is disjoint from its argument, and intersective when it is the meet with a fixed element. Its order dual, a modifier mapping each argument above itself, is extensive.

A modifier of sets can act pointwise, sending a set to the union of the values of a map on its members, which is SetRel.image. The modifiers of numerals and of scalar alternatives are of this kind, and Kamp's classes then read off the map: extensive when every point is in its own value, subsective when no value leaves its point, and privative only for the empty map, while being disjoint from every singleton argument is irreflexivity.

Semantics/Modification/Classification.lean specializes the classes to intensional properties.

Main definitions

• Modifier τ: the functions from τ to τ.
• Modifier.intersective q: the meet with q.
• Modifier.IsSubsective, IsPrivative, IsIntersective: Kamp's classes, and Modifier.IsExtensive, the dual of subsective.
• Modifier.pointwise r: the modifier of sets acting pointwise through r.

Main results

• Modifier.isExtensive_pointwise_iff, isSubsective_pointwise_iff: the classes of a pointwise modifier, read off its map.
• Modifier.isPrivative_pointwise_iff: a pointwise modifier is privative only when its map is empty everywhere.

References

• [Par70]
• [Kam75]

@[reducible, inline]

abbrev Modifier (τ : Type u_1) : Type u_1

A modifier of τ is a function from τ to τ; modifiers stack by composition.

Equations

• Modifier τ = (τ → τ)

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

A modifier m is subsective if m x ≤ x for every x, so that 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

A modifier is subsective if and only if it lies below the identity.

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

A modifier m is privative if m x is disjoint from x for every x, so that 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 everything to ⊥.

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

A modifier is intersective if it is the 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 modifiers are subsective.

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

intersective q meets its argument with q; on predicates it is pointwise conjunction, the meaning of restrictive relative clauses, intersective adjectives and 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

The meet with q applied to r is the meet with r applied to q.

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

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

A modifier m is extensive if x ≤ m x for every x, the order dual of subsective, so that at least three holds of three.

Equations

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

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

theorem Modifier.IsSubsective.comp {α : Type u_1} [Preorder α] {m n : Modifier α} (hm : m.IsSubsective) (hn : n.IsSubsective) : IsSubsective (m ∘ n)

theorem Modifier.IsExtensive.comp {α : Type u_1} [Preorder α] {m n : Modifier α} (hm : m.IsExtensive) (hn : n.IsExtensive) : IsExtensive (m ∘ n)

Pointwise modifiers of sets

def Modifier.pointwise {α : Type u_1} {β : Type u_2} (r : α → Set β) : Set α → Set β

pointwise r sends a set to the union of the values of r on its members.

Equations

• Modifier.pointwise r s = ⋃ a ∈ s, r a

@[simp]

theorem Modifier.mem_pointwise {α : Type u_1} {β : Type u_2} {r : α → Set β} {s : Set α} {b : β} : b ∈ pointwise r s ↔ ∃ a ∈ s, b ∈ r a

@[simp]

theorem Modifier.pointwise_singleton {α : Type u_1} {β : Type u_2} (r : α → Set β) (a : α) : pointwise r {a} = r a

theorem Modifier.pointwise_eq_image {α : Type u_1} {β : Type u_2} (r : α → Set β) (s : Set α) : pointwise r s = SetRel.image {p : α × β | p.2 ∈ r p.1} s

A pointwise modifier is the image under the relation its map is.

theorem Modifier.pointwise_singleton_eq_id {α : Type u_1} : (pointwise fun (a : α) => {a}) = id

theorem Modifier.isExtensive_pointwise_iff {α : Type u_1} {r : α → Set α} : IsExtensive (pointwise r) ↔ ∀ (a : α), a ∈ r a

theorem Modifier.isSubsective_pointwise_iff {α : Type u_1} {r : α → Set α} : IsSubsective (pointwise r) ↔ ∀ (a : α), r a ⊆ {a}

theorem Modifier.isPrivative_pointwise_iff {α : Type u_1} {r : α → Set α} : IsPrivative (pointwise r) ↔ ∀ (a : α), r a = ∅

A pointwise modifier is privative only when its map is empty everywhere, since an argument {a, b} with b ∈ r a meets its own value.

theorem Modifier.disjoint_pointwise_singleton_iff {α : Type u_1} {r : α → Set α} : (∀ (a : α), Disjoint (pointwise r {a}) {a}) ↔ ∀ (a : α), a ∉ r a

A pointwise modifier is disjoint from every singleton argument just in case no point is in its own value.