@[reducible, inline]

abbrev Semantics.FocusInterpretation.PropFocusValue (W : Type u_1) : Type u_1

Propositional focus value: set of propositions. Type: <<s,t>,t> - same as Hamblin questions!

Equations

• Semantics.FocusInterpretation.PropFocusValue W = ((W → Bool) → Bool)

structure Semantics.FocusInterpretation.Squiggle (W : Type u_1) : Type u_1

The ~ operator introduces a focus constraint via anaphor Γ.

@cite{rooth-1992} §2: "α ~ Γ" where:

• α is an expression with focus marking
• Γ is an anaphoric variable resolved to a contextual set of alternatives
• FIP requires: Γ ⊆ ⟦α⟧f

• contrastSet : (W → Bool) → Bool

  The contrasting set Γ (anaphor to context)

def Semantics.FocusInterpretation.fip {W : Type u_1} (gamma focusValue : (W → Bool) → Bool) : Prop

Focus Interpretation Principle (FIP): The contextual contrast set Γ must be a subset of the focus semantic value.

@cite{rooth-1992} §2: "Γ ⊆ ⟦α⟧f"

Equations

• Semantics.FocusInterpretation.fip gamma focusValue = ∀ (p : W → Bool), gamma p = true → focusValue p = true

theorem Semantics.FocusInterpretation.hamblin_is_focus_type (W : Type u_1) : Questions.Hamblin.QuestionDen W = ((W → Bool) → Bool)

Grounding theorem: Hamblin question denotations have the same type as propositional focus semantic values.

This is the foundation of Q-A congruence: the focus value of an answer should equal (or be a superset) the question denotation.

def Semantics.FocusInterpretation.qaCongruent {W : Type u_1} (answerFocus : PropFocusValue W) (question : Questions.Hamblin.QuestionDen W) : Prop

Q-A Congruence: An answer is congruent to a question iff the focus semantic value of the answer equals the question denotation.

@cite{rooth-1992} §4: Focus on the answer must match the wh-position in the question.

Example:

• Q: "Who ate the beans?" = {λw. ate(x, beans, w) | x ∈ D}
• A: "FRED ate the beans" has ⟦A⟧f = {λw. ate(x, beans, w) | x ∈ D}
• Congruent iff ⟦A⟧f = ⟦Q⟧

Equations

• Semantics.FocusInterpretation.qaCongruent answerFocus question = (answerFocus = question)

def Semantics.FocusInterpretation.qaCongruentWeak {W : Type u_1} (answerFocus : PropFocusValue W) (question : Questions.Hamblin.QuestionDen W) : Prop

Weaker Q-A congruence: question alternatives are a subset of answer focus. This handles cases where the answer may introduce additional alternatives.

Equations

• Semantics.FocusInterpretation.qaCongruentWeak answerFocus question = ∀ (p : W → Bool), question p = true → answerFocus p = true

def Semantics.FocusInterpretation.FIPApplication.description : Core.InformationStructure.FIPApplication → String

Description of each FIP application

Equations

• Semantics.FocusInterpretation.FIPApplication.description Core.InformationStructure.FIPApplication.focusingAdverb = "Focus-sensitive particles (only, even, also) associate with focus"
• Semantics.FocusInterpretation.FIPApplication.description Core.InformationStructure.FIPApplication.contrast = "Parallel focus in discourse triggers contrast presupposition"
• Semantics.FocusInterpretation.FIPApplication.description Core.InformationStructure.FIPApplication.scalarImplicature = "Focus alternatives feed into scalar implicature computation"
• Semantics.FocusInterpretation.FIPApplication.description Core.InformationStructure.FIPApplication.qaCongruence = "Answer focus must match question (see Questions/FocusAnswer.lean)"

Full ~ Operator: Focus Resolution

@cite{rooth-1992} §2: α ~ introduces an anaphoric variable C (the comparison class / contrast set) constrained by TWO conditions:

1. FIP: C ⊆ ⟦α⟧f — every proposition in C is a focus alternative
2. Ordinary inclusion: ⟦α⟧o ∈ C — the ordinary value is in C

The existing fip function captures constraint 1 alone. FocusResolution bundles both constraints, making the full ~ semantics explicit.

This is the entry point for the compositional chain that derives TSP: ~ resolves C → degree predicate uses C → significance falls out. See Focus/Sensitivity.lean for the downstream derivation.

structure Semantics.FocusInterpretation.FocusResolution (W : Type u_1) : Type u_1

The full ~ operator resolves focus alternatives to a comparison class C.

Bundles @cite{rooth-1992}'s two constraints:

1. C ⊆ ⟦α⟧f (FIP — comparison class bounded by focus alternatives)
2. ⟦α⟧o ∈ C (ordinary value is in the comparison class)

The comparison class is extensional (List (W → Bool)) for compatibility with Attitudes.Preferential.QuestionDen.

• ordinary : W → Bool

  ⟦α⟧o — the ordinary semantic value of the focused constituent

• focusValue : PropFocusValue W

  ⟦α⟧f — the focus semantic value (set of alternative propositions)

• comparisonClass : List (W → Bool)

  C — the comparison class, resolved from context

• fip_subset (p : W → Bool) : p ∈ self.comparisonClass → self.focusValue p = true

  FIP: C ⊆ ⟦α⟧f — every proposition in C is a focus alternative

• ordinary_in_C : self.ordinary ∈ self.comparisonClass

  ⟦α⟧o ∈ C — the ordinary value is in the comparison class

@[reducible, inline]

abbrev Semantics.FocusInterpretation.ClauseEmbedPred (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A clause-embedding predicate with explicit access to focus alternatives.

Takes: agent, ordinary proposition, focus alternatives, world → truth value.

Non-focus-sensitive predicates (believe, know) ignore the focus alternatives. Focus-sensitive predicates (want, be glad, be surprised) use them to determine the comparison class for degree semantics.

@cite{ozyildiz-etal-2025} def 2/58.

Equations

• Semantics.FocusInterpretation.ClauseEmbedPred W E = (E → (W → Bool) → Semantics.FocusInterpretation.PropFocusValue W → W → Bool)

def Semantics.FocusInterpretation.IsFocusSensitive {W : Type u_1} {E : Type u_2} (V : ClauseEmbedPred W E) : Prop

A clause-embedding predicate V is focus-sensitive iff its truth value can depend on the focus alternatives, not just the ordinary proposition.

@cite{ozyildiz-etal-2025} def 2/58: there exist context, agent, proposition, and two different focus-alternative sets such that V yields different truth values.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.FocusInterpretation.IsNotFocusSensitive {W : Type u_1} {E : Type u_2} (V : ClauseEmbedPred W E) : Prop

A predicate is not focus-sensitive iff it ignores focus alternatives entirely.

Equations

• Semantics.FocusInterpretation.IsNotFocusSensitive V = ∀ (x : E) (p : W → Bool) (f₁ f₂ : Semantics.FocusInterpretation.PropFocusValue W) (w : W), V x p f₁ w = V x p f₂ w

theorem Semantics.FocusInterpretation.not_fs_iff_ignores_focus {W : Type u_1} {E : Type u_2} (V : ClauseEmbedPred W E) : IsNotFocusSensitive V ↔ ¬IsFocusSensitive V

def Semantics.FocusInterpretation.liftNonFS {W : Type u_1} {E : Type u_2} (V : E → (W → Bool) → W → Bool) : ClauseEmbedPred W E

Lift a non-focus-sensitive predicate to the ClauseEmbedPred type by ignoring focus alternatives.

Equations

• Semantics.FocusInterpretation.liftNonFS V x p _f w = V x p w

theorem Semantics.FocusInterpretation.liftNonFS_not_fs {W : Type u_1} {E : Type u_2} (V : E → (W → Bool) → W → Bool) : IsNotFocusSensitive (liftNonFS V)

Any lifted non-focus-sensitive predicate is indeed not focus-sensitive.

Additive Particles and FIP

@cite{rooth-1992} §2.2 analyzes "too" via FIP: @cite{rooth-1985}

"Mary read Lear, and she read Macbeth too"

• Focus: MACBETH
• ⟦Macbeth⟧f = {Lear, Macbeth, Hamlet,...} (works of Shakespeare)
• Antecedent "Lear" must be in ⟦Macbeth⟧f ✓
• FIP: The antecedent is in the focus alternatives

See:

• Phenomena/AdditiveParticles/Data.lean for empirical data
• Theories/Semantics/Focus/Particles.lean for semantic analysis