Compositional "How" — Degree Questions

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

Compositional semantics of degree questions ("how tall is Kim?"), connecting the syntactic structure of degree questions to the maximality-based analysis in Theories/Semantics/Questions/DegreeQuestion.lean.

Compositional Structure

"How tall is Kim?" = [CP [how [DegP d-tall]] [TP Kim is t_d]]

The wh-word "how" is a degree question operator that asks for the degree d such that the matrix clause is true:

⟦how⟧ = λP⟨d,t⟩. ?d. P(d)

In the Hamblin/Karttunen semantics, the answer set is: { p | ∃d. p = λw. height_w(Kim) ≥ d }

The maximally informative answer is the one with d = height(Kim) (@cite{fox-2007}: max⊨ applied to the answer set).

Bridge to Fox & Hackl

Theories/Semantics/Questions/DegreeQuestion.lean provides:

• The UDM (universal density of measurement)
• Negative island analysis (density blocks max⊨ under negation)
• Modal obviation (universal modal rescues max⊨)

This module provides the compositional structure that feeds into that analysis.

def Semantics.Degree.DegreeQuestion.answerSet {W : Type u_1} {D : Type u_2} [Preorder D] (μ : W → D) : Set (W → Prop)

The answer set of a degree question: the set of propositions of the form "μ(x) ≥ d" for each degree d.

For "how tall is Kim?", this is: { λw. height_w(Kim) ≥ d | d ∈ D }

The most informative answer has d = height(Kim).

Equations

• Semantics.Degree.DegreeQuestion.answerSet μ = {p : W → Prop | ∃ (d : D), p = fun (w : W) => μ w ≥ d}

def Semantics.Degree.DegreeQuestion.isMaximalAnswer {W : Type u_1} {D : Type u_2} [LinearOrder D] (μ : W → D) (d₀ : D) (w : W) : Prop

The maximally informative answer to "how tall is Kim?" is the degree d₀ such that "height(Kim) ≥ d₀" is true and entails all other true answers.

This connects to IsMaxInf from Core.Scale: the maximally informative element of the "at least" degree property.

Equations

• Semantics.Degree.DegreeQuestion.isMaximalAnswer μ d₀ w = Core.Scale.IsMaxInf (Core.Scale.atLeastDeg μ) d₀ w

def Semantics.Degree.DegreeQuestion.hasMaximalAnswer {W : Type u_1} {D : Type u_2} [LinearOrder D] (μ : W → D) (w : W) : Prop

The maximally informative answer exists iff the degree property has max⊨. For "at least d", this always exists (= the true value). For "more than d", this fails on dense scales (Fox & Hackl).

Equations

• Semantics.Degree.DegreeQuestion.hasMaximalAnswer μ w = Core.Scale.HasMaxInf (Core.Scale.atLeastDeg μ) w

theorem Semantics.Degree.DegreeQuestion.simple_degree_question_has_answer {W : Type u_1} {D : Type u_2} [LinearOrder D] (μ : W → D) (w : W) : hasMaximalAnswer μ w

Simple degree questions always have maximally informative answers (because "at least d" is a closed degree property).