Dinis and Jacinto (2026): Marginality Scales for Gradable Adjectives

Dinis and Jacinto give the degrees of a vague gradable adjective the structure of their theory of marginal and large differences, ML theory, simplified to a linear order with one primitive, marginally smaller than. A degree is largely smaller than another when it is smaller but not marginally so. As in Kennedy's semantics, an adjective measures objects at circumstances of evaluation by degrees, and the comparative compares degrees; as in Fara's, the positive form holds of an object whose degree is largely greater than the standard of comparison. The positive form then cannot tell apart degrees that differ at most marginally, so its extension is clustered and tolerant, a Soritical sequence must contain a large step, and an object that leaves the extension must have become smaller on the scale.

Main statements

• marginalScaleEquiv: along a linear order, the five axioms with largely smaller than defined are the eleven of the 2025 paper.
• comparative_of_positive_of_not_positive: an object that leaves the positive form's extension has become smaller on the scale, which the two-scale alternative does not predict.
• clustered_positive: at most marginally different degrees are alike for the positive form, so its extension is clustered and tolerant.
• exists_large_step_of_soritical: a Soritical sequence for the positive form crosses into the extension at a large step.

Implementation notes

• ML scales are Degree.MarginalScale, whose five axioms are those of Figure 1 with largely smaller than unfolded.
• A measure function takes a circumstance of evaluation and an object to a degree. The context enters only through the standard of comparison and the scale, which are held fixed.
• The text calls marginal difference transitive and large difference possibly intransitive (p. 106). Marginally smaller than and at most marginal difference are transitive, while marginal difference, being symmetric and irreflexive, is not, and large difference never is.

References

• [DJ26]
• [DJ25]
• [Gra00]
• [Ken99]
• [Ken07b]

Marginal and large difference

theorem DinisJacinto2026.not_isTrans_symmGen_marginallyLT {α : Type u_1} [LinearOrder α] (ml : Degree.MarginalScale α) : ¬IsTrans α (Relation.SymmGen ml.MarginallyLT)

Marginal difference is not transitive, since it is symmetric and irreflexive and Decomposition makes some degree marginally smaller than another.

theorem DinisJacinto2026.not_isTrans_symmGen_largelyLT {α : Type u_1} [LinearOrder α] (ml : Degree.MarginalScale α) : ¬IsTrans α (Relation.SymmGen ml.LargelyLT)

Large difference is never transitive, strengthening the counterexample of fn. 9. By Decomposition, a degree marginally above x and largely below y differs largely from y, as x does, but not from x.

The simplified theory

theorem DinisJacinto2026.isMLModel {α : Type u_1} [LinearOrder α] (ml : Degree.MarginalScale α) : DinisJacinto2025.IsMLModel (fun (x1 x2 : α) => x1 < x2) ml.MarginallyLT ml.LargelyLT

An ML scale satisfies the eleven axioms of [DJ25], Theorem 2.2 among them.

def DinisJacinto2026.marginalScaleEquiv {α : Type u_1} [LinearOrder α] : Degree.MarginalScale α ≃ { p : (α → α → Prop) × (α → α → Prop) // DinisJacinto2025.IsMLModel (fun (x1 x2 : α) => x1 < x2) p.1 p.2 }

Along a linear order, the five axioms are the eleven of [DJ25], with largely smaller than defined as smaller than but not marginally smaller than (§2).

Equations

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

The marginality scales account

def DinisJacinto2026.Comparative {α : 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 holds when the object x at circumstance u is greater on the scale than the object y at circumstance v.

Equations

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

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

The positive form, after Fara, holds when the standard of comparison is largely smaller than the object's degree at the circumstance.

Equations

• DinisJacinto2026.Positive ml μ norm w x = ml.LargelyLT norm (μ w x)

theorem DinisJacinto2026.setOf_positive_subset_gt_over {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} : {x : O | Positive ml μ norm w x} ⊆ μ w ⁻¹' Set.Ioi norm

An object in the positive form's extension exceeds the standard of comparison.

theorem DinisJacinto2026.not_positive_of_marginallyLT {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {a : O} (h : ml.MarginallyLT norm (μ w a)) : ¬Positive ml μ norm w a

An object whose degree exceeds the standard only marginally is not in the positive form's extension (Figure 5).

theorem DinisJacinto2026.comparative_of_positive_of_not_positive {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {u v : C} {a : O} (h₁ : Positive ml μ norm u a) (h₂ : ¬Positive ml μ norm v a) : Comparative μ u a v a

An object in the positive form's extension at one circumstance and out of it at another is greater on the scale at the first, the case of Charles III (§5.4).

theorem DinisJacinto2026.positive_iff_of_atMostMarginal {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {a b : O} (h : ml.AtMostMarginal (μ w a) (μ w b)) : Positive ml μ norm w a ↔ Positive ml μ norm w b

Objects whose degrees differ at most marginally are both in the positive form's extension or both out of it, Fara's similarity constraint (§6.1).

theorem DinisJacinto2026.positive_iff_of_reflTransGen {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {a b : O} (h : Relation.ReflTransGen ml.MarginallyLT (μ w a) (μ w b)) : Positive ml μ norm w a ↔ Positive ml μ norm w b

However many marginal steps separate two objects' degrees, the objects are alike for the positive form (§6.1).

theorem DinisJacinto2026.exists_large_step_of_soritical {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {a b : O} {R : O → O → Prop} (hR : ∀ ⦃x y : O⦄, R x y → μ w x < μ w y) (h : Relation.ReflTransGen R a b) (h₁ : ¬Positive ml μ norm w a) (h₂ : Positive ml μ norm w b) : ∃ (x : O) (y : O), R x y ∧ ¬Positive ml μ norm w x ∧ Positive ml μ norm w y ∧ ml.LargelyLT (μ w x) (μ w y)

In a Soritical sequence for the positive form, a chain of steps each raising the degree from someone out of the extension to someone in it, some step is large, the nonstandard primitivist solution to the Sorites (§3, §6.1).

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

A property is clustered when something has it iff its degree differs at most marginally from the degree of something that has it (§3).

Equations

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

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

Clustered degrees imply degree tolerance. An object whose degree is marginally greater than that of an object without the property lacks it, and an object whose degree is marginally smaller than that of an object with the property has it (§3). The ML axioms are not needed.

theorem DinisJacinto2026.clustered_positive {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} : Clustered ml (Positive ml μ norm w) (μ w)

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

theorem DinisJacinto2026.setOf_positive_eq_gt_over {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {f : α → Lex (ℚ × ℤ)} (hf : ml.IsHom (Degree.MarginalScale.lex ℚ ℤ) f) : {x : O | Positive ml μ norm w x} = (fun (x : O) => (ofLex (f (μ w x))).1) ⁻¹' Set.Ioi (ofLex (f norm)).1

Under a representation, the positive form is the strict comparison of an object's block with the standard's block.

theorem DinisJacinto2026.exists_isHom_setOf_positive_eq {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} [Countable α] (hf : DinisJacinto2025.FinitelyMarginal ml) : ∃ (f : α → Lex (ℚ × ℤ)), ml.IsHom (Degree.MarginalScale.lex ℚ ℤ) f ∧ ∀ (μ : C → O → α) (norm : α) (w : C), {x : O | Positive ml μ norm w x} = (fun (x : O) => (ofLex (f (μ w x))).1) ⁻¹' Set.Ioi (ofLex (f norm)).1

Every countable, finitely marginal scale has a representation under which the positive form, for every measure function, standard and circumstance, compares blocks, so reasoning about it can be carried out in the representative model (§5.2).

theorem DinisJacinto2026.zidane_ronaldo {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {C : Type u_2} {O : Type u_3} {μ : C → O → α} {norm : α} {w : C} {f : α → Lex (ℚ × ℤ)} (hf : ml.IsHom (Degree.MarginalScale.lex ℚ ℤ) f) {zidane ronaldo : O} (hz : (ofLex (f (μ w zidane))).1 = 1) (hr : (ofLex (f (μ w ronaldo))).1 = 0) (hn : (ofLex (f norm)).1 = 0) : Comparative μ w zidane w ronaldo ∧ Positive ml μ norm w zidane ∧ ¬Positive ml μ norm w ronaldo

If a representation places the standard and Ronaldo in block 0 and Zidane in block 1, then Zidane is balder than Ronaldo, and Zidane is bald where Ronaldo, though balder than the standard, is not (§5.2).

theorem DinisJacinto2026.exists_twoScale_not_comparative : ∃ (ρ : Bool → Unit → ℕ) (τ : Bool → ℕ → Lex (ℚ × ℤ)), Positive (Degree.MarginalScale.lex ℚ ℤ) (fun (w : Bool) (x : Unit) => τ w (ρ w x)) (toLex (0, 0)) true () ∧ ¬Positive (Degree.MarginalScale.lex ℚ ℤ) (fun (w : Bool) (x : Unit) => τ w (ρ w x)) (toLex (0, 0)) false () ∧ ¬Comparative ρ true () false ()

The two-scale alternative of §5.4 reads the comparative off precise degrees ρ and the positive form off vague degrees τ w of precise degrees. When the agent's interests change, it lets an object leave the positive form's extension without having been greater on the precise scale.