Heim (2001): Degree Operators and Scope

Heim asks how far a degree phrase moves at LF, given the max semantics of the comparative, on which -er than t says that the greatest degree of its argument exceeds t, Degree.MaxIn (Ioi t), and a DegP scopes under a quantifier or over it, Degree.LowScope and Degree.HighScope. Over a monotone increasing quantifier on a finite domain the two scopes coincide and under a monotone decreasing one the maximum is undefined, so the exactly-differential and less, whose intervals are not upper sets, are the diagnostic cases: under every girl their high scope is a weaker reading the sentence lacks, which Kennedy's generalization, the Heim–Kennedy constraint Degree.IsHeimKennedy, excludes, while over the intensional verbs both scopes are attested. For the neg-raising verbs the maximum redefined as the greatest lower bound of the false degrees collapses the scopes (negRaising_collapse), and -est, using its complement twice, is the absolute superlative (est_iff_absoluteSuperlative).

Implementation notes

• Quantifiers over individuals and over worlds are the same Quantifier.NP, so the intensional cases of Sections 2.1 and 2.3 are the theorems at a type of worlds.
• A high-scope truth condition carries the definedness presupposition of the maximum as an existence conjunct; the paper's undefined maxima are the negations of those conjuncts.
• The de re and de dicto than-clauses of Section 2.4 are von Stechow's diagnosis and are formalized in Studies/VonStechow1984.lean; the examples are typed in Data/Examples/Heim2001.json.

References

• [Hei01]
• [vS84]
• [Hei99]

Monotone increasing quantifiers

theorem Heim2001.forall_collapse {Entity : Type u_1} {D : Type u_3} [LinearOrder D] [Finite Entity] {girl : Entity → Prop} (hg : ∃ (x : Entity), girl x) (μ : Entity → D) {U : Set D} (hU : IsUpperSet U) : Degree.HighScope (Degree.MaxIn U) (Quantifier.GQ.every girl) (Set.Iic ∘ μ) ↔ Degree.LowScope (Degree.MaxIn U) (Quantifier.GQ.every girl) (Set.Iic ∘ μ)

On a finite domain the two scopes of an upper-interval DegP under every girl coincide, the comparative (10) at Ioi t, the equative (13a) at Ici t, and, at a type of worlds, the necessity operator (16) (Section 2.1).

theorem Heim2001.exists_collapse {Entity : Type u_1} {D : Type u_3} [LinearOrder D] [Finite Entity] (girl : Entity → Prop) (μ : Entity → D) {U : Set D} (hU : IsUpperSet U) : Degree.HighScope (Degree.MaxIn U) (Quantifier.GQ.some girl) (Set.Iic ∘ μ) ↔ Degree.LowScope (Degree.MaxIn U) (Quantifier.GQ.some girl) (Set.Iic ∘ μ)

Likewise under some girl, (12), (13b), and the possibility operator (15b).

Monotone decreasing and non-monotone operators

theorem Heim2001.negation_high_undefined {Entity : Type u_1} {D : Type u_3} [LinearOrder D] [NoMaxOrder D] (μ : Entity → D) (a : Entity) : ¬∃ (m : D), IsGreatest (Degree.scopeDegrees (fun (S : Entity → Prop) => ¬S a) (Set.Iic ∘ μ)) m

The degrees to which Mary is not tall have no maximum (17c).

theorem Heim2001.atMost_high_undefined {Entity : Type u_1} {D : Type u_3} [LinearOrder D] [Fintype Entity] [NoMaxOrder D] (girl : Entity → Prop) (μ : Entity → D) : ¬∃ (m : D), IsGreatest (Degree.scopeDegrees (Quantifier.GQ.atMost 2 girl) (Set.Iic ∘ μ)) m

The degrees to which at most two girls are tall have no maximum (18c).

theorem Heim2001.exactly_high_atLeast {Entity : Type u_1} {D : Type u_3} [LinearOrder D] [Fintype Entity] {girl : Entity → Prop} {μ : Entity → D} {m : D} (h : IsGreatest (Degree.scopeDegrees (Quantifier.GQ.exactly 2 girl) (Set.Iic ∘ μ)) m) : IsGreatest (Degree.scopeDegrees (Quantifier.GQ.atLeast 2 girl) (Set.Iic ∘ μ)) m

The maximal degree to which exactly two girls are tall, when defined, is the maximal degree to which at least two are, so the high scope (20c) means at least two girls are taller than 5 feet (20).

Exactly-differentials and less

theorem Heim2001.forall_high_of_low {Entity : Type u_1} {D : Type u_3} [LinearOrder D] [Finite Entity] {girl : Entity → Prop} (hg : ∃ (x : Entity), girl x) (μ : Entity → D) (U : Set D) : Degree.LowScope (Degree.MaxIn U) (Quantifier.GQ.every girl) (Set.Iic ∘ μ) → Degree.HighScope (Degree.MaxIn U) (Quantifier.GQ.every girl) (Set.Iic ∘ μ)

Under every girl the low scope entails the high one at every interval, the shortest girl attaining the maximum, so (22c) is weaker than (22b) at {t}, (24c) than (24b) at Iio t, and at a type of worlds (28c) than (28b) and (30c) than (30b).

theorem Heim2001.exists_low_of_high {Entity : Type u_1} {D : Type u_3} [LinearOrder D] (girl : Entity → Prop) (μ : Entity → D) (U : Set D) : Degree.HighScope (Degree.MaxIn U) (Quantifier.GQ.some girl) (Set.Iic ∘ μ) → Degree.LowScope (Degree.MaxIn U) (Quantifier.GQ.some girl) (Set.Iic ∘ μ)

Under some girl the high scope entails the low one at every interval, the tallest girl being a witness, so (21c) is stronger than (21b), and at a type of worlds (29c) than (29b) and (31c) than (31b).

theorem Heim2001.exactly_high_not_low : Degree.HighScope (Degree.MaxIn {49}) (Quantifier.GQ.every fun (x : Fin 2) => True) (Set.Iic ∘ ![49, 50]) ∧ ¬Degree.LowScope (Degree.MaxIn {49}) (Quantifier.GQ.every fun (x : Fin 2) => True) (Set.Iic ∘ ![49, 50])

The high scope is true and the low scope false when the shortest girl is exactly 4'1'' and another is taller, so every girl is exactly 1'' taller than that is false there and (22c) is no reading of it (22).

theorem Heim2001.less_high_not_low : Degree.HighScope (Degree.MaxIn (Set.Iio 50)) (Quantifier.GQ.every fun (x : Fin 2) => True) (Set.Iic ∘ ![49, 50]) ∧ ¬Degree.LowScope (Degree.MaxIn (Set.Iio 50)) (Quantifier.GQ.every fun (x : Fin 2) => True) (Set.Iic ∘ ![49, 50])

The high scope of every girl is less tall than that says only that the shortest girl is, and is true where the sentence is false (24).

Intensional verbs

theorem Heim2001.required_less {W : Type u_2} {D : Type u_3} [LinearOrder D] [Finite W] {Acc : Set W} (hAcc : Acc.Nonempty) (ℓ : W → D) (t : D) : Degree.HighScope (Degree.MaxIn (Set.Iio t)) (Quantifier.GQ.every fun (x : W) => x ∈ Acc) (Set.Iic ∘ ℓ) ↔ ¬Quantifier.GQ.every (fun (x : W) => x ∈ Acc) fun (w : W) => t ≤ ℓ w

The paper is required to be less long than t with the DegP over required says that the paper is not required to be as long as t (30c).

theorem Heim2001.allowed_less {W : Type u_2} {D : Type u_3} [LinearOrder D] [Finite W] {Acc : Set W} (hAcc : Acc.Nonempty) (ℓ : W → D) (t : D) : Degree.HighScope (Degree.MaxIn (Set.Iio t)) (Quantifier.GQ.some fun (x : W) => x ∈ Acc) (Set.Iic ∘ ℓ) ↔ ¬Quantifier.GQ.some (fun (x : W) => x ∈ Acc) fun (w : W) => t ≤ ℓ w

The paper is allowed to be less long than t with the DegP over allowed says that the paper is not allowed to be as long as t (31c).

theorem Heim2001.negRaising_collapse {W : Type u_2} {D : Type u_3} [LinearOrder D] [Finite W] [DenselyOrdered D] {Des : Set W} (hDes : Des.Nonempty) (ℓ : W → D) (t : D) : (∃ m ∈ Set.Iio t, IsGLB (Degree.scopeDegrees (Quantifier.GQ.no fun (x : W) => x ∈ Des) (Set.Iic ∘ ℓ)) m) ↔ Degree.LowScope (Degree.MaxIn (Set.Iio t)) (Quantifier.GQ.every fun (x : W) => x ∈ Des) (Set.Iic ∘ ℓ)

With the maximum of (35), I want the paper to be less long than t with the DegP over want says that the greatest lower bound of the lengths the paper is desired not to have, those no desired world reaches, is below t, which is the low-scope reading (36a).

The superlative

def Heim2001.est {Entity : Type u_1} {D : Type u_3} [LinearOrder D] (μ : Entity → D) (C : Set Entity) (x : Entity) : Prop

The entry for -est (59a), λx. max{d : R(x, d)} > max{d : ∃y ≠ x. R(y, d)}, over a monotone adjective and a comparison class C is the max-quantified comparative of x against the other members.

Equations

• Heim2001.est μ C x = Degree.MaxComparative Degree.Comparison.gt (fun (x_1 : Entity) => x_1 = x) (fun (y : Entity) => y ∈ C ∧ y ≠ x) μ

theorem Heim2001.est_iff_absoluteSuperlative {Entity : Type u_1} {D : Type u_3} [LinearOrder D] [Finite Entity] {μ : Entity → D} {C : Set Entity} {x : Entity} (hx : x ∈ C) (hC : ∃ y ∈ C, y ≠ x) : est μ C x ↔ Degree.AbsoluteSuperlative μ C x

Over a comparison class with someone else in it, -est is the absolute superlative (59).