Dinis and Jacinto (2026): Marginality scales for gradable adjectives

This file formalizes [dinis-jacinto-2026]'s marginality scales account of vague gradable adjectives. ML theory, the theory of marginal and large differences of [dinis-jacinto-2025], is simplified to a strict linear order with one primitive, marginally smaller than: largely smaller than is smaller but not marginally so, Definition 2.1, and five axioms remain, Figure 1, from which marginal smallness is transitive and bounded, Theorem 2.2, at most marginal difference is an equivalence relation and large difference is not transitive, Definition 2.3 and fn. 9. The representative model of the representation theorem is the lexicographic product of the rationals and the integers, a difference in the second coordinate alone being marginal, Definition 3.1. The account then takes over [fara-2000]'s interest-relative semantics after [Ken99]: a gradable adjective denotes a scale with a measure function from circumstances of evaluation and objects to degrees, the comparative compares degrees, and the positive form holds of an object whose degree is significantly, that is largely, greater than the standard of comparison, §5.1, on scales that satisfy ML, §5.2. Three consequences follow. An object that was in the positive form's extension and no longer is was greater on the scale, the case of Charles III of §5.4, which a two-scale account that reads the comparative off precise degrees cannot deliver. Objects at most marginally different are alike with respect to the positive form, [fara-2000]'s similarity constraint, so that a chain of marginal steps preserves the positive form and a Soritical sequence must contain a step that is not marginal, §6.1. And the clustering of the degrees of the objects in a vague predicate's extension implies tolerance, §3, and holds of the positive form.

Implementation notes

The strict order R is the < of a LinearOrder, whose axioms are the order conditions (1) to (4). Figure 1 is an image; Axioms 3 to 5 are stated as the text glosses them, with largely smaller than unfolded. The measure function's circumstances and objects are type parameters, and the Kaplanian context enters only through the standard of comparison and the agent-relative marginality relation, which are held fixed. The representation and uniqueness theorems of [dinis-jacinto-2025] are not formalized; the representative model is shown to satisfy ML and to carry the examples of §5.2 and fn. 9.

References

• [dinis-jacinto-2026]
• [dinis-jacinto-2025]
• [fara-2000]
• [Ken99]
• [kennedy-2007]

ML theory, §2

structure DinisJacinto2026.MLScale (α : Type u_2) [LinearOrder α] : Type u_2

ML theory, Figure 1: a linear order with a primitive marginally smaller than relation M, largely smaller than being x < y ∧ ¬ M x y.

• M : α → α → Prop

  x is marginally smaller than y.

• exists_large : ∃ (x : α), ∃ (y : α), x < y ∧ ¬self.M x y

  Axiom 1: some element is largely smaller than another.

• lt_of_m (x y : α) : self.M x y → x < y

  Axiom 2: marginally smaller than implies smaller than.

• irrelevance (x y z : α) : self.M x y → (z < y ∧ ¬self.M z y → z < x ∧ ¬self.M z x) ∧ (x < z ∧ ¬self.M x z → y < z ∧ ¬self.M y z)

  Axiom 3, M-irrelevance: when x is marginally smaller than y, whatever is largely smaller than y is largely smaller than x, and y is largely smaller than whatever x is largely smaller than.

• extends_lt (x y z : α) : x < y → (y < z ∧ ¬self.M y z → x < z ∧ ¬self.M x z) ∧ (z < x ∧ ¬self.M z x → z < y ∧ ¬self.M z y)

  Axiom 4: largely smaller than extends along smaller than: whatever is smaller than something largely smaller than z is largely smaller than z, and whatever is largely smaller than something smaller than z is largely smaller than z.

• decomposition (x y : α) : x < y ∧ ¬self.M x y → (∃ (z : α), self.M x z ∧ z < y ∧ ¬self.M z y) ∧ ∃ (w : α), self.M w y ∧ x < w ∧ ¬self.M x w

  Axiom 5, decomposition: a large difference is a marginal step followed by a large one, and a large one followed by a marginal step.

def DinisJacinto2026.MLScale.L {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y : α) : Prop

Largely smaller than, Definition 2.1.

Equations

• ml.L x y = (x < y ∧ ¬ml.M x y)

def DinisJacinto2026.MLScale.MarginalDiff {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y : α) : Prop

Marginal difference, Definition 2.3.

Equations

• ml.MarginalDiff x y = (ml.M x y ∨ ml.M y x)

def DinisJacinto2026.MLScale.AtMostMarginal {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y : α) : Prop

At most marginal difference, Definition 2.3: sameness for present purposes.

Equations

• ml.AtMostMarginal x y = (x = y ∨ ml.MarginalDiff x y)

def DinisJacinto2026.MLScale.LargeDiff {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y : α) : Prop

Large difference, Definition 2.3.

Equations

• ml.LargeDiff x y = (ml.L x y ∨ ml.L y x)

theorem DinisJacinto2026.MLScale.M.lt {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y : α} (h : ml.M x y) : x < y

theorem DinisJacinto2026.MLScale.L.lt {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y : α} (h : ml.L x y) : x < y

theorem DinisJacinto2026.MLScale.M.not_l {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y : α} (h : ml.M x y) : ¬ml.L x y

theorem DinisJacinto2026.MLScale.l_of_lt_of_not_m {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y : α} (hlt : x < y) (h : ¬ml.M x y) : ml.L x y

theorem DinisJacinto2026.MLScale.L.of_lt_of_l {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y z : α} (hxy : x < y) (h : ml.L y z) : ml.L x z

Axiom 4, first half.

theorem DinisJacinto2026.MLScale.L.trans_lt {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y z : α} (h : ml.L x y) (hyz : y < z) : ml.L x z

Axiom 4, second half.

theorem DinisJacinto2026.MLScale.M.trans {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y z : α} (hxy : ml.M x y) (hyz : ml.M y z) : ml.M x z

Theorem 2.2, M-transitivity: marginal steps do not accrue to a large difference.

theorem DinisJacinto2026.MLScale.M.bounded {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y z : α} (hxz : ml.M x z) (hxy : x < y) (hyz : y < z) : ml.M x y ∧ ml.M y z

Theorem 2.2, M-boundedness: what lies between marginally different elements is marginally different from each.

theorem DinisJacinto2026.MLScale.marginalDiff_irrefl {α : Type u_1} [LinearOrder α] {ml : MLScale α} (x : α) : ¬ml.MarginalDiff x x

theorem DinisJacinto2026.MLScale.MarginalDiff.symm {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y : α} (h : ml.MarginalDiff x y) : ml.MarginalDiff y x

theorem DinisJacinto2026.MLScale.largeDiff_irrefl {α : Type u_1} [LinearOrder α] {ml : MLScale α} (x : α) : ¬ml.LargeDiff x x

theorem DinisJacinto2026.MLScale.LargeDiff.symm {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y : α} (h : ml.LargeDiff x y) : ml.LargeDiff y x

theorem DinisJacinto2026.MLScale.AtMostMarginal.refl {α : Type u_1} [LinearOrder α] {ml : MLScale α} (x : α) : ml.AtMostMarginal x x

theorem DinisJacinto2026.MLScale.AtMostMarginal.symm {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y : α} (h : ml.AtMostMarginal x y) : ml.AtMostMarginal y x

theorem DinisJacinto2026.MLScale.AtMostMarginal.trans {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y z : α} (hxy : ml.AtMostMarginal x y) (hyz : ml.AtMostMarginal y z) : ml.AtMostMarginal x z

At most marginal difference is transitive, by M-transitivity when the steps agree in direction and by M-boundedness when they do not.

def DinisJacinto2026.MLScale.atMostMarginalSetoid {α : Type u_1} [LinearOrder α] {ml : MLScale α} : Setoid α

Sameness for present purposes, Definition 2.3, as an equivalence relation.

Equations

• DinisJacinto2026.MLScale.atMostMarginalSetoid = { r := ml.AtMostMarginal, iseqv := ⋯ }

The similarity constraint, §6.1

theorem DinisJacinto2026.MLScale.l_iff_of_m {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y z : α} (hxy : ml.M x y) : ml.L z x ↔ ml.L z y

Marginally different degrees are alike with respect to being largely greater than a standard: the second half is M-irrelevance and the first M-boundedness.

theorem DinisJacinto2026.MLScale.l_iff_of_atMostMarginal {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y z : α} (h : ml.AtMostMarginal x y) : ml.L z x ↔ ml.L z y

Fara's similarity constraint on degrees: at most marginally different degrees are alike with respect to being largely greater than a standard.

theorem DinisJacinto2026.MLScale.l_iff_of_reflTransGen {α : Type u_1} [LinearOrder α] {ml : MLScale α} {x y z : α} (h : Relation.ReflTransGen ml.M x y) : ml.L z x ↔ ml.L z y

M-chains: however many marginal steps separate two degrees, they are alike with respect to being largely greater than a standard.

The representative model, Definition 3.1

def DinisJacinto2026.MLScale.repM (x y : Lex (ℚ × ℤ)) : Prop

Marginally smaller in the representative model: the same first coordinate and a smaller second one.

Equations

• DinisJacinto2026.MLScale.repM x y = ((ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 < (ofLex y).2)

theorem DinisJacinto2026.MLScale.lt_and_not_repM_iff {x y : Lex (ℚ × ℤ)} : x < y ∧ ¬repM x y ↔ (ofLex x).1 < (ofLex y).1

Largely smaller in the representative model is a smaller first coordinate.

theorem DinisJacinto2026.MLScale.fst_le_of_lt {x y : Lex (ℚ × ℤ)} (h : x < y) : (ofLex x).1 ≤ (ofLex y).1

def DinisJacinto2026.MLScale.rep : MLScale (Lex (ℚ × ℤ))

The representative model R*, Definition 3.1: rational-integer pairs in lexicographic order, marginally smaller when the first coordinates agree.

Equations

• One or more equations did not get rendered due to their size.

theorem DinisJacinto2026.MLScale.rep_l_iff {x y : Lex (ℚ × ℤ)} : rep.L x y ↔ (ofLex x).1 < (ofLex y).1

theorem DinisJacinto2026.MLScale.largeDiff_not_trans : rep.LargeDiff (toLex (0, 0)) (toLex (1, 0)) ∧ rep.LargeDiff (toLex (1, 0)) (toLex (0, 1)) ∧ ¬rep.LargeDiff (toLex (0, 0)) (toLex (0, 1))

Large difference is not transitive, fn. 9: in Figure 2, m and n differ marginally though each differs largely from p.

The marginality scales account, §5

def DinisJacinto2026.MLScale.er {α : Type u_1} [LinearOrder α] {C : Type u_2} {O : Type u_3} (μ : C → O → α) (u : C) (x : O) (v : C) (y : O) : Prop

The comparative, §5.1: y at circumstance v is smaller on the scale than x at u.

Equations

• DinisJacinto2026.MLScale.er μ u x v y = (μ v y < μ u x)

def DinisJacinto2026.MLScale.pos {α : Type u_1} [LinearOrder α] (ml : MLScale α) {C : Type u_2} {O : Type u_3} (μ : C → O → α) (norm : α) (w : C) (x : O) : Prop

The positive form, §5.1, after Fara: the standard of comparison is significantly, that is largely, smaller than the object's degree at the circumstance.

Equations

• ml.pos μ norm w x = ml.L norm (μ w x)

theorem DinisJacinto2026.MLScale.pos.lt {α : Type u_1} [LinearOrder α] {ml : MLScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {a : O} (h : ml.pos μ norm w a) : norm < μ w a

The positive form entails exceeding the standard.

theorem DinisJacinto2026.MLScale.not_pos_of_m {α : Type u_1} [LinearOrder α] {ml : MLScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {a : O} (h : ml.M norm (μ w a)) : ¬ml.pos μ norm w a

Figure 5: an object whose degree exceeds the standard only marginally is not in the positive form's extension.

theorem DinisJacinto2026.MLScale.er_of_pos_of_not_pos {α : Type u_1} [LinearOrder α] {ml : MLScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {u v : C} {a : O} (h₁ : ml.pos μ norm u a) (h₂ : ¬ml.pos μ norm v a) : er μ u a v a

Charles III, §5.4: an object in the positive form's extension at one circumstance and out of it at another was greater on the scale, since the scale relations do not vary with the circumstance; a two-scale account that reads the comparative off unchanged precise degrees cannot say so.

theorem DinisJacinto2026.MLScale.tolerance {α : Type u_1} [LinearOrder α] {ml : MLScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {a b : O} : (¬ml.pos μ norm w a → ml.M (μ w a) (μ w b) → ¬ml.pos μ norm w b) ∧ (ml.pos μ norm w a → ml.M (μ w b) (μ w a) → ml.pos μ norm w b)

Tolerance, §3: an object out of the positive form's extension keeps out anything whose degree is marginally greater, and one in it keeps in anything whose degree is marginally smaller.

theorem DinisJacinto2026.MLScale.not_reflTransGen_of_pos {α : Type u_1} [LinearOrder α] {ml : MLScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {a b : O} (h₁ : ¬ml.pos μ norm w a) (h₂ : ml.pos μ norm w b) : ¬Relation.ReflTransGen ml.M (μ w a) (μ w b)

A Soritical sequence for the positive form is no chain of marginal steps: some adjacent pair differs largely, the nonstandard primitivist solution to the Sorites of §3 and §6.1.

def DinisJacinto2026.MLScale.Clustered {α : Type u_1} [LinearOrder α] {ml : MLScale α} {O : Type u_3} (B : O → Prop) (δ : O → α) : Prop

Clustered degrees, §3: something has the property iff its degree differs at most marginally from the degree of something with the property.

Equations

• DinisJacinto2026.MLScale.Clustered B δ = ∀ (x : O), B x ↔ ∃ (y : O), B y ∧ ml.AtMostMarginal (δ y) (δ x)

theorem DinisJacinto2026.MLScale.Clustered.tolerance {α : Type u_1} [LinearOrder α] {ml : MLScale α} {O : Type u_3} {a b : O} {B : O → Prop} {δ : O → α} (h : Clustered B δ) : (¬B a → ml.M (δ a) (δ b) → ¬B b) ∧ (B a → ml.M (δ b) (δ a) → B b)

Clustered degrees imply degree tolerance, §3.

theorem DinisJacinto2026.MLScale.clustered_pos {α : Type u_1} [LinearOrder α] {ml : MLScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} : Clustered (ml.pos μ norm w) (μ w)

The positive form's extension is clustered: the marginality scales account implies the nonstandard primitivist principle of §3.

Ronaldo and Zidane, §5.2

theorem DinisJacinto2026.MLScale.zidane_ronaldo : er (fun (x : Unit) => id) () (toLex (1, 2)) () (toLex (0, 10)) ∧ rep.pos (fun (x : Unit) => id) (toLex (0, 0)) () (toLex (1, 2)) ∧ ¬rep.pos (fun (x : Unit) => id) (toLex (0, 0)) () (toLex (0, 10))

The example of §5.2 in the representative model: with the standard at ⟨0, 0⟩, Zidane at ⟨1, 2⟩ is balder than Ronaldo at ⟨0, 10⟩, and Zidane is bald where Ronaldo, though balder than the standard, is not.