Morzycki (2009): Degree Modification of Gradable Nouns

This file formalizes Morzycki's account of the degree readings of size adjectives, big idiot as a very idiotic person. A gradable noun denotes a measure function from individuals to degrees, and its positive form holds of the individuals that reach the noun's standard (pos). A size adjective in a degree reading is the argument of an adnominal degree head, the nominal counterpart of the head that combines an adjective with a measure phrase (meas): the individual's degree must reach the least degree the size adjective is true of, and also the noun's standard (measN). The resulting predicate is the positive form with the standard raised to that least degree (measN_eq_pos_sup).

The Bigness Generalization, that only adjectives of bigness license degree readings, follows. Antonyms measure along oppositely ordered scales, so the bottom of the noun's scale counts as small wherever the standard of smallness lies, the least small degree is the bottom, and small idiot is idiot (measN_small), whereas the least big degree properly raises a lower standard (measN_ssubset_pos). The degree head complete requires the maximum of the noun's scale and so combines only with nouns whose scales have one (hasMax_of_complete_nonempty).

Implementation notes

The scale of a gradable noun is the whole degree type, so the restriction of the least degree to the noun's scale is left implicit. The Position Generalization, that degree readings arise only attributively, is imposed by the syntax of the nominal degree projection and is not represented, and neither are the degree heads real, true, total and absolute.

References

• [Mor09]
• [KMcN05]

Positive forms and degree heads

@[reducible, inline]

abbrev Morzycki2009.pos {E : Type u_1} {D : Type u_2} [Preorder D] (g : E → D) (s : D) : Set E

The positive form of a gradable predicate with measure function g holds of the individuals whose degree reaches the standard s.

Equations

• Morzycki2009.pos g s = g ⁻¹' Set.Ici s

def Morzycki2009.meas {E : Type u_1} {D : Type u_2} [Preorder D] (g : E → D) (m : Set D) : Set E

The head that combines a gradable predicate with a measure phrase m, a property of degrees, requires the individual's degree to reach the least degree that m is true of, as in six feet tall.

Equations

• Morzycki2009.meas g m = {x : E | ∃ (d : D), IsLeast m d ∧ d ≤ g x}

def Morzycki2009.measN {E : Type u_1} {D : Type u_2} [Preorder D] (g : E → D) (s : D) (m : Set D) : Set E

The adnominal head that combines a gradable noun with a size adjective requires in addition that the noun's standard be reached, since a big idiot is an idiot while someone six feet tall need not be tall.

Equations

• Morzycki2009.measN g s m = Morzycki2009.meas g m ∩ Morzycki2009.pos g s

def Morzycki2009.complete {E : Type u_1} {D : Type u_2} [Preorder D] (g : E → D) : Set E

The degree head complete holds of the individuals at the maximum of the scale.

Equations

• Morzycki2009.complete g = {x : E | IsTop (g x)}

theorem Morzycki2009.mem_pos {E : Type u_1} {D : Type u_2} [Preorder D] {g : E → D} {s : D} {x : E} : x ∈ pos g s ↔ s ≤ g x

theorem Morzycki2009.mem_meas_iff {E : Type u_1} {D : Type u_2} [Preorder D] {g : E → D} {d : D} {m : Set D} {x : E} (hd : IsLeast m d) : x ∈ meas g m ↔ d ≤ g x

theorem Morzycki2009.meas_eq_preimage {E : Type u_1} {D : Type u_2} [Preorder D] {g : E → D} {d : D} {m : Set D} (hm : IsUpperSet m) (hd : IsLeast m d) : meas g m = g ⁻¹' m

The least degree can be dispensed with when the measure phrase is itself an 'at least' property of degrees.

theorem Morzycki2009.measN_subset_pos {E : Type u_1} {D : Type u_2} [Preorder D] {g : E → D} {s : D} {m : Set D} : measN g s m ⊆ pos g s

A big idiot is an idiot.

theorem Morzycki2009.complete_subset_pos {E : Type u_1} {D : Type u_2} [Preorder D] {g : E → D} {s : D} : complete g ⊆ pos g s

Whoever is at the maximum of the scale reaches every standard.

theorem Morzycki2009.hasMax_of_complete_nonempty {E : Type u_1} {D : Type u_2} [Preorder D] {g : E → D} (h : (complete g).Nonempty) : (Degree.Boundedness.ofOrder D).HasMax

The degree head complete combines only with nouns whose scales have a maximum.

The Bigness Generalization

theorem Morzycki2009.measN_eq_pos_sup {E : Type u_1} {D : Type u_2} [SemilatticeSup D] {g : E → D} {s d : D} {m : Set D} (hd : IsLeast m d) : measN g s m = pos g (s ⊔ d)

A size adjective in a degree reading raises the noun's standard to the least degree the adjective is true of.

theorem Morzycki2009.measN_eq_pos_of_bot_mem {E : Type u_1} {D : Type u_2} [SemilatticeSup D] {g : E → D} {s : D} {m : Set D} [OrderBot D] (h : ⊥ ∈ m) : measN g s m = pos g s

The size adjective is vacuous when the bottom of the scale satisfies it.

theorem Morzycki2009.measN_small {E : Type u_1} {D : Type u_2} {S : Type u_3} [SemilatticeSup D] {g : E → D} {s : D} [OrderBot D] [Preorder S] {big : D → S} (hbig : Monotone big) {θ : Sᵒᵈ} (h : (pos (⇑OrderDual.toDual ∘ big) θ).Nonempty) : measN g s (pos (⇑OrderDual.toDual ∘ big) θ) = pos g s

Smallness is vacuous. An adjective of smallness measures along the reverse of the order its antonym big measures along, so if any degree counts as small then the bottom of the scale does, and small idiot is idiot wherever the standard θ of smallness lies.

theorem Morzycki2009.measN_ssubset_pos {E : Type u_1} {D : Type u_2} [SemilatticeSup D] {g : E → D} {s d : D} {m : Set D} (hd : IsLeast m d) (hsd : s < d) {x : E} (hx : g x = s) : measN g s m ⊂ pos g s

Bigness restricts. When the least big degree lies above the noun's standard, an individual just at the standard is an idiot and not a big idiot.