Granularity-Sensitive Degree Semantics @cite{thomas-deo-2020} #
Thomas, W. & Deo, A. (2020). The interaction of just with modified scalar predicates. Sinn und Bedeutung 24, vol. 2, pp. 354–372.
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
@cite{sauerland-stateva-2011} 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
- Semantics.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)
Equative at granularity interval: "as Adj as d_c".
Paper eq. (45): ⟦as...as d_c⟧^g = λGλx.∃d[d > inf(g(d_c)) ∧ G(d)(x)].
For upward-monotone G (e.g., tall, where G(d)(x) iff μ(x) ≥ d), the existential reduces to μ_x > inf(g(d_c)).
Equations
- Semantics.Degree.Granularity.eqAt gi μ_x = (μ_x > gi.lo)
Instances For
Comparative at granularity interval: "Adj-er than d_c".
Paper eq. (49): ⟦er/more than d_c⟧^g = λGλx.∃d[d > sup(g(d_c)) ∧ G(d)(x)].
For upward-monotone G, the existential reduces to μ_x > sup(g(d_c)).
Equations
- Semantics.Degree.Granularity.compAt gi μ_x = (μ_x > gi.hi)
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).
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).
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
- Semantics.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
- Semantics.Degree.Granularity.approxJust p finest μ_x = (p finest μ_x ∧ ∀ (g : G), p g μ_x → Semantics.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 (@cite{deo-thomas-2025} §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.
If ε₁ divides ε₂, then knowing ⌊d/ε₁⌋ determines ⌊d/ε₂⌋.
This is the number-theoretic core of the granularity–refinement
bridge: finer grain indices determine coarser grain indices.
Uses Nat.div_div_eq_div_mul: a / b / c = a / (b * c).
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.
@cite{deo-thomas-2025} 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
- Semantics.Degree.Granularity.granQUD n ε = QUD.ofProject fun (w : Fin n) => ↑w / ε
Instances For
Finer granularity induces partition refinement.
@cite{deo-thomas-2025} §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.