@cite{solt-2018}: Multidimensionality, Subjectivity and Scales

Stephanie Solt (2018). Multidimensionality, Subjectivity and Scales: Experimental Evidence. In The Semantics of Gradability, Vagueness, and Scale Structure, pp. 59–91. Springer.

Status

This file formalizes ONLY the experimental five-class typology from Solt's Figure 1 (pp. 5–6). The full theory (Section 5: dimensional measure functions for subjective vs objective comparatives, the qualitative-vs-quantitative distinction, the Hare-style criteria-vs- meaning split) is unformalized. The reason for the partial formalization is to provide the typology enum as a substrate-adjacent primitive that other gradability study files can reference by name — specifically:

• Phenomena/Gradability/Studies/Tham2025.lean (already in codebase; cracked belongs to AbsPart, the closest sibling class to clean/dirty/salty per Solt's classification)
• A future Lasersohn2005/Stephenson2007/Kennedy2013 study file on faultless disagreement would consume this as the typological partition that ordering-subjectivity respects

When a second consumer beyond Tham2025 lands, the full Section 5 theory becomes the natural extension to formalize.

The five classes (Solt's Figure 1, ordered by % "fact" judgments)

The experiment used a forced-choice subjectivity test on the comparative form of 35 adjectives. The five classes that emerged:

Class	% fact	Examples
RelNum	98%	tall, expensive, old, new
AbsTot	94%	full, empty
AbsPart	67%	wet, dry, straight, curved, rough, smooth, clean,
		dirty, salty
RelNo	55%	sharp, dull, dark, light, hard, soft
Eval	4%	good, bad, beautiful, pretty, ugly, easy, interesting,
		boring, tasty, fun, intelligent, happy, sad

The empirical finding: ordering subjectivity correlates with measurability (RelNum has measurement units; AbsTot has endpoints; Eval has neither), NOT with the standard objective/subjective binary. The middle class (AbsPart) is analytically interesting — these adjectives describe physical properties yet allow faultless disagreement about orderings. Tham 2025's cracked belongs here.

inductive Solt2018Multidim.SubjectivityClass : Type

Solt 2018 (Springer multidim chapter, Fig. 1) five-class typology of gradable adjectives, ordered by ordering-subjectivity:

relNum (most objective, 98% fact judgments) → absTot (94%) → absPart (67%) → relNo (55%) → eval (most subjective, 4% fact judgments).

The ordering is empirical (Solt's experimental result), not stipulative.

• relNum : SubjectivityClass

  Relative gradable, numerical measure (e.g. tall, expensive).

• absTot : SubjectivityClass

  Absolute gradable, totally-closed scale (e.g. full, empty).

• absPart : SubjectivityClass

  Absolute gradable, partially-closed scale (e.g. wet, dry, clean, dirty, salty — and Tham 2025's cracked).

• relNo : SubjectivityClass

  Relative gradable, no numerical measure (e.g. sharp, dull).

• eval : SubjectivityClass

  Evaluative (e.g. good, bad, beautiful, tasty).

@[implicit_reducible]

instance Solt2018Multidim.instReprSubjectivityClass : Repr SubjectivityClass

Equations

• Solt2018Multidim.instReprSubjectivityClass = { reprPrec := Solt2018Multidim.instReprSubjectivityClass.repr }

def Solt2018Multidim.instReprSubjectivityClass.repr : SubjectivityClass → Nat → Std.Format

Equations

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

def Solt2018Multidim.instBEqSubjectivityClass.beq : SubjectivityClass → SubjectivityClass → Bool

Equations

• Solt2018Multidim.instBEqSubjectivityClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Solt2018Multidim.instBEqSubjectivityClass : BEq SubjectivityClass

Equations

• Solt2018Multidim.instBEqSubjectivityClass = { beq := Solt2018Multidim.instBEqSubjectivityClass.beq }

@[implicit_reducible]

instance Solt2018Multidim.instDecidableEqSubjectivityClass : DecidableEq SubjectivityClass

Equations

• Solt2018Multidim.instDecidableEqSubjectivityClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Solt2018Multidim.SubjectivityClass.subjectivityRank : SubjectivityClass → Nat

Ordering-subjectivity rank (1 = most objective, 5 = most subjective). Reflects Solt's experimental ranking, not the % fact judgments themselves.

Equations

• Solt2018Multidim.SubjectivityClass.relNum.subjectivityRank = 1
• Solt2018Multidim.SubjectivityClass.absTot.subjectivityRank = 2
• Solt2018Multidim.SubjectivityClass.absPart.subjectivityRank = 3
• Solt2018Multidim.SubjectivityClass.relNo.subjectivityRank = 4
• Solt2018Multidim.SubjectivityClass.eval.subjectivityRank = 5

theorem Solt2018Multidim.subjectivityRank_strictly_ordered : SubjectivityClass.relNum.subjectivityRank < SubjectivityClass.absTot.subjectivityRank ∧ SubjectivityClass.absTot.subjectivityRank < SubjectivityClass.absPart.subjectivityRank ∧ SubjectivityClass.absPart.subjectivityRank < SubjectivityClass.relNo.subjectivityRank ∧ SubjectivityClass.relNo.subjectivityRank < SubjectivityClass.eval.subjectivityRank

The empirical ordering-subjectivity ranking from Solt's experiment: relNum < absTot < absPart < relNo < eval.

structure Solt2018Multidim.ClassifiedAdj : Type

A concrete adjective in Solt's 35-item sample, classified by the experiment. Solt's full Table is partially encoded here (the high-information cases — RelNum and Eval anchor points + the AbsPart middle class that Tham 2025 builds on). The complete 35-adjective table is unformalized; per-adjective classifications can be derived from the table on Fig. 1, p. 6.

• form : String
• cls : SubjectivityClass

def Solt2018Multidim.instReprClassifiedAdj.repr : ClassifiedAdj → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Solt2018Multidim.instReprClassifiedAdj : Repr ClassifiedAdj

Equations

• Solt2018Multidim.instReprClassifiedAdj = { reprPrec := Solt2018Multidim.instReprClassifiedAdj.repr }

@[implicit_reducible]

instance Solt2018Multidim.instBEqClassifiedAdj : BEq ClassifiedAdj

Equations

• Solt2018Multidim.instBEqClassifiedAdj = { beq := Solt2018Multidim.instBEqClassifiedAdj.beq }

def Solt2018Multidim.instBEqClassifiedAdj.beq : ClassifiedAdj → ClassifiedAdj → Bool

Equations

• Solt2018Multidim.instBEqClassifiedAdj.beq { form := a, cls := a_1 } { form := b, cls := b_1 } = (a == b && a_1 == b_1)
• Solt2018Multidim.instBEqClassifiedAdj.beq x✝¹ x✝ = false

def Solt2018Multidim.representativeSample : List ClassifiedAdj

A representative slice of Solt's 35-adjective sample, including the AbsPart middle class that Tham 2025's cracked extends.

Equations

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

def Solt2018Multidim.crackedClass : SubjectivityClass

Tham 2025's cracked belongs to the AbsPart class — the same class as clean, dirty, wet, dry. This is the cross-paper pointer that lets Tham 2025's substantive analysis be located in Solt's typology without requiring the full multidim chapter formalization.

Equations

• Solt2018Multidim.crackedClass = Solt2018Multidim.SubjectivityClass.absPart

theorem Solt2018Multidim.cracked_is_AbsPart : crackedClass = SubjectivityClass.absPart

theorem Solt2018Multidim.cracked_shares_class_with_dirty : Option.map ClassifiedAdj.cls (List.find? (fun (a : ClassifiedAdj) => a.form == "dirty") representativeSample) = some crackedClass

cracked shares Solt's experimental class with dirty — both are AbsPart predicates per Fig. 1. The look-up is via Option.bind to avoid .get! (no Inhabited instance needed).