Granularity-Sensitive Degree Semantics [TD20] #
The underlying granularity apparatus — granularity functions partitioning a scale into equal-width intervals and the finer/coarser ordering — is [SS11]'s (their (15)–(16)), following [Kri07a]; [TD20]'s contributions are the granularity-level convenience g(d) = (d − ε, d + ε) (their (43)) and the semantics of approximative just (their (44)).
Overview #
A granularity level maps each degree d on a scale to an open interval g(d) = (d − ε, d + ε) of width 2ε (the "grain", eq. 43). Equatives compare μ_x against the interval's infimum (eq. 45); comparatives compare against the supremum (eq. 49). Both use strict >.
Since the infimum and supremum move in opposite directions as ε varies, the entailment patterns reverse:
- Finer grain (smaller ε) → larger infimum → stronger equative
- Finer grain (smaller ε) → smaller supremum → weaker comparative
This reversal explains why approximative just yields different readings:
- just as tall as ≈ "exactly" (negative component vacuous)
- just taller than ≈ "barely" (negative component substantive)
Structure #
- § 1: Granularity intervals (eq. 43), construction from ε (eqs. 40–42), and degree morphology (eqs. 45, 49).
- § 2: Entailment reversal — from interval endpoint monotonicity.
- § 3: Approximative just (eq. 44) — vacuous vs substantive negative component derived from the reversal.
A granularity interval: the open interval (lo, hi) around a degree.
Paper eq. (43): g(d) = (d − ε, d + ε) for non-endpoint d. Endpoints are handled asymmetrically:
- g(min(S)) = (min(S), min(S) + ε)
- g(max(S)) = (max(S) − ε, max(S))
- lo : D
Infimum of the grain cell — used by equatives (eq. 45).
- hi : D
Supremum of the grain cell — used by comparatives (eq. 49).
Instances For
[SS11] granularity framework #
Eqs. (40a-c) define the properties of a granularity function γ:
- (40a) s ∈ γ(s) — every degree is in its own cell
- (40b) γ(s) is an interval — (already guaranteed by
GranInterval) - (40c) |γ(s)| = |γ(s')| for all s, s' — all cells have equal width (guaranteed by parametric construction from ε)
Eq. (41): γ is finer than γ' iff cells of γ are strictly narrower. Eq. (42): The concrete construction γ(d) = (d − ε, d + ε).
Eq. (42): Construct a granularity interval from grain size ε.
g(d) = (d − ε, d + ε) — the open interval of width 2ε around d.
(Eq. 43 refines this for scale endpoints; see GranInterval docstring.)
Equations
- Degree.Granularity.mkGranInterval ε d = { lo := d - ε, hi := d + ε }
Instances For
Eq. (40a): d ∈ g(d) for positive grain — every degree is in the interior of its own cell. For open interval (lo, hi): lo < d < hi.
Eq. (41): Finer granularity → narrower intervals → containment. If ε₁ ≤ ε₂, then g_{ε₁}(d) ⊆ g_{ε₂}(d):
- lo: d − ε₂ ≤ d − ε₁ (finer has larger infimum)
- hi: d + ε₁ ≤ d + ε₂ (finer has smaller supremum)
Granularity selection ([SS11] (18)–(19), (41)) #
A context supplies a set of available granularities; scalar approximators
reset it ([SS11] (18)–(19)): exactly to the finest,
approximately to the coarsest. With uniform-width granularities the
finer-than order (their (41)) is width comparison, so selection is
Finset.min'/max'. Resetting leaves a singleton, on which any further
reset is vacuous — the engine of approximator-stacking oddity
(their §6.3.5).
The finest available grain width — the reset target of exactly ([SS11] (19a)).
Equations
- Degree.Granularity.finestWidth 𝒢 h𝒢 = 𝒢.min' h𝒢
Instances For
The coarsest available grain width — the reset target of approximately ([SS11] (19b)).
Equations
- Degree.Granularity.coarsestWidth 𝒢 h𝒢 = 𝒢.max' h𝒢
Instances For
The central observation (§4.2) #
Equatives and comparatives use opposite ends of the same interval.
Since > is anti-monotone in its right argument (lower threshold →
easier to exceed), the entailment direction reverses:
- Equatives use
lo = d_c − ε, which decreases as ε grows. Lower bar → weaker claim. So fine ⊢ coarse. - Comparatives use
hi = d_c + ε, which increases as ε grows. Higher bar → stronger claim. So coarse ⊢ fine.
The proofs are one-liners: transitivity of < and ≤.
Equatives: finer grain (larger lo) entails coarser grain (smaller lo).
The equative "as Adj as d_c" (eq. 45) at grain cell gi, for
upward-monotone G, reduces to μ_x > gi.lo (the cell's infimum).
If μ_x exceeds the fine-grain infimum, it a fortiori exceeds the
coarse-grain infimum (which is smaller).
Comparatives: coarser grain (larger hi) entails finer grain (smaller hi).
The comparative "Adj-er than d_c" (eq. 49) at grain cell gi, for
upward-monotone G, reduces to μ_x > gi.hi (the cell's supremum).
If μ_x exceeds the coarse-grain supremum, it a fortiori exceeds the
fine-grain supremum (which is smaller).
Approximative just #
Paper eq. (44): ⟦just⟧ = λp λw. p^{g_finest}(w) ∧ ∀g ∈ 𝒢[p^g(w) → p^{g_finest} ≥_S p^g]
Generic over any grain type G and degree type D.
Propositional strength (paper's ≥_S, footnote 10): p at g₁ is at least as strong as p at g₂ iff g₁-truth entails g₂-truth for all degree values.
Paper: p^{g₁} ≥_S p^{g₂} ≡ ∀w[p^{g₁}(w) → p^{g₂}(w)].
Equations
- Degree.Granularity.atLeastAsStrong p g₁ g₂ = ∀ (μ_x : D), p g₁ μ_x → p g₂ μ_x
Instances For
Approximative just (paper eq. 44).
Positive component: the prejacent holds at the finest grain. Negative component: at every grain where the prejacent holds, the finest-grain version is at least as strong.
The paper restricts quantification to a finite contextual set 𝒢. We quantify over all G for simplicity; the structural results (vacuous/substantive) hold either way.
Equations
- Degree.Granularity.approxJust p finest μ_x = (p finest μ_x ∧ ∀ (g : G), p g μ_x → Degree.Granularity.atLeastAsStrong p finest g)
Instances For
Equative prediction: if the finest grain is the strongest for p, then just's negative component is vacuous — just adds nothing. "Just as tall as" ≈ "exactly as tall as".
This holds for equatives because eq_fine_entails_coarse shows
the finest equative (largest lo) entails all coarser equatives.
Comparative prediction: if the finest grain is NOT the strongest at some coarser grain g, then just rules out g. "Just taller than d_c" entails "not taller at grain g".
This holds for comparatives because comp_coarse_entails_fine
shows the finest comparative (smallest hi) does NOT entail
coarser comparatives (larger hi).
Grain width → partition → question width #
The degree-level infrastructure above handles what happens within a grain cell (equatives compare against infimum, comparatives against supremum). This section connects to the question level: how grain width determines a partition on the scale, and how finer grains produce wider questions ([DT25] §3.1.2–3.2).
The key chain:
- Grain width ε induces a partition via ⌊d/ε⌋ (integer division)
- If ε₁ ∣ ε₂, the ε₁-partition refines the ε₂-partition
- Partition refinement implies question width (
refinement_implies_wider)
The first two steps live here; the third is composed in the study file
since it requires toIssue from inquisitive semantics.
A granularity QUD on Fin n, parameterized by grain width ε.
Maps each degree d to grain index ⌊d/ε⌋, inducing a partition where
degrees in the same grain cell are indistinguishable — the ℕ grain
partition (Setoid.ker (· / ε), Core/Algebra/Order/Grain.lean)
restricted to Fin n and packaged as a QUD.
[DT25] definition (22): γ maps each point p to a cell I of a partition such that p ∈ I. For uniform grain width ε on a discrete scale, this is exactly integer division by ε.
Equations
- Degree.Granularity.granQUD n ε = QUD.ofProject fun (w : Fin n) => ↑w / ε
Instances For
Finer granularity induces partition refinement.
[DT25] §3.1.2, (23): if ε₁ divides ε₂ (finer grain fits evenly into coarser grain), then the ε₁-partition refines the ε₂-partition. Every fine cell is contained in exactly one coarse cell.