Beltrama (2025): Evaluation, thresholds, and practical commitments

Mildly positive adjectives, decent, acceptable, adequate, are context-sensitive and gradable like good yet crisp, barely-friendly and without a zone of indifference like the absolute adjectives, and they resist slightly, the diagnostic of a minimum standard ([Bel25], against [KMcN05]'s absolute class). Their positive form takes a necessity standard: the greatest degree of value the object has in every circumstantially accessible world in which it is pursued, the standard that enough supplies with an overt purpose ([Nad23a]) and a functional standard in [KA11]'s sense, so that [Ken07b]'s standard-fixing function must range over functional standards beside the endpoints and comparison-class norms of Interpretive Economy. The middling inference of decent is a scalar implicature against good, and the missing zone of indifference follows from the standard's existential force: an object is acceptable only if some accessible circumstance pursues it, and unacceptable only if none does.

Implementation notes

The necessity standard is the greatest lower bound of the object's values over the pursued accessible worlds, mathlib's IsGLB, which is the paper's maximum of the lower bounds; the value scale is any partial order, open above where a theorem needs it. Existential force is derived under the assumption that circumstantial alternatives leave the object's value fixed. The behaviour with barely, emphasis in downward-entailing contexts and -able derivation are recorded in the example rows only.

References

• [Bel25]
• [Ken07b]
• [KMcN05]
• [Nad23a]
• [KA11]

The necessity standard

def Beltrama2025.pursuedValues {W : Type u_1} {E : Type u_2} {D : Type u_3} (Acc : W → Set W) (pursued : E → W → Prop) (μ : E → W → D) (x : E) (w : W) : Set D

The values an object takes in the accessible worlds where it is pursued.

Equations

• Beltrama2025.pursuedValues Acc pursued μ x w = μ x '' {w' : W | w' ∈ Acc w ∧ pursued x w'}

def Beltrama2025.IsNecessityStandard {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] (Acc : W → Set W) (pursued : E → W → Prop) (μ : E → W → D) (x : E) (w : W) (s : D) : Prop

(64): the necessity standard is the greatest degree the object's value reaches in every accessible world where it is pursued, the greatest lower bound of pursuedValues.

Equations

• Beltrama2025.IsNecessityStandard Acc pursued μ x w s = IsGLB (Beltrama2025.pursuedValues Acc pursued μ x w) s

def Beltrama2025.Pos {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] (μ : E → W → D) (x : E) (w : W) (s : D) : Prop

(65): the positive form at a standard.

Equations

• Beltrama2025.Pos μ x w s = (s ≤ μ x w)

def Beltrama2025.Acceptable {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] (Acc : W → Set W) (pursued : E → W → Prop) (μ : E → W → D) (x : E) (w : W) : Prop

acceptable: the object meets a necessity standard.

Equations

• Beltrama2025.Acceptable Acc pursued μ x w = ∃ (s : D), Beltrama2025.IsNecessityStandard Acc pursued μ x w s ∧ Beltrama2025.Pos μ x w s

def Beltrama2025.Unacceptable {W : Type u_1} {E : Type u_2} (Acc : W → Set W) (pursued : E → W → Prop) (x : E) (w : W) : Prop

unacceptable, the negated form's universal force: no accessible world pursues the object.

Equations

• Beltrama2025.Unacceptable Acc pursued x w = ∀ w' ∈ Acc w, ¬pursued x w'

def Beltrama2025.PosMin {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] (μ : E → W → D) (x : E) (w : W) [OrderBot D] : Prop

The positive form of a minimum-standard adjective: any degree above the scale minimum.

Equations

• Beltrama2025.PosMin μ x w = (⊥ < μ x w)

def Beltrama2025.Middling {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] (μ : E → W → D) (x : E) (w : W) (s t : D) : Prop

The middling reading: decent, at the standard s, and not good, at the standard t.

Equations

• Beltrama2025.Middling μ x w s t = (Beltrama2025.Pos μ x w s ∧ ¬Beltrama2025.Pos μ x w t)

theorem Beltrama2025.pos_of_pursued {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {Acc : W → Set W} {pursued : E → W → Prop} {μ : E → W → D} {x : E} {w : W} {s : D} (hs : IsNecessityStandard Acc pursued μ x w s) (hw : w ∈ Acc w) (hp : pursued x w) : Pos μ x w s

An object pursued in the world of evaluation meets its own standard.

theorem Beltrama2025.exists_pursued {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {Acc : W → Set W} {pursued : E → W → Prop} {μ : E → W → D} {x : E} {w : W} {s : D} [NoMaxOrder D] (hs : IsNecessityStandard Acc pursued μ x w s) : ∃ w' ∈ Acc w, pursued x w'

Existential force: on a scale open above, a standard exists only if the object is pursued in some accessible world, since otherwise every degree is a lower bound.

theorem Beltrama2025.standard_antitone {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {Acc : W → Set W} {pursued : E → W → Prop} {μ : E → W → D} {x : E} {w : W} {s : D} {Acc' : W → Set W} {s' : D} (hs : IsNecessityStandard Acc pursued μ x w s) (hs' : IsNecessityStandard Acc' pursued μ x w s') (h : Acc w ⊆ Acc' w) : s' ≤ s

Context sensitivity: widening the circumstances, hence the pursued worlds, can only lower the standard.

Force and the zone of indifference

theorem Beltrama2025.acceptable_iff {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {Acc : W → Set W} {pursued : E → W → Prop} {μ : E → W → D} (x : E) (w : W) [NoMaxOrder D] (hμ : ∀ w' ∈ Acc w, μ x w' = μ x w) : Acceptable Acc pursued μ x w ↔ ∃ w' ∈ Acc w, pursued x w'

When circumstantial alternatives leave the object's value fixed, acceptable says exactly that some accessible world pursues it.

theorem Beltrama2025.neither_defective {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {Acc : W → Set W} {pursued : E → W → Prop} {μ : E → W → D} (x : E) (w : W) [NoMaxOrder D] (hμ : ∀ w' ∈ Acc w, μ x w' = μ x w) : ¬(¬Acceptable Acc pursued μ x w ∧ ¬Unacceptable Acc pursued x w)

"Neither acceptable nor unacceptable" is defective: the first conjunct denies that any accessible world pursues the object, the second that none does.

theorem Beltrama2025.good_gap {D : Type u_3} [PartialOrder D] (tp : Degree.ThresholdPair D) (h : tp.neg ≤ tp.pos) : tp.gap.Nonempty

good and bad on [Ken07b]'s two standards leave a zone of indifference between them, which the necessity standard's single point does not.

Against the minimum-standard analysis

theorem Beltrama2025.comparative_entails_posMin {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {μ : E → W → D} {x : E} {w : W} [OrderBot D] {y : E} (h : μ y w < μ x w) : PosMin μ x w

Under a minimum standard the comparative entails the positive form.

theorem Beltrama2025.comparative_not_entails_pos {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {μ : E → W → D} {x : E} {w : W} {s : D} {y : E} (h : μ y w < μ x w) (hs : μ x w < s) : μ y w < μ x w ∧ ¬Pos μ x w s

Under a necessity standard it does not ((51b)): an object can outvalue another and fall short of the standard.

theorem Beltrama2025.bot_lt_standard {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {Acc : W → Set W} {pursued : E → W → Prop} {μ : E → W → D} {x : E} {w : W} {s : D} [OrderBot D] (hs : IsLeast (pursuedValues Acc pursued μ x w) s) (h : ∀ v ∈ pursuedValues Acc pursued μ x w, ⊥ < v) : ⊥ < s

slightly diagnoses a standard at the scale minimum; an attained necessity standard lies above it whenever every pursued value does.

The middling inference

theorem Beltrama2025.pos_of_pos_of_le {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {μ : E → W → D} {x : E} {w : W} {s t : D} (h : s ≤ t) (ht : Pos μ x w t) : Pos μ x w s

With good's standard above the necessity standard, good entails decent, so decent implicates not good.

theorem Beltrama2025.middling_cancelable {W : Type u_1} {E : Type u_2} {D : Type u_3} [PartialOrder D] {μ : E → W → D} {x : E} {w : W} {s t : D} (h : s ≤ t) (ht : Pos μ x w t) : Pos μ x w s ∧ Pos μ x w t

The implicature is cancelable: meeting the higher standard is consistent with meeting the lower one, so decent, in fact good is consistent.

theorem Beltrama2025.not_pos_iff {W : Type u_1} {E : Type u_2} {D : Type u_3} [LinearOrder D] {μ : E → W → D} {x : E} {w : W} {s : D} : ¬Pos μ x w s ↔ μ x w < s

A single crisp point: below the standard the positive form fails outright.

theorem Beltrama2025.isNecessityStandard_iff {W : Type u_1} {E : Type u_2} {D : Type u_3} [CompleteLattice D] {Acc : W → Set W} {pursued : E → W → Prop} {μ : E → W → D} {x : E} {w : W} {s : D} : IsNecessityStandard Acc pursued μ x w s ↔ s = sSup {d : D | ∀ w' ∈ Acc w, pursued x w' → d ≤ μ x w'}

The paper's form of (64): on a complete scale the standard is the maximum of the degrees below the object's value in every pursued accessible world.