Documentation

Linglib.Studies.Bale2008

Bale 2008: a universal scale of comparison #

One interpretation of the comparative serves both indirect comparisons (Esme is more beautiful than Einstein is intelligent) and direct ones (Seymour is taller than he is wide). A gradable adjective ranks the comparison class; the ranking's classes form the primary scale; and each class is sent to the universal degree that records its relative position, a fraction with the number of classes as denominator. The comparative says that the subject's universal degree exceeds the standard's, whatever the two scales. Adding members equivalent to existing ones changes no degree, since classes, not members, are counted. A direct comparison is what results when measurements — inches, treated as individuals — belong to both comparison classes: each class then holds exactly one measurement, both scales take the same values, and comparing universal degrees is comparing measurements. A for-phrase or a modified nominal restricts the comparison class to people, drops the measurements, and forces an indirect comparison: Seymour, the shortest of the men but as wide as the widest, is taller than he is wide yet not taller for a man than he is wide for a man.

Main definitions #

Member, beauty, intelligence: the ten-member committee and its two rankings; Member', beautyTwin, intelligenceTwin: the expanded committee, each new member as beautiful and as intelligent as an original one.
Person, height, width: the seven people together with the measurements up to eighty inches, ranked by height and width in inches.
heightClass, widthClass: the nineteen men ranked among themselves.

Main results #

committee: the two committee sentences' truth values; expanded: the expanded committee assigns every member the degree it had.
direct_comparison, seymour: with measurements in both scales universal degrees compare as measurements do, so Seymour is taller than he is wide.
not_more_of_least_of_greatest, for_a_man: a subject lowest on its scale is never more than a standard highest on its own, so Seymour is not taller for a man than he is wide for a man.
rows_truth: the paper's evaluated sentences take the truth values it reports.

References #

[bale-2008]
[Cre76] — scales as quotients of a comparison relation
[klein-1980] — comparison classes and the delineation alternative
[Ken99] — the measure-function interpretation and the comparative
[BV72] — comparisons of deviation
[fox-hackl-2006] — density of the universal scale

The comparative #

def Bale2008.More {α : Type u_1} {β : Type u_2} (μ₁ : α → ℚ) (x : α) (μ₂ : β → ℚ) (y : β) :

x is more ADJ₁ than y is ADJ₂: the subject's universal degree on its scale exceeds the standard's on its own.

Equations

Bale2008.More μ₁ x μ₂ y = (μ₂ y < μ₁ x)

Instances For

theorem Bale2008.not_more_of_least_of_greatest {α : Type u_1} {β : Type u_2} {D : Type u_3} {D' : Type u_4} [Fintype α] [Fintype β] [LinearOrder D] [LinearOrder D'] (rank₁ : α → D) (rank₂ : β → D') {x : α} {y : β} (hx : ∀ (z : α), rank₁ x ≤ rank₁ z) (hy : ∀ (z : β), rank₂ z ≤ rank₂ y) :

¬More (Degree.universalDegree rank₁) x (Degree.universalDegree rank₂) y

A subject ranked lowest on its scale is never more than a standard ranked highest on its own: its degree is at most one over the number of classes and the standard's is one.

The committee #

inductive Bale2008.Member :

The ten committee members; b is Betty, e Evelin, h Heather.

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

Instances For

@[instance_reducible]

instance Bale2008.instDecidableEqMember :

DecidableEq Member

Equations

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

@[instance_reducible]

instance Bale2008.instFintypeMember :

Fintype Member

Equations

Bale2008.instFintypeMember = { elems := { val := ↑Bale2008.Member.enumList, nodup := Bale2008.Member.enumList_nodup }, complete := Bale2008.instFintypeMember._proof_1 }

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

@[instance_reducible]

instance Bale2008.instReprMember :

Equations

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

def Bale2008.beauty :

Member → Fin 10

The ranking by beauty, most beautiful highest: a, b, c, d, e, f, g, h, i, j.

Equations

Instances For

def Bale2008.intelligence :

Member → Fin 10

The ranking by intelligence, most intelligent highest: i, f, j, g, h, a, d, b, e, c.

Equations

Instances For

theorem Bale2008.beauty_surjective :

Function.Surjective beauty

theorem Bale2008.intelligence_surjective :

Function.Surjective intelligence

theorem Bale2008.universalDegree_beauty (m : Member) :

Degree.universalDegree beauty m = (↑↑(beauty m) + 1) / 10

With no ties, a member's universal degree is one plus the number below them, over ten.

theorem Bale2008.universalDegree_intelligence (m : Member) :

Degree.universalDegree intelligence m = (↑↑(intelligence m) + 1) / 10

theorem Bale2008.committee :

More (Degree.universalDegree beauty) Member.b (Degree.universalDegree intelligence) Member.h ∧ ¬More (Degree.universalDegree intelligence) Member.b (Degree.universalDegree beauty) Member.e

Betty, second most beautiful, is more beautiful for a committee member than Heather, fifth most intelligent, is intelligent; Betty, third least intelligent, is not more intelligent than Evelin, fifth most beautiful, is beautiful.

inductive Bale2008.Member' :

The expanded committee: five further members, each as beautiful and as intelligent as one of the original ten.

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

@[instance_reducible]

instance Bale2008.instDecidableEqMember' :

DecidableEq Member'

Equations

Bale2008.instDecidableEqMember' = Bale2008.instDecidableEqMember'.decEq

@[instance_reducible]

instance Bale2008.instFintypeMember' :

Fintype Member'

Equations

Bale2008.instFintypeMember' = Fintype.ofEquiv (Bale2008.Member ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit) Bale2008.Member'.proxyTypeEquiv

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

@[instance_reducible]

instance Bale2008.instReprMember' :

Equations

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

def Bale2008.beautyTwin :

Member' → Member

The original member each is as beautiful as: a′ and b′ as Betty, c′ as c, d′ as d, e′ as Evelin.

Equations

Instances For

def Bale2008.intelligenceTwin :

Member' → Member

The original member each is as intelligent as: a′ as Heather, b′ and c′ as Betty, d′ as f, e′ as Evelin.

Equations

Instances For

theorem Bale2008.expanded (m : Member') :

Degree.universalDegree (beauty ∘ beautyTwin) m = Degree.universalDegree beauty (beautyTwin m) ∧ Degree.universalDegree (intelligence ∘ intelligenceTwin) m = Degree.universalDegree intelligence (intelligenceTwin m)

Every member of the expanded committee keeps the degree of the original member they match, on both scales: the quotient absorbs the newcomers into existing classes.

Measurements #

inductive Bale2008.Person :

The seven people of the height-and-width situation; s is Seymour.

a : Person
b : Person
c : Person
d : Person
e : Person
f : Person
s : Person

Instances For

@[instance_reducible]

instance Bale2008.instDecidableEqPerson :

DecidableEq Person

Equations

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

@[instance_reducible]

instance Bale2008.instFintypePerson :

Fintype Person

Equations

Bale2008.instFintypePerson = { elems := { val := ↑Bale2008.Person.enumList, nodup := Bale2008.Person.enumList_nodup }, complete := Bale2008.instFintypePerson._proof_1 }

def Bale2008.instReprPerson.repr :

Person → ℕ → Std.Format

Equations

Bale2008.instReprPerson.repr Bale2008.Person.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Person.a")).group prec✝
Bale2008.instReprPerson.repr Bale2008.Person.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Person.b")).group prec✝
Bale2008.instReprPerson.repr Bale2008.Person.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Person.c")).group prec✝
Bale2008.instReprPerson.repr Bale2008.Person.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Person.d")).group prec✝
Bale2008.instReprPerson.repr Bale2008.Person.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Person.e")).group prec✝
Bale2008.instReprPerson.repr Bale2008.Person.f prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Person.f")).group prec✝
Bale2008.instReprPerson.repr Bale2008.Person.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Person.s")).group prec✝

Instances For

@[instance_reducible]

instance Bale2008.instReprPerson :

Equations

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

def Bale2008.height :

Person ⊕ Fin 80 → Fin 80

The height ranking over people and the measurements from one to eighty inches, in inches above one: a six foot three, b six foot two, c six foot, d, e and f five foot ten, Seymour five foot two, and each measurement itself.

Equations

Bale2008.height (Sum.inl Bale2008.Person.a) = 74
Bale2008.height (Sum.inl Bale2008.Person.b) = 73
Bale2008.height (Sum.inl Bale2008.Person.c) = 71
Bale2008.height (Sum.inl Bale2008.Person.d) = 69
Bale2008.height (Sum.inl Bale2008.Person.e) = 69
Bale2008.height (Sum.inl Bale2008.Person.f) = 69
Bale2008.height (Sum.inl Bale2008.Person.s) = 61
Bale2008.height (Sum.inr m) = m

Instances For

def Bale2008.width :

Person ⊕ Fin 80 → Fin 80

The width ranking: Seymour three feet, f two foot five, b two foot two, the rest two foot one, and each measurement itself.

Equations

Bale2008.width (Sum.inl Bale2008.Person.s) = 35
Bale2008.width (Sum.inl Bale2008.Person.f) = 28
Bale2008.width (Sum.inl Bale2008.Person.b) = 25
Bale2008.width (Sum.inl Bale2008.Person.a) = 24
Bale2008.width (Sum.inl Bale2008.Person.c) = 24
Bale2008.width (Sum.inl Bale2008.Person.d) = 24
Bale2008.width (Sum.inl Bale2008.Person.e) = 24
Bale2008.width (Sum.inr m) = m

Instances For

theorem Bale2008.height_surjective :

Function.Surjective height

theorem Bale2008.width_surjective :

Function.Surjective width

theorem Bale2008.direct_comparison (x y : Person ⊕ Fin 80) :

More (Degree.universalDegree height) x (Degree.universalDegree width) y ↔ width y < height x

Each class of either scale holds exactly one measurement, so the two scales take the same values and comparing universal degrees is comparing measurements: a direct comparison.

theorem Bale2008.seymour_measured :

Degree.universalDegree height (Sum.inl Person.s) = 62 / 80 ∧ Degree.universalDegree width (Sum.inl Person.s) = 36 / 80 ∧ More (Degree.universalDegree height) (Sum.inl Person.s) (Degree.universalDegree width) (Sum.inl Person.s) ∧ ¬More (Degree.universalDegree width) (Sum.inl Person.s) (Degree.universalDegree height) (Sum.inl Person.s)

Seymour's universal degrees are his measurements over eighty, so he is taller than he is wide and not wider than he is tall.

For a man #

@[reducible, inline]

abbrev Bale2008.Man :

The nineteen men, Seymour last.

Equations

Bale2008.Man = Fin 19

Instances For

def Bale2008.seymour :

Seymour.

Equations

Bale2008.seymour = 18

Instances For

def Bale2008.heightClass (m : Man) :

Fin 8

The height classes of the men: Seymour alone in the lowest of eight. The text fixes only that every other man is taller; their classes reproduce the eight levels of the paper's figure.

Equations

Bale2008.heightClass m = if m = Bale2008.seymour then 0 else ⟨↑m % 7 + 1, ⋯⟩

Instances For

def Bale2008.widthClass (m : Man) :

Fin 7

The width classes of the men: Seymour and one other man in the highest of seven.

Equations

Bale2008.widthClass m = if m = Bale2008.seymour ∨ m = 8 then 6 else ⟨↑m % 6, ⋯⟩

Instances For

theorem Bale2008.seymour_shortest (m : Man) :

heightClass seymour ≤ heightClass m

theorem Bale2008.seymour_widest (m : Man) :

widthClass m ≤ widthClass seymour

theorem Bale2008.for_a_man :

Degree.universalDegree heightClass seymour = 1 / 8 ∧ Degree.universalDegree widthClass seymour = 1 ∧ ¬More (Degree.universalDegree heightClass) seymour (Degree.universalDegree widthClass) seymour

Restricted to men, Seymour's height degree is one eighth and his width degree one, so he is not taller for a man than he is wide for a man, though five feet exceeds three.

The rows #

def Bale2008.Member.parse? :

String → Option Member

A committee member by name.

Equations

Bale2008.Member.parse? "a" = some Bale2008.Member.a
Bale2008.Member.parse? "b" = some Bale2008.Member.b
Bale2008.Member.parse? "c" = some Bale2008.Member.c
Bale2008.Member.parse? "d" = some Bale2008.Member.d
Bale2008.Member.parse? "e" = some Bale2008.Member.e
Bale2008.Member.parse? "f" = some Bale2008.Member.f
Bale2008.Member.parse? "g" = some Bale2008.Member.g
Bale2008.Member.parse? "h" = some Bale2008.Member.h
Bale2008.Member.parse? "i" = some Bale2008.Member.i
Bale2008.Member.parse? "j" = some Bale2008.Member.j
Bale2008.Member.parse? x✝ = none

Instances For

def Bale2008.Person.parse? :

String → Option Person

A person of the measured situation by name.

Equations

Bale2008.Person.parse? "a" = some Bale2008.Person.a
Bale2008.Person.parse? "b" = some Bale2008.Person.b
Bale2008.Person.parse? "c" = some Bale2008.Person.c
Bale2008.Person.parse? "d" = some Bale2008.Person.d
Bale2008.Person.parse? "e" = some Bale2008.Person.e
Bale2008.Person.parse? "f" = some Bale2008.Person.f
Bale2008.Person.parse? "s" = some Bale2008.Person.s
Bale2008.Person.parse? x✝ = none

Instances For

def Bale2008.degree? (r : Data.Examples.LinguisticExample) (who scale : String) :

Option ℚ

The universal degree a row assigns one of its participants, by model and scale.

Equations

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

Instances For

def Bale2008.truth? (r : Data.Examples.LinguisticExample) :

Option Bool

The truth value the paper reports.

Equations

Bale2008.truth? r = match r.feature? "truth" with | some "true" => some true | some "false" => some false | x => none

Instances For

theorem Bale2008.rows_truth (r : Data.Examples.LinguisticExample) :

r ∈ Examples.all → ∀ t ∈ truth? r, ∀ d₁ ∈ degree? r "subject" "subjectScale", ∀ d₂ ∈ degree? r "standard" "standardScale", d₂ < d₁ ↔ t = true

Every sentence the paper evaluates in one of its situations has the truth value it reports: the subject's universal degree exceeds the standard's exactly when the paper says the sentence is true.