Bale (2008): A universal scale of comparison

A gradable adjective orders a comparison class by a quasi-order, such as has as much beauty as. Its classes of equivalent members form the primary scale, and each member is sent to the universal degree of its class: one plus the number of classes below it, over the number of classes. The comparative compares universal degrees whatever the two scales, so one interpretation serves indirect comparisons (Betty is more beautiful than Heather is intelligent) and direct ones (Seymour is taller than he is wide). A comparison is direct when the comparison class contains the measurements in inches up to a bound and everyone is as tall, or as wide, as exactly one of them: both primary scales are then the measurement system, and universal degrees compare as measurements do. A for-clause restricts the comparison class to men and drops the measurements, so Seymour, short and very wide, is taller than he is wide but not taller for a man than he is wide for a man.

Main statements

• indirect_comparison: Betty is more beautiful than Heather is intelligent, but not more intelligent than Evelin is beautiful.
• direct_comparison: with the measurements up to a common bound in the comparison class, comparing universal degrees is comparing measurements.
• for_a_man: under the same quasi-orders, Seymour is taller than he is wide but not taller for a man than he is wide for a man.
• rows_truth: the sentences the paper evaluates take the truth values it reports.

Implementation notes

• Universal degrees are Degree.universalDegree: an adjective's quasi-order is given by a measure into a linear order, and a comparison class by a finite set, which restricts the quasi-order as Klein's comparison classes do.
• The comparative is Kennedy's, as in the paper: MORE applied to the greatest degree the than-clause reaches is Degree.MaxComparative .gt over the two measures (more_iff), stated as the point comparison μ ⁻¹' Set.Ioi n.
• Universal degrees are rationals: the paper's universal scale is the rationals from zero to one.
• Measurements are individuals .inr n of n inches, bounded by the comparison class; heights and widths are in inches as printed, and the committee's rankings count from the bottom.

References

• [Bal08]
• [Ken99]
• [Kle80]

The comparative

theorem Bale2008.more_iff {E : Type u_1} {F : Type u_2} (μ₁ : E → ℚ) (μ₂ : F → ℚ) (x : E) (y : F) : Degree.MaxComparative Degree.Comparison.gt (fun (x_1 : E ⊕ F) => x_1 = Sum.inl x) (fun (x : E ⊕ F) => x = Sum.inr y) (Sum.elim μ₁ μ₂) ↔ x ∈ μ₁ ⁻¹' Set.Ioi (μ₂ y)

MORE applied to the greatest degree to which y is ADJ₂, the meaning of x is more ADJ₁ than y is ADJ₂, holds of x exactly when the degree of x exceeds that of y.

theorem Bale2008.not_more_of_least_of_greatest {D : Type u_1} {D' : Type u_2} {E : Type u_3} {F : Type u_4} [LinearOrder D] [DecidableEq D] [LinearOrder D'] [DecidableEq D'] {μ : E → D} {ν : F → D'} {C : Finset E} {C' : Finset F} {x : E} {y : F} (hx : x ∈ C) (hy : y ∈ C') (hmin : ∀ z ∈ C, μ x ≤ μ z) (hmax : ∀ z ∈ C', ν z ≤ ν y) : x ∉ Degree.universalDegree μ C ⁻¹' Set.Ioi (Degree.universalDegree ν C' y)

A member lowest on one scale is not more ADJ₁ than a member highest on another is ADJ₂, since its degree is at most one over the number of classes and the standard's is one.

The committee

inductive Bale2008.Member : Type

The committee has ten original members a–j, among them Betty (b), Evelin (e) and Heather (h), and the expanded committee adds five members a'–e'.

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

@[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✝
• 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✝

@[instance_reducible]

instance Bale2008.instReprMember : Repr Member

Equations

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

def Bale2008.original : Finset Member

The original ten members.

Equations

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

def Bale2008.beauty : Member → ℕ

A member's beauty is their position counted from the least beautiful, the original ten ranking a, b, c, …, j from the most beautiful down; a' and b' are as beautiful as Betty, c' as c, d' as d and e' as Evelin.

Equations

• Bale2008.beauty Bale2008.Member.a = 10
• Bale2008.beauty Bale2008.Member.b = 9
• Bale2008.beauty Bale2008.Member.a' = 9
• Bale2008.beauty Bale2008.Member.b' = 9
• Bale2008.beauty Bale2008.Member.c = 8
• Bale2008.beauty Bale2008.Member.c' = 8
• Bale2008.beauty Bale2008.Member.d = 7
• Bale2008.beauty Bale2008.Member.d' = 7
• Bale2008.beauty Bale2008.Member.e = 6
• Bale2008.beauty Bale2008.Member.e' = 6
• Bale2008.beauty Bale2008.Member.f = 5
• Bale2008.beauty Bale2008.Member.g = 4
• Bale2008.beauty Bale2008.Member.h = 3
• Bale2008.beauty Bale2008.Member.i = 2
• Bale2008.beauty Bale2008.Member.j = 1

def Bale2008.intelligence : Member → ℕ

A member's intelligence is their position counted from the least intelligent, the original ten ranking i, f, j, g, h, a, d, b, e, c from the most intelligent down; a' is as intelligent as Heather, b' and c' as Betty, d' as f and e' as Evelin.

Equations

• Bale2008.intelligence Bale2008.Member.i = 10
• Bale2008.intelligence Bale2008.Member.f = 9
• Bale2008.intelligence Bale2008.Member.d' = 9
• Bale2008.intelligence Bale2008.Member.j = 8
• Bale2008.intelligence Bale2008.Member.g = 7
• Bale2008.intelligence Bale2008.Member.h = 6
• Bale2008.intelligence Bale2008.Member.a' = 6
• Bale2008.intelligence Bale2008.Member.a = 5
• Bale2008.intelligence Bale2008.Member.d = 4
• Bale2008.intelligence Bale2008.Member.b = 3
• Bale2008.intelligence Bale2008.Member.b' = 3
• Bale2008.intelligence Bale2008.Member.c' = 3
• Bale2008.intelligence Bale2008.Member.e = 2
• Bale2008.intelligence Bale2008.Member.e' = 2
• Bale2008.intelligence Bale2008.Member.c = 1

theorem Bale2008.indirect_comparison : Member.b ∈ Degree.universalDegree beauty original ⁻¹' Set.Ioi (Degree.universalDegree intelligence original Member.h) ∧ Member.b ∉ Degree.universalDegree intelligence original ⁻¹' Set.Ioi (Degree.universalDegree beauty original 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.

theorem Bale2008.expanded : Degree.universalDegree beauty Finset.univ = Degree.universalDegree beauty original ∧ Degree.universalDegree intelligence Finset.univ = Degree.universalDegree intelligence original

The expanded committee assigns every member the universal degrees the original committee does, since each newcomer joins an existing class.

Measurements

def Bale2008.withMeasurements {E : Type u_1} (P : Finset E) (N : ℕ) : Finset (E ⊕ ℕ)

The comparison class of the people in P and the measurements from one to N inches.

Equations

• Bale2008.withMeasurements P N = P.disjSum (Finset.Icc 1 N)

theorem Bale2008.image_withMeasurements {E : Type u_1} {μ : E ⊕ ℕ → ℕ} {P : Finset E} {N : ℕ} (hμ : ∀ (n : ℕ), μ (Sum.inr n) = n) (hP : ∀ x ∈ P, μ (Sum.inl x) ∈ Finset.Icc 1 N) : Finset.image μ (withMeasurements P N) = Finset.Icc 1 N

When each measurement measures itself and every person measures one of the measurements up to N, the classes are the measurements.

theorem Bale2008.universalDegree_withMeasurements {E : Type u_1} {μ : E ⊕ ℕ → ℕ} {P : Finset E} {N : ℕ} (hμ : ∀ (n : ℕ), μ (Sum.inr n) = n) (hP : ∀ x ∈ P, μ (Sum.inl x) ∈ Finset.Icc 1 N) {x : E} (hx : x ∈ P) : Degree.universalDegree μ (withMeasurements P N) (Sum.inl x) = ↑(μ (Sum.inl x)) / ↑N

With the measurements up to N in the comparison class, a person's universal degree is their measurement over N.

theorem Bale2008.direct_comparison {E : Type u_1} {μ ν : E ⊕ ℕ → ℕ} {P : Finset E} {N : ℕ} (hμ : ∀ (n : ℕ), μ (Sum.inr n) = n) (hν : ∀ (n : ℕ), ν (Sum.inr n) = n) (hPμ : ∀ x ∈ P, μ (Sum.inl x) ∈ Finset.Icc 1 N) (hPν : ∀ x ∈ P, ν (Sum.inl x) ∈ Finset.Icc 1 N) {z w : E ⊕ ℕ} (hz : z ∈ withMeasurements P N) (hw : w ∈ withMeasurements P N) : z ∈ Degree.universalDegree μ (withMeasurements P N) ⁻¹' Set.Ioi (Degree.universalDegree ν (withMeasurements P N) w) ↔ ν w < μ z

When the comparison class keeps the measurements up to a common bound, each measuring itself on both scales, and everyone measures within the bound, comparing universal degrees is comparing measurements, as in a direct comparison.

inductive Bale2008.Person : Type

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

@[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 }

@[instance_reducible]

instance Bale2008.instReprPerson : Repr Person

Equations

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

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✝

def Bale2008.height : Person ⊕ ℕ → ℕ

Heights are in inches. Man a is six foot three, b six foot two, c six foot, d, e and f five foot ten and Seymour five foot two, and a measurement is as tall as itself.

Equations

• Bale2008.height (Sum.inl Bale2008.Person.a) = 75
• Bale2008.height (Sum.inl Bale2008.Person.b) = 74
• Bale2008.height (Sum.inl Bale2008.Person.c) = 72
• Bale2008.height (Sum.inl Bale2008.Person.d) = 70
• Bale2008.height (Sum.inl Bale2008.Person.e) = 70
• Bale2008.height (Sum.inl Bale2008.Person.f) = 70
• Bale2008.height (Sum.inl Bale2008.Person.s) = 62
• Bale2008.height (Sum.inr n) = n

def Bale2008.width : Person ⊕ ℕ → ℕ

Widths are in inches. Seymour is three feet wide, f two foot five, b two foot two and the rest two foot one, and a measurement is as wide as itself.

Equations

• Bale2008.width (Sum.inl Bale2008.Person.s) = 36
• Bale2008.width (Sum.inl Bale2008.Person.f) = 29
• Bale2008.width (Sum.inl Bale2008.Person.b) = 26
• Bale2008.width (Sum.inl Bale2008.Person.a) = 25
• Bale2008.width (Sum.inl Bale2008.Person.c) = 25
• Bale2008.width (Sum.inl Bale2008.Person.d) = 25
• Bale2008.width (Sum.inl Bale2008.Person.e) = 25
• Bale2008.width (Sum.inr n) = n

def Bale2008.measured : Finset (Person ⊕ ℕ)

The comparison class of the height and width situation holds the seven people and the measurements up to eighty inches.

Equations

• Bale2008.measured = Bale2008.withMeasurements Finset.univ 80

theorem Bale2008.taller_than_wide : Degree.universalDegree height measured (Sum.inl Person.s) = 62 / 80 ∧ Degree.universalDegree width measured (Sum.inl Person.s) = 36 / 80 ∧ Sum.inl Person.s ∈ Degree.universalDegree height measured ⁻¹' Set.Ioi (Degree.universalDegree width measured (Sum.inl Person.s)) ∧ Sum.inl Person.s ∉ Degree.universalDegree width measured ⁻¹' Set.Ioi (Degree.universalDegree height measured (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

inductive Bale2008.Man : Type

The nineteen men; s is Seymour.

• a : Man
• b : Man
• c : Man
• d : Man
• e : Man
• f : Man
• g : Man
• h : Man
• i : Man
• j : Man
• k : Man
• l : Man
• m : Man
• n : Man
• o : Man
• p : Man
• q : Man
• r : Man
• s : Man

@[instance_reducible]

instance Bale2008.instDecidableEqMan : DecidableEq Man

Equations

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

@[instance_reducible]

instance Bale2008.instFintypeMan : Fintype Man

Equations

• Bale2008.instFintypeMan = { elems := { val := ↑Bale2008.Man.enumList, nodup := Bale2008.Man.enumList_nodup }, complete := Bale2008.instFintypeMan._proof_1 }

def Bale2008.instReprMan.repr : Man → ℕ → Std.Format

Equations

• Bale2008.instReprMan.repr Bale2008.Man.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.a")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.b")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.c")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.d")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.e")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.f prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.f")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.g prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.g")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.h prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.h")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.i")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.j prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.j")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.k prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.k")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.l")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.m prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.m")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.n")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.o")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.p")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.q prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.q")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.r")).group prec✝
• Bale2008.instReprMan.repr Bale2008.Man.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bale2008.Man.s")).group prec✝

@[instance_reducible]

instance Bale2008.instReprMan : Repr Man

Equations

• Bale2008.instReprMan = { reprPrec := Bale2008.instReprMan.repr }

def Bale2008.heightClass : Man → ℕ

A man's height class counts from the shortest. Seymour is alone at the bottom, followed by o and p; k, l, m and n; q and c; f, g, h and i; d and e; j and r; and a and b.

Equations

• Bale2008.heightClass Bale2008.Man.s = 1
• Bale2008.heightClass Bale2008.Man.o = 2
• Bale2008.heightClass Bale2008.Man.p = 2
• Bale2008.heightClass Bale2008.Man.k = 3
• Bale2008.heightClass Bale2008.Man.l = 3
• Bale2008.heightClass Bale2008.Man.m = 3
• Bale2008.heightClass Bale2008.Man.n = 3
• Bale2008.heightClass Bale2008.Man.q = 4
• Bale2008.heightClass Bale2008.Man.c = 4
• Bale2008.heightClass Bale2008.Man.f = 5
• Bale2008.heightClass Bale2008.Man.g = 5
• Bale2008.heightClass Bale2008.Man.h = 5
• Bale2008.heightClass Bale2008.Man.i = 5
• Bale2008.heightClass Bale2008.Man.d = 6
• Bale2008.heightClass Bale2008.Man.e = 6
• Bale2008.heightClass Bale2008.Man.j = 7
• Bale2008.heightClass Bale2008.Man.r = 7
• Bale2008.heightClass Bale2008.Man.a = 8
• Bale2008.heightClass Bale2008.Man.b = 8

def Bale2008.widthClass : Man → ℕ

A man's width class counts from the narrowest. Men q, r and a are at the bottom, then p; n and o; j, k, l and m; f, g and h; b, c, d and e; and Seymour and i at the top.

Equations

• Bale2008.widthClass Bale2008.Man.q = 1
• Bale2008.widthClass Bale2008.Man.r = 1
• Bale2008.widthClass Bale2008.Man.a = 1
• Bale2008.widthClass Bale2008.Man.p = 2
• Bale2008.widthClass Bale2008.Man.n = 3
• Bale2008.widthClass Bale2008.Man.o = 3
• Bale2008.widthClass Bale2008.Man.j = 4
• Bale2008.widthClass Bale2008.Man.k = 4
• Bale2008.widthClass Bale2008.Man.l = 4
• Bale2008.widthClass Bale2008.Man.m = 4
• Bale2008.widthClass Bale2008.Man.f = 5
• Bale2008.widthClass Bale2008.Man.g = 5
• Bale2008.widthClass Bale2008.Man.h = 5
• Bale2008.widthClass Bale2008.Man.b = 6
• Bale2008.widthClass Bale2008.Man.c = 6
• Bale2008.widthClass Bale2008.Man.d = 6
• Bale2008.widthClass Bale2008.Man.e = 6
• Bale2008.widthClass Bale2008.Man.i = 7
• Bale2008.widthClass Bale2008.Man.s = 7

def Bale2008.men : Finset (Man ⊕ ℕ)

The comparison class that for a man fixes holds the men and no measurements.

Equations

• Bale2008.men = Finset.map Function.Embedding.inl Finset.univ

theorem Bale2008.for_a_man {τ ω : Man ⊕ ℕ → ℕ} (hτ : ∀ (x y : Man), τ (Sum.inl x) ≤ τ (Sum.inl y) ↔ heightClass x ≤ heightClass y) (hω : ∀ (x y : Man), ω (Sum.inl x) ≤ ω (Sum.inl y) ↔ widthClass x ≤ widthClass y) (hτn : ∀ (n : ℕ), τ (Sum.inr n) = n) (hωn : ∀ (n : ℕ), ω (Sum.inr n) = n) (hs : τ (Sum.inl Man.s) = 60 ∧ ω (Sum.inl Man.s) = 36) (hb : ∀ (x : Man), τ (Sum.inl x) ∈ Finset.Icc 1 80 ∧ ω (Sum.inl x) ∈ Finset.Icc 1 80) : Sum.inl Man.s ∈ Degree.universalDegree τ (withMeasurements Finset.univ 80) ⁻¹' Set.Ioi (Degree.universalDegree ω (withMeasurements Finset.univ 80) (Sum.inl Man.s)) ∧ Degree.universalDegree τ men (Sum.inl Man.s) = 1 / 8 ∧ Degree.universalDegree ω men (Sum.inl Man.s) = 1 ∧ Sum.inl Man.s ∉ Degree.universalDegree τ men ⁻¹' Set.Ioi (Degree.universalDegree ω men (Sum.inl Man.s))

Seymour is five feet tall and three feet wide. Among men ordered as above and measurements up to eighty inches he is taller than he is wide, but restricted to men his 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.

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

def Bale2008.Person.parse? : String → Option Person

A person of the height and width 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

def Bale2008.Man.parse? : String → Option Man

A man by name.

Equations

• Bale2008.Man.parse? "a" = some Bale2008.Man.a
• Bale2008.Man.parse? "b" = some Bale2008.Man.b
• Bale2008.Man.parse? "c" = some Bale2008.Man.c
• Bale2008.Man.parse? "d" = some Bale2008.Man.d
• Bale2008.Man.parse? "e" = some Bale2008.Man.e
• Bale2008.Man.parse? "f" = some Bale2008.Man.f
• Bale2008.Man.parse? "g" = some Bale2008.Man.g
• Bale2008.Man.parse? "h" = some Bale2008.Man.h
• Bale2008.Man.parse? "i" = some Bale2008.Man.i
• Bale2008.Man.parse? "j" = some Bale2008.Man.j
• Bale2008.Man.parse? "k" = some Bale2008.Man.k
• Bale2008.Man.parse? "l" = some Bale2008.Man.l
• Bale2008.Man.parse? "m" = some Bale2008.Man.m
• Bale2008.Man.parse? "n" = some Bale2008.Man.n
• Bale2008.Man.parse? "o" = some Bale2008.Man.o
• Bale2008.Man.parse? "p" = some Bale2008.Man.p
• Bale2008.Man.parse? "q" = some Bale2008.Man.q
• Bale2008.Man.parse? "r" = some Bale2008.Man.r
• Bale2008.Man.parse? "s" = some Bale2008.Man.s
• Bale2008.Man.parse? x✝ = none

def Bale2008.degree? (r : Datum) (who scale : String) : Option ℚ

A row assigns one of its participants a universal degree on one of its scales in the comparison class of its situation, which is the original committee, the people with the measurements up to eighty inches, or the men.

Equations

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

def Bale2008.truth? (r : Datum) : Option Bool

The truth value a row reports.

Equations

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

theorem Bale2008.rows_truth (r : Datum) : r ∈ Examples.all → (r.feature? "model").isSome = true → ∃ 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, since the subject's universal degree exceeds the standard's exactly when the paper says the sentence is true.