The presuppositional superlative

x is the μ-est of C presupposes that x is a member of the comparison class and asserts that it measures above every other member. Von Fintel gives the superlative morpheme this entry, with the class a predicate like girl in her class, so that the presupposition rather than the assertion fails when the class shrinks below x; at a world it is Heim's absolute superlative Degree.AbsoluteSuperlative. The assertion is the set-standard comparative of x over the other members' degrees, so its anti-additivity in the class comes from Hoeksema's anti-additivity of the set comparative.

Main definitions

• Degree.superlative: the superlative as a trivalent proposition.

Main results

• Degree.superlative_assertion_iff: the assertion is the set-standard comparative over the other members of the class.
• Degree.isAntiAdditive_superlative_assertion: the assertion is anti-additive in the class.
• Degree.superlative_eq_one_iff_absoluteSuperlative: at a world the superlative is true exactly when x is the absolute superlative of the class there.

Implementation notes

The comparison class is given at each world, C : W → Set α, the transpose of von Fintel's world-dependent predicate. The degree measure μ does not vary with the world; von Fintel's ιd P(x)(d) measures at the world of evaluation.

References

• [vF99a]
• [Hei99]
• [Hoe83]

noncomputable def Degree.superlative {α : Type u_1} {D : Type u_2} {W : Type u_3} [Preorder D] (μ : α → D) (C : W → Set α) (x : α) : W → SignType

x is the μ-est of C presupposes that x is in the comparison class and asserts that it measures above every other member of the class ([vF99a]'s (79)).

Equations

• Degree.superlative μ C x = {w : W | x ∈ C w}.indicator fun (w : W) => SignType.ofProp (∀ y ∈ C w, y ≠ x → μ y < μ x)

@[simp]

theorem Degree.superlative_eq_zero_iff {α : Type u_1} {D : Type u_2} {W : Type u_3} [Preorder D] {μ : α → D} {C : W → Set α} {x : α} {w : W} : superlative μ C x w = 0 ↔ x ∉ C w

@[simp]

theorem Degree.superlative_eq_one_iff {α : Type u_1} {D : Type u_2} {W : Type u_3} [Preorder D] {μ : α → D} {C : W → Set α} {x : α} {w : W} : superlative μ C x w = 1 ↔ x ∈ C w ∧ ∀ y ∈ C w, y ≠ x → μ y < μ x

theorem Degree.superlative_assertion_iff {α : Type u_1} {D : Type u_2} [Preorder D] {μ : α → D} {x : α} {s : Set α} : (∀ y ∈ s, y ≠ x → μ y < μ x) ↔ x ∈ μ ⁻¹' strictUpperBounds (μ '' (s \ {x}))

The assertion is the set-standard comparative of x against the degrees of the other members of the class.

theorem Degree.isAntiAdditive_superlative_assertion {α : Type u_1} {D : Type u_2} {W : Type u_3} [Preorder D] (μ : α → D) (x : α) : NaturalLogic.IsAntiAdditive fun (C : W → Set α) (w : W) => ∀ y ∈ C w, y ≠ x → μ y < μ x

The assertion is anti-additive in the comparison class, by the anti-additivity of the set-standard comparative ([Hoe83]).

theorem Degree.superlative_eq_one_iff_absoluteSuperlative {α : Type u_1} {D : Type u_2} {W : Type u_3} [LinearOrder D] {μ : α → D} {C : W → Set α} {x : α} {w : W} : superlative μ C x w = 1 ↔ AbsoluteSuperlative μ (C w) x

At a world the superlative is true exactly when x is the absolute superlative of the class there ([Hei99]).