Focus-Sensitivity and Degree Semantics

@cite{rooth-1992} @cite{villalta-2008} @cite{kennedy-2007} @cite{ozyildiz-etal-2025}

Structural bridge between Rooth's focus alternatives, Villalta's degree semantics for preferential predicates, and Kennedy's significance presuppositions.

The Compositional Chain

Focus marking on α produces ⟦α⟧o and ⟦α⟧f          [Rooth 1985/1992]
        ↓
~ resolves C ⊆ ⟦α⟧f with ⟦α⟧o ∈ C                 [Rooth 1992]
        ↓
Degree predicate: μ(x, ⟦α⟧o) > θ(C)                [Villalta 2008]
        ↓
Significance presup: ∃q ∈ C. μ(x,q) > θ(C)         [Kennedy 2007]
        ↓
For positive valence: this = TSP                      [Uegaki & Sudo 2019]

Key Results

• liftDegreeFS: degree predicates become focus-sensitive ClauseEmbedPreds
• liftDegreeFS_is_fs: proves focus-sensitivity when threshold depends on C
• focusSignificance: ~ + degree predicate → significance presupposition
• tsp_from_focus: for positive valence, focus significance = TSP
• assertion_entails_tsp: if the assertion holds, TSP is automatically satisfied (the ordinary value, guaranteed in C by ~, is itself the witness)

Lifting Degree Predicates via Focus Alternatives

A degree-comparison predicate μ(x,p) > θ(C) becomes a ClauseEmbedPred when the comparison class C is determined by the focus alternatives via a conversion function altsToC.

This models what the ~ operator does: it resolves focus alternatives ⟦α⟧f to a comparison class C. The altsToC parameter abstracts over the contextual resolution.

Combined with liftNonFS (from Interpretation.lean), this gives a complete structural account of focus-sensitivity:

• Degree predicates → focus-sensitive (by liftDegreeFS_is_fs)
• Doxastic predicates → not focus-sensitive (by liftNonFS_not_fs)

def Semantics.Focus.Sensitivity.liftDegreeFS {W : Type u_1} {E : Type u_2} (μ : Attitudes.Preferential.PreferenceFunction W E) (θ : Attitudes.Preferential.ThresholdFunction W) (altsToC : FocusInterpretation.PropFocusValue W → Attitudes.Preferential.QuestionDen W) : FocusInterpretation.ClauseEmbedPred W E

Lift a degree-comparison predicate to ClauseEmbedPred by using focus alternatives as the comparison class.

• @cite{rooth-1992}: focus alternatives ⟦α⟧f
• @cite{villalta-2008}: comparison class C in μ(x,p) > θ(C)
• Connection: C = altsToC(⟦α⟧f) — the ~ operator's role

Equations

• Semantics.Focus.Sensitivity.liftDegreeFS μ θ altsToC x p f _w = decide (μ x p > θ (altsToC f))

theorem Semantics.Focus.Sensitivity.liftDegreeFS_is_fs {W : Type u_1} {E : Type u_2} (μ : Attitudes.Preferential.PreferenceFunction W E) (θ : Attitudes.Preferential.ThresholdFunction W) (altsToC : FocusInterpretation.PropFocusValue W → Attitudes.Preferential.QuestionDen W) (x : E) (p : W → Bool) (w : W) (f₁ f₂ : FocusInterpretation.PropFocusValue W) (h_above : μ x p > θ (altsToC f₁)) (h_below : ¬μ x p > θ (altsToC f₂)) : FocusInterpretation.IsFocusSensitive (liftDegreeFS μ θ altsToC)

Degree predicates lifted via focus alternatives ARE focus-sensitive, provided the threshold depends nontrivially on the comparison class.

Sufficient condition: two focus-alternative sets yield different thresholds, with the preference value falling between them.

This is THE structural bridge between @cite{rooth-1992} and @cite{villalta-2008}: degree truth depends on focus alternatives because they determine the comparison class.

From ~ to Significance Presuppositions

When the ~ operator resolves focus alternatives to a comparison class C (via FocusResolution), and a degree predicate uses C, Kennedy's significance generalization produces a presupposition.

The Derivation

1. ~ introduces C with C ⊆ ⟦α⟧f and ⟦α⟧o ∈ C (FocusResolution)
2. Degree predicate asserts: μ(x, ⟦α⟧o) > θ(C)
3. Kennedy significance: the degree scale must be "significant" w.r.t. C
4. For positive valence: significance = ∃q ∈ C. μ(x,q) > θ(C) = TSP

Why ⟦α⟧o ∈ C Matters

The ordinary-value-in-C constraint (from FocusResolution.ordinary_in_C) ensures that whenever the assertion is true, the TSP is automatically satisfied — the ordinary value itself is the witness. This is the compositional reason why TSP is non-vacuous: ~ guarantees a candidate.

def Semantics.Focus.Sensitivity.focusSignificance {W : Type u_1} {E : Type u_2} (valence : Attitudes.Preferential.AttitudeValence) (μ : Attitudes.Preferential.PreferenceFunction W E) (θ : Attitudes.Preferential.ThresholdFunction W) (x : E) (res : FocusInterpretation.FocusResolution W) : Bool

Significance presupposition arising from combining a degree predicate with a focus-resolved comparison class.

When ~ resolves ⟦α⟧f to C, and a degree predicate V uses C, the presupposition depends on V's valence:

• Positive (hope, want): ∃q ∈ C. μ(x,q) > θ(C) — this IS TSP
• Negative (fear): weaker threat-identification condition

@cite{kennedy-2007}: degree constructions carry significance presuppositions. @cite{uegaki-sudo-2019}: significance + positive valence = TSP.

Equations

• Semantics.Focus.Sensitivity.focusSignificance valence μ θ x res = Semantics.Attitudes.Preferential.significancePresupSatisfied valence μ θ x res.comparisonClass

theorem Semantics.Focus.Sensitivity.tsp_from_focus {W : Type u_1} {E : Type u_2} (μ : Attitudes.Preferential.PreferenceFunction W E) (θ : Attitudes.Preferential.ThresholdFunction W) (x : E) (res : FocusInterpretation.FocusResolution W) : focusSignificance Attitudes.Preferential.AttitudeValence.positive μ θ x res = Attitudes.Preferential.tspSatisfied μ θ x res.comparisonClass

For positive valence, focus significance IS TSP.

This closes the compositional chain: ~ → C → degree predicate → Kennedy significance → TSP.

The proof is definitional: significancePresupSatisfied .positive dispatches to tspSatisfied by construction. The non-trivial content is the ARCHITECTURE — TSP arises compositionally from focus + degree semantics rather than being stipulated per-predicate.

theorem Semantics.Focus.Sensitivity.assertion_entails_tsp {W : Type u_1} {E : Type u_2} (μ : Attitudes.Preferential.PreferenceFunction W E) (θ : Attitudes.Preferential.ThresholdFunction W) (x : E) (res : FocusInterpretation.FocusResolution W) (h_assert : μ x res.ordinary > θ res.comparisonClass) : Attitudes.Preferential.tspSatisfied μ θ x res.comparisonClass = true

If the degree assertion holds, the TSP is automatically satisfied.

The ordinary value ⟦α⟧o is guaranteed to be in C (by ~'s second constraint, FocusResolution.ordinary_in_C). So if μ(x, ⟦α⟧o) > θ(C) (the assertion), then ⟦α⟧o witnesses ∃q ∈ C. μ(x,q) > θ(C) (the TSP).

This is the compositional reason why TSP is a presupposition, not an independent requirement: it's entailed by the assertion whenever ~ resolves properly.

theorem Semantics.Focus.Sensitivity.negative_significance_trivial {W : Type u_1} {E : Type u_2} (μ : Attitudes.Preferential.PreferenceFunction W E) (θ : Attitudes.Preferential.ThresholdFunction W) (x : E) (res : FocusInterpretation.FocusResolution W) : focusSignificance Attitudes.Preferential.AttitudeValence.negative μ θ x res = true

Negative valence predicates always satisfy significance (trivially).

Fear, worry, and other negative-valence predicates have a weaker "threat identification" significance condition that is trivially true — hence no TSP, hence no triviality with questions, hence they CAN take interrogative complements.