Focus interpretation

Set-based encoding of Rooth's focus interpretation principle (FIP). Focus values are represented as Set (Set W), matching Hamblin-style question denotations; the anaphoric squiggle machinery lives in Semantics/Focus/Control.lean.

References

• [Roo92].

@[reducible, inline]

abbrev Semantics.Focus.Interpretation.PropFocusValue (W : Type u_2) : Type u_2

Propositional focus value: a set of propositions over W.

Equations

• Semantics.Focus.Interpretation.PropFocusValue W = Set (Set W)

def Semantics.Focus.Interpretation.fip {W : Type u_1} (gamma focusValue : Set (Set W)) : Prop

Focus interpretation principle: the contextual contrast set Γ is a subset of the focus semantic value.

Equations

• Semantics.Focus.Interpretation.fip gamma focusValue = (gamma ⊆ focusValue)

def Semantics.Focus.Interpretation.qaCongruent {W : Type u_1} (answerFocus question : PropFocusValue W) : Prop

Q-A congruence (strong): answer focus value equals question denotation.

Equations

• Semantics.Focus.Interpretation.qaCongruent answerFocus question = (answerFocus = question)

def Semantics.Focus.Interpretation.qaCongruentWeak {W : Type u_1} (answerFocus question : PropFocusValue W) : Prop

Q-A congruence (weak): question denotation is a subset of the answer focus value.

Equations

• Semantics.Focus.Interpretation.qaCongruentWeak answerFocus question = (question ⊆ answerFocus)