Clausal comparatives: set and max standards

[Hoe83] [vS84] [Rul95] [Hei01]

Comparison against a than-clause denotation rather than a point: the set-of-degrees S-comparative (Comparison.gt.overSet μ directly), the max-quantified reading (thanDegrees/maxComparative/maxEquative, IsGreatest-based), and downward-entailingness of than-clauses. The point-standard collapse (overSet_singleton, maxComparative_eq_iff) makes the binary comparativeSem the atomic special case.

Set-of-degrees comparative

The S-comparative ([Hoe83] §3.8 Def 7) generalizes comparativeSem from a single standard to an arbitrary degree-set standard. It is Comparison.gt.overSet μ (μ ⁻¹' strictUpperBounds Δ) — the strict-> set-standard predication of Core.Order.Comparison — not a separate definition; the binary comparator is its singleton case (Comparison.overSet_singleton). The properties below are stated about Comparison.gt.overSet μ directly. Needs only [Preorder D].

theorem Degree.mem_gtOverSet_iff_subset_Iio {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (Δ : Set D) (y : Entity) : y ∈ Core.Order.Comparison.gt.overSet μ Δ ↔ Δ ⊆ Set.Iio (μ y)

The set-of-degrees comparative Comparison.gt.overSet μ ([Hoe83]) as a strict-interval inclusion: y clears the than-clause iff every standard degree lies strictly below μ y. Strict mirror of mathlib's mem_upperBounds_iff_subset_Iic; both faces are Iff.rfl siblings.

theorem Degree.gtOverSet_isAntiAdditive {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) : Entailment.IsAntiAdditive (Core.Order.Comparison.gt.overSet μ)

[Hoe83] Fact 4: the S-comparative Comparison.gt.overSet μ is anti-additive in its set-of-degrees argument — the algebraic source of NPI licensing in clausal than-comparatives.

theorem Degree.gtOverSet_eq_singleton_of_isGreatest {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) {Δ : Set D} {m : D} (hm : IsGreatest Δ m) : Core.Order.Comparison.gt.overSet μ Δ = Core.Order.Comparison.gt.overSet μ {m}

Reduction lemma ([BP04] §3, order-theoretic form): the S-comparative Comparison.gt.overSet μ is determined by the greatest element of its degree-set argument. Needs neither linearity nor density — only [Preorder D] and the IsGreatest witness.

Max-quantified comparative

[vS84] [Rul95]

The clausal comparative: some matrix witness measures strictly above the maximum of the than-clause degree set. Matrix and than restrictions are independent predicates over an arbitrary witness sort, so heterogeneous comparatives are the general case. Shared by Studies/Wellwood2015, Studies/Pasternak2019, and Semantics/Attitudes/Confidence.

def Degree.thanDegrees {α : Type u_1} {D : Type u_2} [Preorder D] (Pthan : α → Prop) (μ : α → D) : Set D

The than-clause degree set: degrees reached by some Pthan-witness. Generalizes the phrasal principal-downset standard (thanDegrees_singleton) to clausal standards with arbitrary witness predicates.

Equations

• Degree.thanDegrees Pthan μ = {d : D | ∃ (x : α), Pthan x ∧ d ≤ μ x}

theorem Degree.thanDegrees_singleton {α : Type u_1} {D : Type u_2} [Preorder D] (μ : α → D) (b : α) : thanDegrees (fun (x : α) => x = b) μ = Set.Iic (μ b)

A unique standard collapses the than-clause degree set to the principal downset of its measure — the phrasal standard (ThanClause.thanClauseDenotation).

def Degree.maxComparative {α : Type u_1} {D : Type u_2} [Preorder D] (Pmatrix Pthan : α → Prop) (μ : α → D) : Prop

The max-quantified comparative: the Pthan degree set has a greatest element δ, and some Pmatrix-witness measures strictly above δ.

Equations

• Degree.maxComparative Pmatrix Pthan μ = ∃ (δ : D), IsGreatest (Degree.thanDegrees Pthan μ) δ ∧ ∃ (x : α), Pmatrix x ∧ δ < μ x

theorem Degree.isGreatest_thanDegrees_of_unique {α : Type u_1} {D : Type u_2} [Preorder D] {Pthan : α → Prop} {μ : α → D} {xb : α} (hb : Pthan xb) (hb_unique : ∀ (x : α), Pthan x → x = xb) : IsGreatest (thanDegrees Pthan μ) (μ xb)

A unique Pthan-witness makes its measure the greatest than-clause degree.

theorem Degree.maxComparative_unique {α : Type u_1} {D : Type u_2} [Preorder D] {Pmatrix Pthan : α → Prop} {μ : α → D} {xa xb : α} (ha : Pmatrix xa) (ha_unique : ∀ (x : α), Pmatrix x → x = xa) (hb : Pthan xb) (hb_unique : ∀ (x : α), Pthan x → x = xb) : maxComparative Pmatrix Pthan μ ↔ μ xb < μ xa

Under unique matrix and than witnesses, the max-quantified comparative reduces to direct measure comparison.

def Degree.maxEquative {α : Type u_1} {D : Type u_2} [Preorder D] (Pmatrix Pthan : α → Prop) (μ : α → D) : Prop

Max-quantified equative: the Pthan degree set has a greatest element δ, and some Pmatrix-witness measures at least δ — maxComparative with the weak threshold.

Equations

• Degree.maxEquative Pmatrix Pthan μ = ∃ (δ : D), IsGreatest (Degree.thanDegrees Pthan μ) δ ∧ ∃ (x : α), Pmatrix x ∧ δ ≤ μ x

theorem Degree.maxComparative_entails_maxEquative {α : Type u_1} {D : Type u_2} [Preorder D] (Pmatrix Pthan : α → Prop) (μ : α → D) : maxComparative Pmatrix Pthan μ → maxEquative Pmatrix Pthan μ

The strict comparative entails the equative.

theorem Degree.maxComparative_eq_iff {α : Type u_1} {D : Type u_2} [Preorder D] (μ : α → D) (xa xb : α) : maxComparative (fun (x : α) => x = xa) (fun (x : α) => x = xb) μ ↔ μ xb < μ xa

Singleton collapse: comparing unique individuals is direct measure comparison.

theorem Degree.maxComparative_iff_gtOverSet {α : Type u_1} {D : Type u_2} [Preorder D] (Pmatrix Pthan : α → Prop) (μ : α → D) : maxComparative Pmatrix Pthan μ ↔ (∃ (δ : D), IsGreatest (thanDegrees Pthan μ) δ) ∧ ∃ (x : α), Pmatrix x ∧ x ∈ Core.Order.Comparison.gt.overSet μ (thanDegrees Pthan μ)

Grounding in the S-comparative: when the than-clause degree set has a maximum, a matrix witness clears it iff it clears the whole set (Comparison.gt.overSet, via gtOverSet_eq_singleton_of_isGreatest).

Downward-entailingness of than-clauses

theorem Degree.comparative_than_DE {α : Type u_1} (R : α → α → Prop) (μ_a : α) (D₁ D₂ : Set α) (h_sub : D₁ ⊆ D₂) (h : ∀ d ∈ D₂, R μ_a d) (d : α) : d ∈ D₁ → R μ_a d

Universal quantification over a domain is antitone in the domain — the generic monotonicity fact behind than-clauses being downward-entailing (not [Hoe83]'s specific anti-additivity result, which is in Studies/Hoeksema1983.lean).

Superlatives

[Hei99] [Sza86] [Bob12]

-est universally quantifies the comparative over a comparison class ([Hei99]; the semantic reflex of [Bob12]'s containment [[[ADJ] CMPR] SPRL]): absolute readings fix the class extensionally, relative readings via focus alternatives.

def Degree.absoluteSuperlative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (C : Set Entity) (x : Entity) : Prop

Absolute superlative: x is the G-est entity in comparison class C — x beats every other member on the comparative.

Equations

• Degree.absoluteSuperlative μ C x = (x ∈ C ∧ ∀ y ∈ C, y ≠ x → Degree.comparativeSem μ x y Core.Order.ScalePolarity.positive)

def Degree.relativeSuperlative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] {Alt : Type u_3} (μ : Entity → D) (f : Alt → Entity) (focusedAlt : Alt) (alternatives : Set Alt) : Prop

Relative superlative ([Hei99]): the focused alternative's entity outranks every other alternative's under f.

Equations

• Degree.relativeSuperlative μ f focusedAlt alternatives = ∀ a ∈ alternatives, a ≠ focusedAlt → Degree.comparativeSem μ (f focusedAlt) (f a) Core.Order.ScalePolarity.positive

theorem Degree.absolute_unique {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (C : Set Entity) (x y : Entity) (hx : absoluteSuperlative μ C x) (hy : absoluteSuperlative μ C y) : x = y

At most one entity satisfies the absolute superlative.

theorem Degree.absoluteSuperlative_isGreatest {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (C : Set Entity) (x : Entity) (h : absoluteSuperlative μ C x) : IsGreatest (μ '' C) (μ x)

The absolute superlative makes μ x the greatest element of the degree image μ '' C; the converse fails (ties).