Fox and Hackl (2006): The Universal Density of Measurement

This file formalizes Fox and Hackl's Universal Density of Measurement, the claim that the measurement scales of natural language semantics are dense, and the single mechanism it drives through scalar implicatures, only, degree questions and definite descriptions. Each maximizes a property of degrees with MAXinf, the most informative true degree, which is Dayal's strongest true answer of the degree property (Question.IsStrongestTrueAnswer), and the Constraint on Interval Maximization, not_isExhaustivelyResolvable_of_isNecessarilyOpen, says this fails on a property that necessarily describes an open interval. More than d and not … d are such properties, so they carry no implicature, reject only, and make negative islands; a universal modal closes the interval (isExhaustivelyResolvable_box) and an existential modal does not (not_isGreatest_diamond); at cardinality granularity more than n exhaustifies to exactly n + 1 (moreThan_exact_nat).

Implementation notes

On a strictly antitone family the most informative degree is the greatest true one (Question.isExhaustivelyResolvable_range_iff_isGreatest), so density removes it exactly when the true set is open at its informative end; the downward-monotone cases are the order duals. The paper's example sentences are the rows of Examples.all.

References

• [FH06b]
• [Rul95]
• [BR99a]
• [Day96]
• [Hac00]

Necessarily open properties

def FoxHackl2006.IsNecessarilyOpen {D : Type u_1} {W : Type u_2} [LinearOrder D] (φ : D → Set W) : Prop

A property of degrees necessarily describes an open interval when at every world some degree fails it and every smaller degree satisfies it.

Equations

• FoxHackl2006.IsNecessarilyOpen φ = ∀ (w : W), ∃ (d : D), w ∉ φ d ∧ ∀ d' < d, w ∈ φ d'

@[reducible, inline]

abbrev FoxHackl2006.IsNecessarilyOpenBelow {D : Type u_1} {W : Type u_2} [LinearOrder D] (φ : D → Set W) : Prop

A property is necessarily open from below when at every world some degree fails it and every larger degree satisfies it.

Equations

• FoxHackl2006.IsNecessarilyOpenBelow φ = FoxHackl2006.IsNecessarilyOpen fun (d : Dᵒᵈ) => φ (OrderDual.ofDual d)

theorem FoxHackl2006.not_isExhaustivelyResolvable_of_isNecessarilyOpen {D : Type u_1} {W : Type u_2} [LinearOrder D] [DenselyOrdered D] {φ : D → Set W} (hφ : StrictAnti φ) (hopen : IsNecessarilyOpen φ) (w : W) : ¬Question.IsExhaustivelyResolvable (Set.range φ) w

By the Constraint on Interval Maximization (42), on a dense scale a necessarily open upward-monotone property has no most informative degree.

theorem FoxHackl2006.not_isExhaustivelyResolvable_of_isNecessarilyOpenBelow {D : Type u_1} {W : Type u_2} [LinearOrder D] [DenselyOrdered D] {φ : D → Set W} (hφ : StrictMono φ) (hopen : IsNecessarilyOpenBelow φ) (w : W) : ¬Question.IsExhaustivelyResolvable (Set.range φ) w

(42) for downward-monotone properties.

Implicatures and only

theorem FoxHackl2006.isNecessarilyOpen_gt_over {D : Type u_1} {W : Type u_2} [LinearOrder D] (μ : W → D) : IsNecessarilyOpen fun (x : D) => μ ⁻¹' Set.Ioi x

More than d necessarily describes an open interval, since the true degrees at w are those below the count.

theorem FoxHackl2006.moreThan_not_isExhaustivelyResolvable {D : Type u_1} {W : Type u_2} [LinearOrder D] [DenselyOrdered D] (μ : W → D) (hμ : Function.Surjective μ) (w : W) : ¬Question.IsExhaustivelyResolvable (Set.range fun (x : D) => μ ⁻¹' Set.Ioi x) w

On a dense scale more than d has no most informative degree, so it carries no scalar implicature and rejects only ((2), (5), (7b–c)).

theorem FoxHackl2006.exhAgainst_lt_iff_isStrongestTrueAnswer {D : Type u_1} {W : Type u_2} [LinearOrder D] {φ : D → Set W} (hφ : StrictAnti φ) {i : D} {w : W} : Exhaustification.exhAgainst (fun (x1 x2 : D) => x1 < x2) (fun (x : D) => w ∈ φ x) i ↔ Question.IsStrongestTrueAnswer (Set.range φ) w (φ i)

Exhaustifying a strictly antitone degree property against its stronger members asserts that the prejacent is the most informative true degree, so only and the scalar implicature are MAXinf.

Modal operators

@[reducible, inline]

abbrev FoxHackl2006.requirementBase {D : Type u_1} {W : Type u_2} [LinearOrder D] (φ : D → Set W) (a : D) : SetRel W W

The deontic modal base whose only requirement is φ a is the set of worlds where φ holds of some degree above a.

Equations

• FoxHackl2006.requirementBase φ a = {p : W × W | ∃ (d : D), a < d ∧ p.2 ∈ φ d}

theorem FoxHackl2006.box_eq_Iic {D : Type u_1} {W : Type u_2} [LinearOrder D] [DenselyOrdered D] {φ : D → Set W} (hφ : StrictAnti φ) (a : D) (w : W) : {d : D | w ∈ (requirementBase φ a).core (φ d)} = Set.Iic a

(46) Under requirementBase φ a, required to φ d describes the closed interval Iic a.

theorem FoxHackl2006.isExhaustivelyResolvable_box {D : Type u_1} {W : Type u_2} [LinearOrder D] [DenselyOrdered D] {φ : D → Set W} (hφ : StrictAnti φ) (a : D) (w : W) : Question.IsExhaustivelyResolvable (Set.range fun (d : D) => (requirementBase φ a).core (φ d)) w

A universal modal closes the interval, so required to φ more than d has a most informative degree, a itself ((13), (46)).

theorem FoxHackl2006.not_isGreatest_diamond {D : Type u_1} {W : Type u_2} [LinearOrder D] [DenselyOrdered D] {φ : D → Set W} (hφ : StrictAnti φ) (hopen : IsNecessarilyOpen φ) (R : SetRel W W) (w : W) : ¬∃ (m : D), IsGreatest {d : D | w ∈ R.preimage (φ d)} m

No existential modal closes the interval, since the true degrees of allowed to φ d have no greatest element, so the constraint still applies ((14), (47)).

Negative islands

theorem FoxHackl2006.isNecessarilyOpenBelow_lt_over {D : Type u_1} {W : Type u_2} [LinearOrder D] (μ : W → D) : IsNecessarilyOpenBelow fun (x : D) => μ ⁻¹' Set.Iio x

Not … d is necessarily open from below, since the true degrees are those above the measure.

theorem FoxHackl2006.negation_not_isExhaustivelyResolvable {D : Type u_1} {W : Type u_2} [LinearOrder D] [DenselyOrdered D] (μ : W → D) (hμ : Function.Surjective μ) (w : W) : ¬Question.IsExhaustivelyResolvable (Set.range fun (x : D) => μ ⁻¹' Set.Iio x) w

On a dense scale the negated degree property has no most informative (least true) degree, so a degree question or definite description over it is undefined ((16), (19a), (25)).

theorem FoxHackl2006.isExhaustivelyResolvable_box_below {D : Type u_1} {W : Type u_2} [LinearOrder D] [DenselyOrdered D] {φ : D → Set W} (hφ : StrictMono φ) (a : D) (w : W) : Question.IsExhaustivelyResolvable (Set.range fun (d : D) => SetRel.core {p : W × W | ∃ d < a, p.2 ∈ φ d} (φ d)) w

In required not to φ d a universal modal over a downward-monotone property closes the interval from below ((27b), (28a), (29a)).

theorem FoxHackl2006.not_isLeast_diamond {D : Type u_1} {W : Type u_2} [LinearOrder D] [DenselyOrdered D] {φ : D → Set W} (hφ : StrictMono φ) (hopen : IsNecessarilyOpenBelow φ) (R : SetRel W W) (w : W) : ¬∃ (m : D), IsLeast {d : D | w ∈ R.preimage (φ d)} m

Allowed not to φ d stays open from below ((28b), (29b), (47)).

Cardinality as a level of granularity

theorem FoxHackl2006.moreThan_exact_nat {W : Type u_2} (μ : W → ℕ) (hμ : Function.Surjective μ) (m : ℕ) (w : W) : Question.IsStrongestTrueAnswer (Set.range fun (x : ℕ) => μ ⁻¹' Set.Ioi x) w (μ ⁻¹' Set.Ioi m) ↔ μ w = m + 1

At cardinality granularity more than n is at least n + 1, whose most informative degree is the count, so only more than 15F means exactly 16 ((73)–(75)).