Background orderings and threshold properties

In the states-based analysis of gradable predicates of Cariani, Santorio and Wellwood, which builds on Wellwood's comparative and which the same authors apply to confidence reports, a gradable predicate contributes two things: a background ordering of states, the states of having some heat for hot, and in each context a threshold property, the states that count as hot. The positive form says that the subject holds a state with the threshold property. The comparative bypasses the threshold: an admissible measure of one of the subject's states exceeds the greatest degree of the standard's. No covert positive morpheme is needed, and neither form entails the other.

The background is a preorder S and a threshold property is an upper set T of it, the monotonicity postulate of the analysis. A map ρ : S → X sends each state to its holder, or to its theme, so the positive form of x is x ∈ ρ '' T, and the comparative of a over b is Degree.MaxComparative .gt (ρ · = a) (ρ · = b) μ for an admissible measure μ. This file adds no definitions. It records how the two components interact: the one inference from a comparative to a positive form, upward monotonicity, holds on a total background and on no other.

Read as extensions, the threshold properties form a monotone delineation exactly when the background is total, the parallel the authors draw with Klein's consistency postulate, and the thresholds are degree thresholds pulled back along the measure exactly when the measure reflects the background.

Main statements

• mem_image_of_maxComparative: if b has the property and a has more of it than b, then a has the property, given an admissible measure and a total background.
• maxComparative_and_not_mem_image: the comparative does not entail the positive form.
• isMonotoneOn_upperSets_iff: the thresholds form a monotone delineation iff the background is total.
• forall_isUpperSet_exists_preimage_iff: the thresholds are pulled-back degree thresholds iff the measure reflects the background.

References

• [CSW23]
• [CSW24]
• [Wel15]
• [Kle80]

Upward monotonicity

theorem Degree.mem_image_of_maxComparative {S : Type u_1} {X : Type u_2} {D : Type u_3} [Preorder S] [Preorder D] {ρ : S → X} {μ : S → D} {T : Set S} [Std.Total fun (x1 x2 : S) => x1 ≤ x2] (hT : IsUpperSet T) (hμ : StrictMono μ) {a b : X} (hb : b ∈ ρ '' T) (h : MaxComparative Comparison.gt (fun (x : S) => ρ x = a) (fun (x : S) => ρ x = b) μ) : a ∈ ρ '' T

If b has the property and a has more of it than b, then a has the property. The comparative supplies a state of a's measuring above a state of b's with the property, an admissible measure on a total background places it above that state, and the threshold is upward closed.

theorem Degree.not_mem_image_Ici_of_not_le {S : Type u_1} {X : Type u_2} {D : Type u_3} [Preorder S] [Preorder D] {ρ : S → X} {μ : S → D} {s t : S} (hst : ¬s ≤ t) (hlt : μ s < μ t) (hs : ∀ (u : S), ρ u = ρ s → u = s) (ht : ∀ (u : S), ρ u = ρ t → u = t) : ρ s ∈ ρ '' Set.Ici s ∧ MaxComparative Comparison.gt (fun (x : S) => ρ x = ρ t) (fun (x : S) => ρ x = ρ s) μ ∧ ρ t ∉ ρ '' Set.Ici s

Without totality upward monotonicity fails. When s and t are the only states of their holders, s is not below t but measures below it, and the property is the one of lying above s, the holder of s has the property and the holder of t has more of it without having it.

The comparative and the positive form

theorem Degree.maxComparative_and_not_mem_image {S : Type u_1} {X : Type u_2} {D : Type u_3} [Preorder D] {ρ : S → X} {μ : S → D} {T : Set S} {s t : S} (hlt : μ t < μ s) (hsT : s ∉ T) (hs : ∀ (u : S), ρ u = ρ s → u = s) (ht : ∀ (u : S), ρ u = ρ t → u = t) : MaxComparative Comparison.gt (fun (x : S) => ρ x = ρ s) (fun (x : S) => ρ x = ρ t) μ ∧ ρ s ∉ ρ '' T

The comparative does not entail the positive form. When s and t are the only states of their holders and s measures above t without the property, the holder of s has more of it than the holder of t without having it.

Delineations and degree thresholds

theorem Degree.isMonotoneOn_upperSets_iff {S : Type u_1} [Preorder S] : { toFun := id }.IsMonotoneOn {C : Set S | IsUpperSet C} ↔ ∀ (s t : S), s ≤ t ∨ t ≤ s

The upper sets of a background, as extensions, form a monotone delineation iff the background is total. Two incomparable states give the cycle of a nonlinear delineation.

theorem Degree.exists_isUpperSet_of_maxComparative {S : Type u_1} {X : Type u_2} {D : Type u_3} [Preorder S] [Preorder D] {ρ : S → X} {μ : S → D} (hm : Monotone μ) {a b : X} (h : MaxComparative Comparison.gt (fun (x : S) => ρ x = a) (fun (x : S) => ρ x = b) μ) : ∃ (T : Set S), IsUpperSet T ∧ a ∈ ρ '' T ∧ b ∉ ρ '' T

With a monotone measure, if a has more than b then some threshold property holds of a and not of b.

theorem Degree.maxComparative_of_exists_isUpperSet {S : Type u_1} {X : Type u_2} {D : Type u_3} [Preorder S] [Preorder D] {ρ : S → X} {μ : S → D} [Std.Total fun (x1 x2 : S) => x1 ≤ x2] (hμ : StrictMono μ) {a b : X} (hb : ∃ (δ : D), IsGreatest (μ '' {s : S | ρ s = b}) δ) (h : ∃ (T : Set S), IsUpperSet T ∧ a ∈ ρ '' T ∧ b ∉ ρ '' T) : MaxComparative Comparison.gt (fun (x : S) => ρ x = a) (fun (x : S) => ρ x = b) μ

On a total background with an admissible measure a separating threshold yields the comparative, when the degrees of b's states have a greatest element.

theorem Degree.maxComparative_iff_exists_isUpperSet {S : Type u_1} {X : Type u_2} {D : Type u_3} [Preorder S] [Preorder D] {ρ : S → X} {μ : S → D} [Std.Total fun (x1 x2 : S) => x1 ≤ x2] (hμ : StrictMono μ) (hm : Monotone μ) {a b : X} (hb : ∃ (δ : D), IsGreatest (μ '' {s : S | ρ s = b}) δ) : MaxComparative Comparison.gt (fun (x : S) => ρ x = a) (fun (x : S) => ρ x = b) μ ↔ ∃ (T : Set S), IsUpperSet T ∧ a ∈ ρ '' T ∧ b ∉ ρ '' T

On a total background with a monotone admissible measure, a has more than b iff some threshold property holds of a and not of b, as in Klein's comparative.

theorem Degree.forall_isUpperSet_exists_preimage_iff {S : Type u_1} {D : Type u_3} [Preorder S] [Preorder D] {μ : S → D} : (∀ (T : Set S), IsUpperSet T → ∃ (U : Set D), IsUpperSet U ∧ T = μ ⁻¹' U) ↔ ∀ (a b : S), μ a ≤ μ b → a ≤ b

Every threshold property of the background is a degree threshold pulled back along the measure iff the measure reflects the background.

theorem Degree.total_of_reflect_le {S : Type u_1} [Preorder S] {D : Type u_4} [LinearOrder D] {μ : S → D} (h : ∀ (a b : S), μ a ≤ μ b → a ≤ b) (s t : S) : s ≤ t ∨ t ≤ s

A measure into a linear scale that reflects the background makes it total.

theorem Degree.exists_isUpperSet_forall_ne_preimage {S : Type u_1} [Preorder S] {D : Type u_4} [LinearOrder D] (μ : S → D) {s t : S} (hst : ¬s ≤ t) (hts : ¬t ≤ s) : ∃ (T : Set S), IsUpperSet T ∧ ∀ (U : Set D), IsUpperSet U → T ≠ μ ⁻¹' U

On a non-total background some threshold property is no degree threshold pulled back along any measure into a linear scale.

theorem Degree.preimage_Ici_apply_eq_Ici {S : Type u_1} {D : Type u_3} [Preorder S] [Preorder D] {μ : S → D} (h : ∀ (a b : S), μ a ≤ μ b → a ≤ b) (hm : Monotone μ) (c : S) : μ ⁻¹' Set.Ici (μ c) = Set.Ici c

When the measure reflects the background and respects ties, the threshold above a contrast state c is the degree-threshold positive form at the degree of c.