The semantics of degree

Cresswell's degree of comparison is a point paired with the ordering of its scale, and er than holds of two degree properties when both are instantiated and every degree of the first exceeds every degree of the second on their common scale, so a comparative across scales is anomalous and a disjoined standard is compared universally. Mass nouns and plurals carry degrees of volume and of number through the totality operator, degrees need no units since any comparison relation yields a scale by quotienting, and the counterfactual shorter than he is compares heights across worlds.

We take degrees on a family of scales to be mathlib's disjoint sum of the scales' orders and prove the same-scale restriction, the universal reading of disjoined standards, the reduction of the totality comparatives to volumes and cardinalities, the synonymy of all and every given that there are men, the comparative on constructed degrees, and the counterfactual through a Stalnaker selection function.

Implementation notes

• The plural is read as in (49), a nonempty set of things satisfying the noun with its cardinality; as printed, (3.6) fixes the set to all of them, on which (54) would require the set of all men to walk.

References

• M. J. Cresswell, The semantics of degree (1976)
• R. C. Stalnaker, A theory of conditionals (1968)

Comparison of degree properties (2.3), (2.7)

def Cresswell1976.ErThan {D : Type u_1} [LT D] (ω ω' : Set D) : Prop

Er than holds of two properties of degrees when both are instantiated and every degree of the first exceeds every degree of the second (2.3).

Equations

• Cresswell1976.ErThan ω ω' = (ω.Nonempty ∧ ω'.Nonempty ∧ ∀ a ∈ ω, ∀ b ∈ ω', b < a)

def Cresswell1976.AsAs {D : Type u_1} [LT D] (ω ω' : Set D) : Prop

As as holds when every degree of the first exceeds or equals every degree of the second (2.7).

Equations

• Cresswell1976.AsAs ω ω' = (ω.Nonempty ∧ ω'.Nonempty ∧ ∀ a ∈ ω, ∀ b ∈ ω', b < a ∨ b = a)

def Cresswell1976.Exactly {D : Type u_1} (ω ω' : Set D) : Prop

Exactly as as holds when the degrees coincide (2.7).

Equations

• Cresswell1976.Exactly ω ω' = (ω.Nonempty ∧ ω'.Nonempty ∧ ∀ a ∈ ω, ∀ b ∈ ω', a = b)

theorem Cresswell1976.ErThan.asAs {D : Type u_1} [LT D] {ω ω' : Set D} (h : ErThan ω ω') : AsAs ω ω'

theorem Cresswell1976.Exactly.asAs {D : Type u_1} [LT D] {ω ω' : Set D} (h : Exactly ω ω') : AsAs ω ω'

@[simp]

theorem Cresswell1976.erThan_singleton {D : Type u_1} [LT D] {a b : D} : ErThan {a} {b} ↔ b < a

A phrasal comparative compares its two degrees ((13), (18)).

theorem Cresswell1976.erThan_singleton_toDual {D : Type u_1} [LT D] {a b : D} : ErThan {OrderDual.toDual a} {OrderDual.toDual b} ↔ a < b

@[simp]

theorem Cresswell1976.asAs_singleton {D : Type u_1} [LT D] {a b : D} : AsAs {a} {b} ↔ b < a ∨ b = a

@[simp]

theorem Cresswell1976.exactly_singleton {D : Type u_1} {a b : D} : Exactly {a} {b} ↔ a = b

theorem Cresswell1976.erThan_union {D : Type u_1} [LT D] {ω ω₁ ω₂ : Set D} (h₁ : ω₁.Nonempty) (h₂ : ω₂.Nonempty) : ErThan ω (ω₁ ∪ ω₂) ↔ ErThan ω ω₁ ∧ ErThan ω ω₂

A disjoined standard is compared universally, so taller than Arabella or Clarissa is taller than both (footnote 10).

theorem Cresswell1976.erThan_image_toDual {D : Type u_1} [LT D] {ω ω' : Set D} : ErThan (⇑OrderDual.toDual '' ω) (⇑OrderDual.toDual '' ω') ↔ ErThan ω' ω

Reading a scale downward reverses the comparison, so shorter than is taller than with the terms exchanged ((39), (72)).

theorem Cresswell1976.asAs_singleton_iff_le {E : Type u_1} {α : Type u_2} {μ : E → α} {x y : E} [PartialOrder α] : AsAs {μ x} {μ y} ↔ μ y ≤ μ x

On one scale the equative is the weak comparison of the two measures (2.7).

Degrees on a family of scales (2.1)

theorem Cresswell1976.ErThan.fst_eq {ι : Type u_1} {P : ι → Type u_2} [(i : ι) → LT (P i)] {ω ω' : Set ((i : ι) × P i)} (h : ErThan ω ω') {a b : (i : ι) × P i} (ha : a ∈ ω) (hb : b ∈ ω') : a.fst = b.fst

Compared degrees lie on one scale (2.3).

theorem Cresswell1976.not_erThan_of_fst_ne {ι : Type u_1} {P : ι → Type u_2} [(i : ι) → LT (P i)] {ω ω' : Set ((i : ι) × P i)} (h : ∀ a ∈ ω, ∀ b ∈ ω', a.fst ≠ b.fst) : ¬ErThan ω ω'

Degree properties on distinct scales are never compared, which is the anomaly of (23), (65) and (69).

theorem Cresswell1976.erThan_image_sigmaMk {ι : Type u_1} {P : ι → Type u_2} [(i : ι) → LT (P i)] {i : ι} {ω ω' : Set (P i)} : ErThan (Sigma.mk i '' ω) (Sigma.mk i '' ω') ↔ ErThan ω ω'

On one scale the comparative is the scale's.

The scales of the paper's comparatives

inductive Cresswell1976.Scale : Type

The examples compare on spatial and temporal distances, volumes, the numbers of (3.6), and the unit-free scales of §4.

• distance : Scale
• time : Scale
• volume : Scale
• number : Scale
• cleverness : Scale
• beauty : Scale

@[instance_reducible]

instance Cresswell1976.instDecidableEqScale : DecidableEq Scale

Equations

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

@[reducible, inline]

abbrev Cresswell1976.DirectedScale : Type

A directed scale is the relation of a degree read upward or, for short, downward (2.1).

Equations

• Cresswell1976.DirectedScale = (Cresswell1976.Scale × Polarity)

def Cresswell1976.DirectedScale.ofLabel : String → Option DirectedScale

The scale a paperFeatures label names.

Equations

• Cresswell1976.DirectedScale.ofLabel "distance" = some (Cresswell1976.Scale.distance, Polarity.positive)
• Cresswell1976.DirectedScale.ofLabel "distanceDownward" = some (Cresswell1976.Scale.distance, Polarity.negative)
• Cresswell1976.DirectedScale.ofLabel "time" = some (Cresswell1976.Scale.time, Polarity.positive)
• Cresswell1976.DirectedScale.ofLabel "volume" = some (Cresswell1976.Scale.volume, Polarity.positive)
• Cresswell1976.DirectedScale.ofLabel "number" = some (Cresswell1976.Scale.number, Polarity.positive)
• Cresswell1976.DirectedScale.ofLabel "cleverness" = some (Cresswell1976.Scale.cleverness, Polarity.positive)
• Cresswell1976.DirectedScale.ofLabel "beauty" = some (Cresswell1976.Scale.beauty, Polarity.positive)
• Cresswell1976.DirectedScale.ofLabel x✝ = none

def Cresswell1976.datum (e : Datum) : Option (DirectedScale × DirectedScale × Judgment)

The scales of an example's two terms and its judgment.

Equations

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

def Cresswell1976.data : List (DirectedScale × DirectedScale × Judgment)

The comparatives whose scales the paper records.

Equations

• Cresswell1976.data = List.filterMap Cresswell1976.datum Cresswell1976.Examples.all

theorem Cresswell1976.scale_ne_of_unacceptable (d : DirectedScale × DirectedScale × Judgment) : d ∈ data → d.2.2 = Judgment.unacceptable → d.1 ≠ d.2.1

The starred comparatives compare distinct scales.

theorem Cresswell1976.not_erThan_of_unacceptable {P : DirectedScale → Type u_1} [(s : DirectedScale) → LT (P s)] {d : DirectedScale × DirectedScale × Judgment} (hd : d ∈ data) (hj : d.2.2 = Judgment.unacceptable) {ω ω' : Set ((s : DirectedScale) × P s)} (hω : ∀ a ∈ ω, a.fst = d.1) (hω' : ∀ b ∈ ω', b.fst = d.2.1) : ¬ErThan ω ω'

Every starred comparative is unsatisfiable, whatever the points of its scales.

Superlatives, mass nouns and plurals ((2.6), §3)

def Cresswell1976.tot {E : Type u_1} {D : Type u_2} [LE D] (ω : E → D → Prop) (ω' : E → Prop) : Set D

Tot gives the degree of the greatest part of whatever satisfies both predicates (3.2).

Equations

• Cresswell1976.tot ω ω' = {u : D | IsGreatest {d : D | ∃ (c : E), ω' c ∧ ω c d} u}

def Cresswell1976.Est {E : Type u_1} {D : Type u_2} [LE D] (ω : E → D → Prop) (a : E) : Prop

Est holds when a bears a unique degree at or above every degree of anything (2.6).

Equations

• Cresswell1976.Est ω a = ∃! b : D, ω a b ∧ b ∈ upperBounds {d : D | ∃ (c : E), ω c d}

theorem Cresswell1976.est_iff {E : Type u_1} {D : Type u_2} [LE D] (μ : E → D) (a : E) : Est (fun (c : E) (d : D) => μ c = d) a ↔ ∀ (c : E), μ c ≤ μ a

The superlative of a measure holds of a greatest value, ties allowed as in (2.6), as in tallest spy (27).

theorem Cresswell1976.tot_eq_singleton {E : Type u_1} {D : Type u_2} [PartialOrder D] {ω : E → D → Prop} {ω' : E → Prop} {u : D} (h : IsGreatest {d : D | ∃ (c : E), ω' c ∧ ω c d} u) : tot ω ω' = {u}

theorem Cresswell1976.erThan_tot_tot {E : Type u_1} {D : Type u_2} [PartialOrder D] {ω : E → D → Prop} {ω' : E → Prop} {E' : Type u_3} {ω₁ : E' → D → Prop} {ω₁' : E' → Prop} {u u₁ : D} (h : IsGreatest {d : D | ∃ (c : E), ω' c ∧ ω c d} u) (h₁ : IsGreatest {d : D | ∃ (c : E'), ω₁' c ∧ ω₁ c d} u₁) : ErThan (tot ω ω') (tot ω₁ ω₁') ↔ u₁ < u

The comparative of two totalities compares their greatest degrees, so more water ebbs than mud flows compares two volumes ((42), (44)).

def Cresswell1976.Pl {E : Type u_1} (noun a : Finset E) (n : ℕ) : Prop

Pl gives a nonempty set of things satisfying the noun, with its cardinality, a positive integer, as degree ((3.6), (49)).

Equations

• Cresswell1976.Pl noun a n = (a ⊆ noun ∧ a.Nonempty ∧ a.card = n)

def Cresswell1976.All {A : Type u_2} {B : Type u_3} (ω : A → B → Prop) (ω' : A → Prop) : Prop

All holds when something satisfies the plural and everything that does satisfies the predicate (3.7).

Equations

• Cresswell1976.All ω ω' = ((∃ (a : A) (b : B), ω a b) ∧ ∀ (a : A), (∃ (b : B), ω a b) → ω' a)

theorem Cresswell1976.tot_pl {E : Type u_1} (noun : Finset E) (pred : E → Prop) [DecidablePred pred] (h : (Finset.filter pred noun).Nonempty) : (tot (Pl noun) fun (a : Finset E) => ∀ x ∈ a, pred x) = {(Finset.filter pred noun).card}

The totality of the sets satisfying a distributive predicate is the number of things satisfying it, so more men walk counts the walking men ((54), (55)).

theorem Cresswell1976.erThan_tot_pl {E : Type u_1} (man bird : Finset E) (walk fly : E → Prop) [DecidablePred walk] [DecidablePred fly] (hw : (Finset.filter walk man).Nonempty) (hf : (Finset.filter fly bird).Nonempty) : ErThan (tot (Pl man) fun (a : Finset E) => ∀ x ∈ a, walk x) (tot (Pl bird) fun (a : Finset E) => ∀ x ∈ a, fly x) ↔ (Finset.filter fly bird).card < (Finset.filter walk man).card

More men walk than birds fly holds when the walking men outnumber the flying birds ((52), (55)).

theorem Cresswell1976.all_pl_iff_forall {E : Type u_1} (noun : Finset E) (pred : E → Prop) : (All (Pl noun) fun (a : Finset E) => ∀ x ∈ a, pred x) ↔ noun.Nonempty ∧ ∀ x ∈ noun, pred x

All men walk and every man walks are synonymous given that there are men, although all takes the plural and every (3.8) the count noun ((56), (57)).

Degrees from comparisons (§4)

theorem Cresswell1976.erThan_singleton_mk {E : Type u_1} (φ : E → E → Prop) (a b : E) : ErThan {⟦a⟧} {⟦b⟧} ↔ φ a b

On the degrees a comparison relation constructs, the comparative is the relation itself, as in Arabella is more beautiful than Clarissa ((62), (4.2)).

Comparison across worlds ((70)–(73))

theorem Cresswell1976.erThan_sel {W : Type u_1} {D : Type u_2} [Preorder D] (s : Conditional.SelectionFunction W) (height : W → D) (smokes : Set W) (w : W) : ErThan {OrderDual.toDual (height (s.sel w smokes))} {OrderDual.toDual (height w)} ↔ height (s.sel w smokes) < height w

If Bill had been a smoker he would be shorter than he is holds when his height at the nearest world where he smokes is below his actual height ((71)).

theorem Cresswell1976.not_erThan_sel_of_mem {W : Type u_1} {D : Type u_2} [Preorder D] (s : Conditional.SelectionFunction W) (height : W → D) (smokes : Set W) (w : W) (hw : w ∈ smokes) : ¬ErThan {OrderDual.toDual (height (s.sel w smokes))} {OrderDual.toDual (height w)}

A smoker would not be shorter than he is, since the nearest world where he smokes is the actual one.