Cresswell (1976): The Semantics of Degree

[Cre76]

Degrees of comparison in a λ-categorial possible-worlds semantics: a degree is a scale-tagged point ⟨u, >⟩ (2.1), er than (2.3) compares degrees only on a shared scale (so (23) taller man than … clever man is anomalous — the same-scale restriction [Bal08]'s universal scale later removes), the equative as as (2.7) is weak ≥ with exactly forcing =, and §4 grounds the degree ontology by constructing degrees from comparison relations: φ-equivalence classes (4.1) with the induced comparison well-defined (4.2). The construction is Degree.cresswellSetoid/Degree.CresswellDegree in Semantics/Degree/Hom.lean; this file checks the paper's claims on its own examples.

Formalized here: the (4.1)–(4.2) construction on the Arabella/Clarissa beauty example (62), the same-scale comparative (18) Bill is a taller man than Ophidia is a long snake (heights and lengths share the spatial-distance scale), the weak equative, and footnote 10's disjunctive than-clause universality (taller than Arabella or Clarissa = taller than both), derived from Degree.maxComparative.

§4: degrees constructed from comparisons (62)

inductive Cresswell1976.Person : Type

Individuals of the beauty example (62)–(63).

• arabella : Person
• clarissa : Person
• bill : Person
• tom : Person

@[implicit_reducible]

instance Cresswell1976.instDecidableEqPerson : DecidableEq Person

Equations

• Cresswell1976.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cresswell1976.instReprPerson : Repr Person

Equations

• Cresswell1976.instReprPerson = { reprPrec := Cresswell1976.instReprPerson.repr }

def Cresswell1976.instReprPerson.repr : Person → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cresswell1976.instReprPerson.repr Cresswell1976.Person.bill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cresswell1976.Person.bill")).group prec✝
• Cresswell1976.instReprPerson.repr Cresswell1976.Person.tom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cresswell1976.Person.tom")).group prec✝

def Cresswell1976.moreBeautiful : Person → Person → Prop

A comparison relation φ: x is more beautiful than y, with Bill and Tom equally beautiful (both below Clarissa, who is below Arabella).

Equations

• Cresswell1976.moreBeautiful Cresswell1976.Person.arabella Cresswell1976.Person.clarissa = True
• Cresswell1976.moreBeautiful Cresswell1976.Person.arabella Cresswell1976.Person.bill = True
• Cresswell1976.moreBeautiful Cresswell1976.Person.arabella Cresswell1976.Person.tom = True
• Cresswell1976.moreBeautiful Cresswell1976.Person.clarissa Cresswell1976.Person.bill = True
• Cresswell1976.moreBeautiful Cresswell1976.Person.clarissa Cresswell1976.Person.tom = True
• Cresswell1976.moreBeautiful x✝¹ x✝ = False

@[implicit_reducible]

instance Cresswell1976.instDecidableRelPersonMoreBeautiful : DecidableRel moreBeautiful

Equations

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

theorem Cresswell1976.bill_tom_same_degree : ⟦Person.bill⟧ = ⟦Person.tom⟧

Bill and Tom are φ-indistinguishable, so they determine the same degree of beauty — (4.1)'s equivalence collapses ties.

§2: same-scale comparison (18) and the equative (2.7)

def Cresswell1976.extent : Person → ℚ

Heights and lengths in the shared spatial-distance scale (ℚ): (2.2)'s point that tall and long "both involve the same scale" is what licenses (18).

Equations

• Cresswell1976.extent Cresswell1976.Person.bill = 6
• Cresswell1976.extent Cresswell1976.Person.tom = 5
• Cresswell1976.extent Cresswell1976.Person.arabella = 4
• Cresswell1976.extent Cresswell1976.Person.clarissa = 3

theorem Cresswell1976.er_than_single_scale (a b : Person) : (∃ (u₁ : ℚ) (u₂ : ℚ), u₁ = extent a ∧ u₂ = extent b ∧ u₂ < u₁) ↔ Degree.comparativeSem extent a b Core.Order.ScalePolarity.positive

(18) Bill is a taller man than Ophidia is a long snake, in the single-scale regime: the comparative reduces to comparativeSem on the shared measure ((2.3) with unique degree witnesses).

theorem Cresswell1976.as_as_weak (a b : Person) : extent b < extent a ∨ extent a = extent b ↔ Degree.equativeSem extent a b Core.Order.ScalePolarity.positive

(2.7): as as is the weak equative — "either u₁ > u₂ or u₁ = u₂" — i.e. equativeSem; exactly (u₁ = u₂) is equativeStrengthened.

Footnote 10: disjunctive than-clauses are universal

theorem Cresswell1976.taller_than_disjunction_iff (x y z : Person) : Degree.maxComparative (fun (x_1 : Person) => x_1 = x) (fun (w : Person) => w = y ∨ w = z) extent ↔ extent y < extent x ∧ extent z < extent x

Bill is taller than Arabella or Clarissa entails taller than both ((iii)–(v)): the than-clause maximum over a disjunctive predicate is the max of the two degrees, so the max-quantified comparative decomposes into the conjunction.