Documentation

Linglib.Theories.Semantics.Questions.DegreeQuestion

Degree Questions and the Universal Density of Measurement #

@cite{beck-rullmann-1999} @cite{fox-2007} @cite{link-1983} @cite{rullmann-1995} @cite{fox-hackl-2006}

@cite{fox-2007} "The universal density of measurement" (Linguistics and Philosophy 29:537–586).

Core Claim #

Degree questions, definite descriptions, and scalar implicatures all involve the same maximality requirement (Core.Scale.HasMaxInf). When the relevant scale is dense ([DenselyOrdered α]), this requirement interacts with negation and modals to produce systematic acceptability patterns.

The Unification #

Fox & Hackl show that four apparently distinct constructions reduce to HasMaxInf applied to a degree property φ:

ConstructionFormulation
Degree question "How much φ?"HasMaxInf φ w
Definite "the amount that φ"HasMaxInf φ w (@cite{link-1983} maximality)
Only/EXH "only φ"HasMaxInf φ w (OIG, F&H eq. 6)
Implicature of bare "φ"HasMaxInf φ w (covert EXH)

All four fail when HasMaxInf φ w is unsatisfiable — which happens precisely when φ describes an open set on a dense scale (no infimum/supremum).

What This File Formalizes #

The new content beyond Core.Scale (which provides degree properties atLeastDeg, moreThanDeg, etc. and their HasMaxInf/density theorems):

  1. Negative islands: negation of a downward-monotone property on a dense scale yields an open complement with no max⊨ element
  2. Modal obviation: ∀-modals rescue maximality violations, ∃-modals don't
  3. Monotonicity preservation through modals

Degree properties (eqDeg, atLeastDeg, moreThanDeg, atMostDeg, lessThanDeg), their monotonicity, HasMaxInf theorems, Kennedy–F&H bridge, and discrete–dense divergence theorems are in Core.Scale (§ 6 of Core/MeasurementScale.lean).

source
def Semantics.Questions.DegreeQuestion.negatedDegreeProp {α : Type u_1} {W : Type u_2} (φ : α → W → Prop) :
α → W → Prop

The negated degree property: ¬φ(d)(w).

Example: φ(d)(w) = "John weighs ≥ d pounds in w" negated: "John does not weigh ≥ d pounds in w"

Equations
Instances For
    source
    theorem Semantics.Questions.DegreeQuestion.negativeIsland_noAnswer {α : Type u_1} {W : Type u_2} [LinearOrder α] [DenselyOrdered α] (φ : α → W → Prop) (_hMono : Core.Scale.IsDownwardMonotone φ) (w : W) (boundary : α) (hBelow : ∀ d ≤ boundary, φ d w) (hAbove : ∀ (d : α), boundary < d → ¬φ d w) (hWitness : ∀ (a b : α), a < b → ∃ (w' : W), φ a w' ∧ ¬φ b w') :
    ¬Core.Scale.HasMaxInf (negatedDegreeProp φ) w

    Negative island theorem (@cite{fox-2007} §3.3):

    "*How much does John not weigh?" is unacceptable because on a dense scale, the negated set {d | ¬φ(d)(w)} has no maximally informative element.

    Setup: φ is downward monotone (e.g., "weighs ≥ d": smaller thresholds are easier to satisfy). At world w, there is a boundary below which φ holds and above which it fails. Density ensures that for any d in the negated set, there exists d' strictly between the boundary and d — and ¬φ(d) does not entail ¬φ(d'), because in a world where the boundary sits between d' and d, ¬φ(d) holds but ¬φ(d') fails.

    The hWitness hypothesis plays the role of hSurj in moreThan_noMaxInf: it guarantees enough worlds exist to separate degrees. For the concrete case φ = atLeastDeg μ, this follows from surjectivity of μ.

    source
    def Semantics.Questions.DegreeQuestion.universalModalProp {α : Type u_1} {W : Type u_2} (φ : α → W → Prop) (R : W → W → Prop) :
    α → W → Prop

    Degree property under a universal modal (required, certain, have to): □φ(d)(w) := ∀w' ∈ R(w). φ(d)(w')

    @cite{fox-2007} exx. (13)–(14): the negation ¬□φ = ∃w'. ¬φ(d)(w') can have a max⊨ element even on dense scales, because two ∃-claims about different d can use different witness worlds — so neither entails the other, and maximality is achievable.

    Equations
    Instances For
      source
      def Semantics.Questions.DegreeQuestion.existentialModalProp {α : Type u_1} {W : Type u_2} (φ : α → W → Prop) (R : W → W → Prop) :
      α → W → Prop

      Degree property under an existential modal (allowed, possible, can): ◇φ(d)(w) := ∃w' ∈ R(w). φ(d)(w')

      Equations
      Instances For
        source
        theorem Semantics.Questions.DegreeQuestion.universalModal_preserves_upMono {α : Type u_1} {W : Type u_2} [LinearOrder α] (φ : α → W → Prop) (R : W → W → Prop) (hMono : Core.Scale.IsUpwardMonotone φ) :
        Core.Scale.IsUpwardMonotone (universalModalProp φ R)

        ∀-modal preserves upward monotonicity.

        source
        theorem Semantics.Questions.DegreeQuestion.existentialModal_preserves_upMono {α : Type u_1} {W : Type u_2} [LinearOrder α] (φ : α → W → Prop) (R : W → W → Prop) (hMono : Core.Scale.IsUpwardMonotone φ) :
        Core.Scale.IsUpwardMonotone (existentialModalProp φ R)

        ∃-modal preserves upward monotonicity.

        source
        def Semantics.Questions.DegreeQuestion.obviatesMaxViolation :
        Core.Modality.ModalForce → Bool

        Modal obviation (@cite{fox-2007} §§2.3, 3.4, 4.2): ∀-modals can circumvent maximality violations; ∃-modals cannot.

        • ¬(∀w'. φ(d)(w')) = ∃w'. ¬φ(d)(w') — different d can use different witness worlds, so the complement can be a closed set with a maximum.
        • ¬(∃w'. φ(d)(w')) = ∀w'. ¬φ(d)(w') — still yields a downward-monotone negated set with no minimum on dense scales.

        Examples:

        • "You're only required to read more than 30 books" ✓
        • "*You're only allowed to smoke more than 30 cigarettes" ✗
        Equations
        Instances For
          source
          theorem Semantics.Questions.DegreeQuestion.necessity_obviates :
          obviatesMaxViolation Core.Modality.ModalForce.necessity = true
          source
          theorem Semantics.Questions.DegreeQuestion.weakNecessity_obviates :
          obviatesMaxViolation Core.Modality.ModalForce.weakNecessity = true
          source
          theorem Semantics.Questions.DegreeQuestion.possibility_fails :
          obviatesMaxViolation Core.Modality.ModalForce.possibility = false