Documentation

Linglib.Studies.Bale2008

Bale (2008): A Universal Scale of Comparison #

Direct comparisons (Seymour is taller than he is wide) and indirect comparisons (Esme is more beautiful than Einstein is intelligent) unified through a Universal Scale Ω ≅ ℚ ∩ (0, 1]: individuals map to a primary scale built from an adjectival quasi-order restricted to a comparison class ([Cre76]-style equivalence classes), and the homomorphism ℌ maps each class to the universal degree encoding its relative position (Degree.relativeRank). MORE compares universal degrees (λμ λd λx. μ(x) ≻ d), so cross-scale comparison is well-typed; direct comparison is the special case where a measurement system structures both primary scales identically.

Formalized: the ten-member committee model with the beauty and intelligence orders, the (19a)/(19b) truth-value contrast, preservation of the primary order under ℌ, robustness of universal degrees under adding equally-ranked members (degrees count equivalence classes, not individuals), and the for-clause prediction that class-relative ranks can invert raw measurements (taller for a boy than wide for a boy false for a Seymour who is extremely wide but average in height).

The committee model (§4.2, Figs. 4–5) #

inductive Bale2008.Member :

The ten committee members a–j.

a : Member
b : Member
c : Member
d : Member
e : Member
f : Member
g : Member
h : Member
i : Member
j : Member

Instances For

@[implicit_reducible]

instance Bale2008.instDecidableEqMember :

DecidableEq Member

Equations

Bale2008.instDecidableEqMember x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bale2008.instReprMember.repr :

Member → ℕ → Std.Format

Equations

Bale2008.instReprMember.repr Bale2008.Member.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.a")).group prec✝
Bale2008.instReprMember.repr Bale2008.Member.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.b")).group prec✝
Bale2008.instReprMember.repr Bale2008.Member.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.c")).group prec✝
Bale2008.instReprMember.repr Bale2008.Member.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.d")).group prec✝
Bale2008.instReprMember.repr Bale2008.Member.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.e")).group prec✝
Bale2008.instReprMember.repr Bale2008.Member.f prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.f")).group prec✝
Bale2008.instReprMember.repr Bale2008.Member.g prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.g")).group prec✝
Bale2008.instReprMember.repr Bale2008.Member.h prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.h")).group prec✝
Bale2008.instReprMember.repr Bale2008.Member.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.i")).group prec✝
Bale2008.instReprMember.repr Bale2008.Member.j prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member.j")).group prec✝

Instances For

@[implicit_reducible]

instance Bale2008.instReprMember :

Equations

Bale2008.instReprMember = { reprPrec := Bale2008.instReprMember.repr }

def Bale2008.beautyPos :

Member → Fin 10

Position in the beauty primary scale, bottom = 0: the order a → b → c → d → e → f → g → h → i → j from most to least beautiful.

Equations

Instances For

def Bale2008.intelligencePos :

Member → Fin 10

Position in the intelligence primary scale: the order i → f → j → g → h → a → d → b → e → c from most to least intelligent.

Equations

Instances For

def Bale2008.universalBeauty (m : Member) :

ℚ

Universal beauty degree: ℌ applied to the member's class in the beauty scale. Betty (b) receives d_{9/10} as in Fig. 4.

Equations

Bale2008.universalBeauty m = Degree.relativeRank (Bale2008.beautyPos m)

Instances For

def Bale2008.universalIntelligence (m : Member) :

ℚ

Universal intelligence degree; Heather (h) receives d_{6/10} as in Fig. 5.

Equations

Bale2008.universalIntelligence m = Degree.relativeRank (Bale2008.intelligencePos m)

Instances For

theorem Bale2008.relativeRank_fin10 (k : Fin 10) :

Degree.relativeRank k = (↑↑k + 1) / 10

ℌ on a ten-class scale: position k from the bottom receives d_{(k+1)/10} (Figs. 4–5's degree labels).

theorem Bale2008.betty_beautiful_gt_heather_intelligent :

universalIntelligence Member.h < universalBeauty Member.b

(19a) Betty is more beautiful for a committee member than Heather is intelligent — true: d_{9/10} ≻ d_{6/10}.

theorem Bale2008.betty_intelligent_not_gt_evelin_beautiful :

¬universalBeauty Member.e < universalIntelligence Member.b

(19b) Betty is more intelligent for a committee member than Evelin is beautiful — false: d_{3/10} ⊁ d_{6/10}.

theorem Bale2008.more_eq_comparativeSem (x y : Member) :

universalIntelligence y < universalBeauty x ↔ universalBeauty x > universalIntelligence y

Indirect comparison IS the point-standard comparative over universal degrees: Bale's MORE = λμ λd λx. μ(x) ≻ d instantiated at the than-clause degree.

theorem Bale2008.universalBeauty_lt_iff (x y : Member) :

universalBeauty x < universalBeauty y ↔ beautyPos x < beautyPos y

ℌ preserves the primary scale (§3.2): within one scale, indirect comparison agrees with direct rank comparison.

Robustness (§4.2, Figs. 6–9): degrees count classes #

inductive Bale2008.Member' :

The expanded committee: five extra members, each exactly as beautiful as an original member (b' ≈ b, a' ≈ b, c' ≈ c, d' ≈ d, e' ≈ e per Fig. 6).

old (m : Member) : Member'
a' : Member'
b' : Member'
c' : Member'
d' : Member'
e' : Member'

Instances For

def Bale2008.instDecidableEqMember'.decEq (x✝ x✝¹ : Member') :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[implicit_reducible]

instance Bale2008.instDecidableEqMember' :

DecidableEq Member'

Equations

Bale2008.instDecidableEqMember' = Bale2008.instDecidableEqMember'.decEq

def Bale2008.instReprMember'.repr :

Member' → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
Bale2008.instReprMember'.repr Bale2008.Member'.a' prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member'.a'")).group prec✝
Bale2008.instReprMember'.repr Bale2008.Member'.b' prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member'.b'")).group prec✝
Bale2008.instReprMember'.repr Bale2008.Member'.c' prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member'.c'")).group prec✝
Bale2008.instReprMember'.repr Bale2008.Member'.d' prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member'.d'")).group prec✝
Bale2008.instReprMember'.repr Bale2008.Member'.e' prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Member'.e'")).group prec✝

Instances For

@[implicit_reducible]

instance Bale2008.instReprMember' :

Equations

Bale2008.instReprMember' = { reprPrec := Bale2008.instReprMember'.repr }

def Bale2008.beautyPos' :

Member' → Fin 10

Beauty class in the expanded model: equivalent members share a class, so the scale still has ten positions.

Equations

Instances For

theorem Bale2008.universalBeauty_stable (m : Member) :

Degree.relativeRank (beautyPos' (Member'.old m)) = universalBeauty m

Universal degrees are unchanged by adding equally-ranked members: the assignment "is based on the number of equivalence classes in the domain rather than the number of individuals".

For-clauses strip measurements (§1, §4.1) #

inductive Bale2008.Boy :

Five boys with height and width measurements (in feet): Seymour is 5 ft tall — dead average — but 4 ft wide — the widest by far.

seymour : Boy
huey : Boy
dewey : Boy
louie : Boy
webby : Boy

Instances For

@[implicit_reducible]

instance Bale2008.instDecidableEqBoy :

DecidableEq Boy

Equations

Bale2008.instDecidableEqBoy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bale2008.instReprBoy.repr :

Boy → ℕ → Std.Format

Equations

Bale2008.instReprBoy.repr Bale2008.Boy.seymour prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Boy.seymour")).group prec✝
Bale2008.instReprBoy.repr Bale2008.Boy.huey prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Boy.huey")).group prec✝
Bale2008.instReprBoy.repr Bale2008.Boy.dewey prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Boy.dewey")).group prec✝
Bale2008.instReprBoy.repr Bale2008.Boy.louie prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Boy.louie")).group prec✝
Bale2008.instReprBoy.repr Bale2008.Boy.webby prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Boy.webby")).group prec✝

Instances For

@[implicit_reducible]

instance Bale2008.instReprBoy :

Repr Boy

Equations

Bale2008.instReprBoy = { reprPrec := Bale2008.instReprBoy.repr }

def Bale2008.heightFt :

Boy → ℚ

Equations

Bale2008.heightFt Bale2008.Boy.seymour = 5
Bale2008.heightFt Bale2008.Boy.huey = 6
Bale2008.heightFt Bale2008.Boy.dewey = 55 / 10
Bale2008.heightFt Bale2008.Boy.louie = 45 / 10
Bale2008.heightFt Bale2008.Boy.webby = 4

Instances For

def Bale2008.widthFt :

Boy → ℚ

Equations

Bale2008.widthFt Bale2008.Boy.seymour = 4
Bale2008.widthFt Bale2008.Boy.huey = 2
Bale2008.widthFt Bale2008.Boy.dewey = 15 / 10
Bale2008.widthFt Bale2008.Boy.louie = 1
Bale2008.widthFt Bale2008.Boy.webby = 1 / 2

Instances For

def Bale2008.heightPos :

Boy → Fin 5

Class-relative height position among the boys (Seymour: middle).

Equations

Instances For

def Bale2008.widthPos :

Boy → Fin 5

Class-relative width position among the boys (Seymour: top).

Equations

Instances For

theorem Bale2008.seymour_for_a_boy :

widthFt Boy.seymour < heightFt Boy.seymour ∧ ¬Degree.relativeRank (widthPos Boy.seymour) < Degree.relativeRank (heightPos Boy.seymour)

Seymour is taller for a boy than he is wide for a boy is FALSE "despite the fact that the measurement of his height is greater than the measurement of his width": for-clauses restrict the primary scales to measurement-free class-relative ones, on which Seymour's width position exceeds his height position.