@cite{rooth-1992} Bridge — Focus Interpretation @cite{rooth-1992}

Bridges the empirical data in Focus/Basic.lean to the formal theory in Focus/Interpretation.lean (FIP, Q-A congruence), with a full compositional derivational chain through Montague semantics and connection to English fragment entries.

Pipeline

Fragments/English/Nouns ──▷ Montague Lexicon ──▷ Tree
                                                        │
                                                    interp
                                                        │
                                                        ▼
                              propositions (QAWorld → Bool)
                                                        │
                                                   fromAlternatives
                                                        │
                                                        ▼
                                              QuestionDen / PropFocusValue
                                                        │
                                                   FIP / qaCongruent
                                                        │
                                                        ▼
                                              Bridge theorems ↔ Data

Model

• Q-A congruence: 4 worlds crossing subject (Fred/Mary) × object (beans/rice). Subject focus matches "Who ate the beans?"; object focus does not.
• "Only" association: 3 worlds for who Mary introduced to Sue.

What's exercised

• AltMeaning, AltMeaning.unfeatured — O/A-value computation (§3)
• Focus, Background — focus/background partition (§4)
• Theme, Rheme, InfoStructure — information structure analysis (§5)
• HasInfoStructure — typeclass instance (§5b)
• FIPApplication — FIP application classification (§8)
• Tree, interp — compositional derivation (§10–§11)
• Derivation — derivation bundles (§13)
• Fragments.English.Nouns, .Predicates.Verbal — fragment entries (§14)

inductive Phenomena.Focus.Rooth1992Bridge.QAWorld : Type

Worlds crossing subject (Fred/Mary) × object (beans/rice). Sufficient to distinguish subject-focus from object-focus alternative sets.

• fredBeans : QAWorld
• fredRice : QAWorld
• maryBeans : QAWorld
• maryRice : QAWorld

instance Phenomena.Focus.Rooth1992Bridge.instDecidableEqQAWorld : DecidableEq QAWorld

Equations

• Phenomena.Focus.Rooth1992Bridge.instDecidableEqQAWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Focus.Rooth1992Bridge.instBEqQAWorld.beq : QAWorld → QAWorld → Bool

Equations

• Phenomena.Focus.Rooth1992Bridge.instBEqQAWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Focus.Rooth1992Bridge.instBEqQAWorld : BEq QAWorld

Equations

• Phenomena.Focus.Rooth1992Bridge.instBEqQAWorld = { beq := Phenomena.Focus.Rooth1992Bridge.instBEqQAWorld.beq }

def Phenomena.Focus.Rooth1992Bridge.instReprQAWorld.repr : QAWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Focus.Rooth1992Bridge.instReprQAWorld : Repr QAWorld

Equations

• Phenomena.Focus.Rooth1992Bridge.instReprQAWorld = { reprPrec := Phenomena.Focus.Rooth1992Bridge.instReprQAWorld.repr }

def Phenomena.Focus.Rooth1992Bridge.qaWorlds : List QAWorld

Equations

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

def Phenomena.Focus.Rooth1992Bridge.fredAteBeans : QAWorld → Bool

"Fred ate the beans"

Equations

• Phenomena.Focus.Rooth1992Bridge.fredAteBeans Phenomena.Focus.Rooth1992Bridge.QAWorld.fredBeans = true
• Phenomena.Focus.Rooth1992Bridge.fredAteBeans x✝ = false

def Phenomena.Focus.Rooth1992Bridge.maryAteBeans : QAWorld → Bool

"Mary ate the beans"

Equations

• Phenomena.Focus.Rooth1992Bridge.maryAteBeans Phenomena.Focus.Rooth1992Bridge.QAWorld.maryBeans = true
• Phenomena.Focus.Rooth1992Bridge.maryAteBeans x✝ = false

def Phenomena.Focus.Rooth1992Bridge.fredAteRice : QAWorld → Bool

"Fred ate the rice"

Equations

• Phenomena.Focus.Rooth1992Bridge.fredAteRice Phenomena.Focus.Rooth1992Bridge.QAWorld.fredRice = true
• Phenomena.Focus.Rooth1992Bridge.fredAteRice x✝ = false

def Phenomena.Focus.Rooth1992Bridge.altSubjectFocused : Core.InformationStructure.AltMeaning String

Focused "FRED" in "FRED ate the beans" (Rooth §2.4, ex. 23a): O-value = "Fred"; A-value = {"Fred", "Mary"}.

Equations

• Phenomena.Focus.Rooth1992Bridge.altSubjectFocused = { oValue := "Fred", aValue := ["Fred", "Mary"] }

def Phenomena.Focus.Rooth1992Bridge.altPredicateUnfeatured : Core.InformationStructure.AltMeaning String

Non-focused "ate the beans": singleton A-value (no alternatives). Exercises AltMeaning.unfeatured.

Equations

• Phenomena.Focus.Rooth1992Bridge.altPredicateUnfeatured = Core.InformationStructure.AltMeaning.unfeatured "ate the beans"

theorem Phenomena.Focus.Rooth1992Bridge.unfeatured_preserves_oValue : altPredicateUnfeatured.oValue = "ate the beans"

Unfeatured O-value equals the input.

theorem Phenomena.Focus.Rooth1992Bridge.unfeatured_singleton_aValue : altPredicateUnfeatured.aValue = ["ate the beans"]

Unfeatured A-value is a singleton containing the O-value. Non-focused expressions evoke no alternatives (@cite{rooth-1992} §1).

def Phenomena.Focus.Rooth1992Bridge.qaFocus : Core.InformationStructure.Focus String

Focus partition of "FRED ate the beans": Fred is focused, evoking {Fred, Mary} as alternatives (Rooth §2.4, ex. 25a).

Equations

• Phenomena.Focus.Rooth1992Bridge.qaFocus = { focused := "Fred", alternatives := ["Fred", "Mary"] }

def Phenomena.Focus.Rooth1992Bridge.qaBackground : Core.InformationStructure.Background String

Background of "FRED ate the beans": the non-focused material.

Equations

• Phenomena.Focus.Rooth1992Bridge.qaBackground = { elements := ["ate", "the", "beans"] }

def Phenomena.Focus.Rooth1992Bridge.qaTheme : Core.InformationStructure.Theme String

Theme: the QUD presupposition "_ ate the beans" (λ-abstract). Rooth §2.4: in a Q-A pair, the theme corresponds to the question's content.

Equations

• Phenomena.Focus.Rooth1992Bridge.qaTheme = { content := "λx. x ate the beans" }

def Phenomena.Focus.Rooth1992Bridge.qaRheme : Core.InformationStructure.Rheme String

Rheme: the answer "Fred".

Equations

• Phenomena.Focus.Rooth1992Bridge.qaRheme = { content := "Fred" }

def Phenomena.Focus.Rooth1992Bridge.qaInfo : Core.InformationStructure.InfoStructure String

Full information structure of "FRED ate the beans" in response to "Who ate the beans?"

Equations

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

theorem Phenomena.Focus.Rooth1992Bridge.qa_theme_content : qaInfo.theme.content = "λx. x ate the beans"

Theme carries the presupposed content.

theorem Phenomena.Focus.Rooth1992Bridge.qa_rheme_content : qaInfo.rheme.content = "Fred"

Rheme carries the asserted answer.

theorem Phenomena.Focus.Rooth1992Bridge.qa_foci_match : qaInfo.foci = [qaFocus.focused]

Focus list matches the focused element.

theorem Phenomena.Focus.Rooth1992Bridge.qa_background_match : qaInfo.background = qaBackground.elements

Background list matches the background elements.

structure Phenomena.Focus.Rooth1992Bridge.FocusedSentence : Type

Minimal derivation type for exercising HasInfoStructure. Pairs a focused constituent with background material.

• focusedWord : String
• backgroundWords : List String

def Phenomena.Focus.Rooth1992Bridge.instReprFocusedSentence.repr : FocusedSentence → ℕ → Std.Format

Equations

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

instance Phenomena.Focus.Rooth1992Bridge.instReprFocusedSentence : Repr FocusedSentence

Equations

• Phenomena.Focus.Rooth1992Bridge.instReprFocusedSentence = { reprPrec := Phenomena.Focus.Rooth1992Bridge.instReprFocusedSentence.repr }

instance Phenomena.Focus.Rooth1992Bridge.instHasInfoStructureFocusedSentenceString : Core.InformationStructure.HasInfoStructure FocusedSentence String

Exercises the HasInfoStructure typeclass: a FocusedSentence determines an InfoStructure.

Equations

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

def Phenomena.Focus.Rooth1992Bridge.fredSentence : FocusedSentence

Equations

• Phenomena.Focus.Rooth1992Bridge.fredSentence = { focusedWord := "Fred", backgroundWords := ["ate", "the", "beans"] }

theorem Phenomena.Focus.Rooth1992Bridge.infoStructure_extracts_focus : (Core.InformationStructure.HasInfoStructure.infoStructure fredSentence).foci = ["Fred"]

The typeclass correctly extracts focus.

theorem Phenomena.Focus.Rooth1992Bridge.infoStructure_extracts_background : (Core.InformationStructure.HasInfoStructure.infoStructure fredSentence).background = ["ate", "the", "beans"]

The typeclass correctly extracts background.

@cite{rooth-1992} §2.4, constraint (26d): In a Q-A pair ⟨ψ, α⟩, ⟦ψ⟧° ⊆ ⟦α⟧f. The ordinary semantic value of the question is a subset of the focus semantic value of the answer.

def Phenomena.Focus.Rooth1992Bridge.q_whoAteBeans : Semantics.Questions.Hamblin.QuestionDen QAWorld

"Who ate the beans?" — Hamblin question with subject alternatives. ⟦Q⟧° = {fredAteBeans, maryAteBeans} (Rooth §2.4, ex. 24).

Equations

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

def Phenomena.Focus.Rooth1992Bridge.fv_subjectFocus : Semantics.Questions.Hamblin.QuestionDen QAWorld

Focus value of "[FRED]_F ate the beans" — same subject alternatives. ⟦A⟧f = {fredAteBeans, maryAteBeans} (Rooth §2.4, ex. 25a).

Equations

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

def Phenomena.Focus.Rooth1992Bridge.fv_objectFocus : Semantics.Questions.Hamblin.QuestionDen QAWorld

Focus value of "Fred ate the [BEANS]_F" — object alternatives. ⟦A⟧f = {fredAteBeans, fredAteRice} (varies object, not subject).

Equations

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

theorem Phenomena.Focus.Rooth1992Bridge.qa_subject_focus_congruent : Semantics.FocusInterpretation.qaCongruent fv_subjectFocus q_whoAteBeans

Q-A congruence: subject focus value = question denotation. ⟦[FRED]_F ate the beans⟧f = ⟦Who ate the beans?⟧ (Rooth §2.4).

theorem Phenomena.Focus.Rooth1992Bridge.fip_congruent : Semantics.FocusInterpretation.fip q_whoAteBeans fv_subjectFocus

FIP (27) holds: question alternatives ⊆ focus value. Trivially satisfied when the sets are equal.

theorem Phenomena.Focus.Rooth1992Bridge.fip_fails_object_focus : ¬Semantics.FocusInterpretation.fip q_whoAteBeans fv_objectFocus

FIP fails for object focus: "maryAteBeans" is in the question alternatives but not in the object-focus alternatives. This is why "#Fred ate the BEANS" is not a congruent answer to "Who ate the beans?"

theorem Phenomena.Focus.Rooth1992Bridge.maryAteBeans_answers_question : Semantics.Questions.Hamblin.isAnswer q_whoAteBeans maryAteBeans = true

Witness: "Mary ate the beans" is an answer to the question...

theorem Phenomena.Focus.Rooth1992Bridge.maryAteBeans_not_in_objectFocus : Semantics.Questions.Hamblin.isAnswer fv_objectFocus maryAteBeans = false

...but is NOT in the object-focus alternative set.

Rooth §2.1, constraint (26a): the domain of quantification C of a focusing adverb is a subset of the focus semantic value ⟦α⟧f.

Rooth's formalization (30b): only(C) introduces
  ∀P[P ∈ C ∧ P(m) → P = VP']
where C is constrained by the FIP to be a set of properties
matching the focus semantic value. 

inductive Phenomena.Focus.Rooth1992Bridge.OnlyWorld : Type

Worlds for the "only" model: who Mary introduced to Sue.

• billOnly : OnlyWorld
• johnOnly : OnlyWorld
• both : OnlyWorld

instance Phenomena.Focus.Rooth1992Bridge.instDecidableEqOnlyWorld : DecidableEq OnlyWorld

Equations

• Phenomena.Focus.Rooth1992Bridge.instDecidableEqOnlyWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Focus.Rooth1992Bridge.instBEqOnlyWorld : BEq OnlyWorld

Equations

• Phenomena.Focus.Rooth1992Bridge.instBEqOnlyWorld = { beq := Phenomena.Focus.Rooth1992Bridge.instBEqOnlyWorld.beq }

def Phenomena.Focus.Rooth1992Bridge.instBEqOnlyWorld.beq : OnlyWorld → OnlyWorld → Bool

Equations

• Phenomena.Focus.Rooth1992Bridge.instBEqOnlyWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Focus.Rooth1992Bridge.instReprOnlyWorld.repr : OnlyWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Focus.Rooth1992Bridge.instReprOnlyWorld : Repr OnlyWorld

Equations

• Phenomena.Focus.Rooth1992Bridge.instReprOnlyWorld = { reprPrec := Phenomena.Focus.Rooth1992Bridge.instReprOnlyWorld.repr }

def Phenomena.Focus.Rooth1992Bridge.onlyWorlds : List OnlyWorld

Equations

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

def Phenomena.Focus.Rooth1992Bridge.introBill : OnlyWorld → Bool

"Mary introduced Bill to Sue"

Equations

• Phenomena.Focus.Rooth1992Bridge.introBill Phenomena.Focus.Rooth1992Bridge.OnlyWorld.billOnly = true
• Phenomena.Focus.Rooth1992Bridge.introBill Phenomena.Focus.Rooth1992Bridge.OnlyWorld.johnOnly = false
• Phenomena.Focus.Rooth1992Bridge.introBill Phenomena.Focus.Rooth1992Bridge.OnlyWorld.both = true

def Phenomena.Focus.Rooth1992Bridge.introJohn : OnlyWorld → Bool

"Mary introduced John to Sue"

Equations

• Phenomena.Focus.Rooth1992Bridge.introJohn Phenomena.Focus.Rooth1992Bridge.OnlyWorld.billOnly = false
• Phenomena.Focus.Rooth1992Bridge.introJohn Phenomena.Focus.Rooth1992Bridge.OnlyWorld.johnOnly = true
• Phenomena.Focus.Rooth1992Bridge.introJohn Phenomena.Focus.Rooth1992Bridge.OnlyWorld.both = true

def Phenomena.Focus.Rooth1992Bridge.altBillFocused : Core.InformationStructure.AltMeaning (OnlyWorld → Bool)

Focus on BILL (Rooth §2.1, ex. 3a): O-value = introBill; A-value = {introBill, introJohn}. Focus determines the domain of "only".

Equations

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

def Phenomena.Focus.Rooth1992Bridge.onlyBill : OnlyWorld → Bool

"Only Bill" = Mary introduced Bill but not John (Rooth §2.1).

Equations

• Phenomena.Focus.Rooth1992Bridge.onlyBill Phenomena.Focus.Rooth1992Bridge.OnlyWorld.billOnly = true
• Phenomena.Focus.Rooth1992Bridge.onlyBill x✝ = false

def Phenomena.Focus.Rooth1992Bridge.onlyJohn : OnlyWorld → Bool

"Only John" = Mary introduced John but not Bill.

Equations

• Phenomena.Focus.Rooth1992Bridge.onlyJohn Phenomena.Focus.Rooth1992Bridge.OnlyWorld.johnOnly = true
• Phenomena.Focus.Rooth1992Bridge.onlyJohn x✝ = false

theorem Phenomena.Focus.Rooth1992Bridge.only_bill_semantics : (onlyWorlds.all fun (w : OnlyWorld) => onlyBill w == (introBill w && !introJohn w)) = true

"Only" with focus on BILL: O-value holds and all non-actual alternatives are excluded (Rooth §2.1, (30b)).

theorem Phenomena.Focus.Rooth1992Bridge.only_john_semantics : (onlyWorlds.all fun (w : OnlyWorld) => onlyJohn w == (introJohn w && !introBill w)) = true

"Only" with focus on JOHN: symmetric case.

theorem Phenomena.Focus.Rooth1992Bridge.only_focus_determines_meaning : onlyBill ≠ onlyJohn

Different focus → different "only" meaning. Focus on BILL excludes John; focus on JOHN excludes Bill (Rooth §2.1, exs. 3a vs 3b).

theorem Phenomena.Focus.Rooth1992Bridge.datum_qa_congruent_app : Basic.qaCongruent.application = Core.InformationStructure.FIPApplication.qaCongruence

The Q-A congruent datum uses the correct FIPApplication.

theorem Phenomena.Focus.Rooth1992Bridge.datum_qa_incongruent_app : Basic.qaIncongruent.application = Core.InformationStructure.FIPApplication.qaCongruence

The Q-A incongruent datum uses the correct FIPApplication.

theorem Phenomena.Focus.Rooth1992Bridge.datum_qa_congruent_focus : Basic.qaCongruent.focus = "Fred"

Focus in the congruent answer matches the data.

theorem Phenomena.Focus.Rooth1992Bridge.datum_qa_incongruent_focus : Basic.qaIncongruent.focus = "beans"

Focus in the incongruent answer matches the data.

theorem Phenomena.Focus.Rooth1992Bridge.datum_only_bill_app : Basic.roothOnlyBill.application = Core.InformationStructure.FIPApplication.focusingAdverb

The "only Bill" datum uses focusing adverb application.

theorem Phenomena.Focus.Rooth1992Bridge.datum_only_sue_app : Basic.roothOnlySue.application = Core.InformationStructure.FIPApplication.focusingAdverb

The "only Sue" datum uses focusing adverb application.

The data (Basic.lean) says "FRED ate the beans" is congruent and "#Fred ate the BEANS" is incongruent with "Who ate the beans?". The theory (FIP, §6) explains:

- Subject focus produces a focus value equal to the question
  denotation (§6a), so FIP is satisfied.
- Object focus produces a focus value that differs (§6b):
  maryAteBeans ∈ ⟦Q⟧° but maryAteBeans ∉ ⟦A⟧f, so FIP fails.

For "only" (§7), the data says focus determines what "only"
excludes. The theory confirms: the FIP constrains the domain C
of "only" to be a subset of the focus value, so different focus
positions yield different exclusion domains. 

theorem Phenomena.Focus.Rooth1992Bridge.bridge_qa_congruent : Basic.qaCongruent.application = Core.InformationStructure.FIPApplication.qaCongruence ∧ Semantics.FocusInterpretation.qaCongruent fv_subjectFocus q_whoAteBeans

Bridge: congruent judgment confirmed by FIP.

theorem Phenomena.Focus.Rooth1992Bridge.bridge_qa_incongruent : Basic.qaIncongruent.application = Core.InformationStructure.FIPApplication.qaCongruence ∧ ¬Semantics.FocusInterpretation.fip q_whoAteBeans fv_objectFocus

Bridge: incongruent judgment explained by FIP failure.

The propositions in §2 were hand-defined. Here we derive them compositionally: entity denotations + a world-indexed verb meaning are combined via direct function application and Heim & Kratzer's interp to produce the same truth conditions.

The derivational chain is:
  Fragment entry → Montague LexEntry → Tree → interp → Bool
run once per world to yield a world-indexed proposition. 

inductive Phenomena.Focus.Rooth1992Bridge.E : Type

Entity domain for the focus model.

• fred : E
• mary : E
• beans : E
• rice : E

instance Phenomena.Focus.Rooth1992Bridge.instDecidableEqE : DecidableEq E

Equations

• Phenomena.Focus.Rooth1992Bridge.instDecidableEqE x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Focus.Rooth1992Bridge.instBEqE : BEq E

Equations

• Phenomena.Focus.Rooth1992Bridge.instBEqE = { beq := Phenomena.Focus.Rooth1992Bridge.instBEqE.beq }

def Phenomena.Focus.Rooth1992Bridge.instBEqE.beq : E → E → Bool

Equations

• Phenomena.Focus.Rooth1992Bridge.instBEqE.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Focus.Rooth1992Bridge.instReprE : Repr E

Equations

• Phenomena.Focus.Rooth1992Bridge.instReprE = { reprPrec := Phenomena.Focus.Rooth1992Bridge.instReprE.repr }

def Phenomena.Focus.Rooth1992Bridge.instReprE.repr : E → ℕ → Std.Format

Equations

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

def Phenomena.Focus.Rooth1992Bridge.focusModel : Semantics.Montague.Model

Equations

• Phenomena.Focus.Rooth1992Bridge.focusModel = { Entity := Phenomena.Focus.Rooth1992Bridge.E, decEq := inferInstance }

def Phenomena.Focus.Rooth1992Bridge.ateInWorld (w : QAWorld) : focusModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

World-indexed verb semantics for "ate". ateInWorld w obj subj follows Montague's argument order (object first, then subject).

Equations

• Phenomena.Focus.Rooth1992Bridge.ateInWorld Phenomena.Focus.Rooth1992Bridge.QAWorld.fredBeans Phenomena.Focus.Rooth1992Bridge.E.beans Phenomena.Focus.Rooth1992Bridge.E.fred = true
• Phenomena.Focus.Rooth1992Bridge.ateInWorld Phenomena.Focus.Rooth1992Bridge.QAWorld.fredRice Phenomena.Focus.Rooth1992Bridge.E.rice Phenomena.Focus.Rooth1992Bridge.E.fred = true
• Phenomena.Focus.Rooth1992Bridge.ateInWorld Phenomena.Focus.Rooth1992Bridge.QAWorld.maryBeans Phenomena.Focus.Rooth1992Bridge.E.beans Phenomena.Focus.Rooth1992Bridge.E.mary = true
• Phenomena.Focus.Rooth1992Bridge.ateInWorld Phenomena.Focus.Rooth1992Bridge.QAWorld.maryRice Phenomena.Focus.Rooth1992Bridge.E.rice Phenomena.Focus.Rooth1992Bridge.E.mary = true
• Phenomena.Focus.Rooth1992Bridge.ateInWorld w obj subj = false

def Phenomena.Focus.Rooth1992Bridge.focusLex (w : QAWorld) : Semantics.Montague.Lexicon focusModel

Montague lexicon parameterized by world. Maps surface forms to typed denotations.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Focus.Rooth1992Bridge.focusLex w "Fred" = some { ty := Semantics.Montague.Ty.e, denot := Phenomena.Focus.Rooth1992Bridge.E.fred }
• Phenomena.Focus.Rooth1992Bridge.focusLex w "Mary" = some { ty := Semantics.Montague.Ty.e, denot := Phenomena.Focus.Rooth1992Bridge.E.mary }
• Phenomena.Focus.Rooth1992Bridge.focusLex w "beans" = some { ty := Semantics.Montague.Ty.e, denot := Phenomena.Focus.Rooth1992Bridge.E.beans }
• Phenomena.Focus.Rooth1992Bridge.focusLex w "rice" = some { ty := Semantics.Montague.Ty.e, denot := Phenomena.Focus.Rooth1992Bridge.E.rice }
• Phenomena.Focus.Rooth1992Bridge.focusLex w word = none

def Phenomena.Focus.Rooth1992Bridge.tree_fredAteBeans : Core.Tree.Tree Unit String

Syntax tree: [S [NP Fred] [VP [V ate] [NP beans]]]

Equations

• Phenomena.Focus.Rooth1992Bridge.tree_fredAteBeans = (Core.Tree.Tree.leaf "Fred").bin ((Core.Tree.Tree.leaf "ate").bin (Core.Tree.Tree.leaf "beans"))

def Phenomena.Focus.Rooth1992Bridge.tree_maryAteBeans : Core.Tree.Tree Unit String

Syntax tree: [S [NP Mary] [VP [V ate] [NP beans]]]

Equations

• Phenomena.Focus.Rooth1992Bridge.tree_maryAteBeans = (Core.Tree.Tree.leaf "Mary").bin ((Core.Tree.Tree.leaf "ate").bin (Core.Tree.Tree.leaf "beans"))

def Phenomena.Focus.Rooth1992Bridge.tree_fredAteRice : Core.Tree.Tree Unit String

Syntax tree: [S [NP Fred] [VP [V ate] [NP rice]]]

Equations

• Phenomena.Focus.Rooth1992Bridge.tree_fredAteRice = (Core.Tree.Tree.leaf "Fred").bin ((Core.Tree.Tree.leaf "ate").bin (Core.Tree.Tree.leaf "rice"))

def Phenomena.Focus.Rooth1992Bridge.treeResult (lex : Semantics.Montague.Lexicon focusModel) (t : Core.Tree.Tree Unit String) : Option Bool

Extract the Bool truth value from a tree interpretation. Returns none if the tree is uninterpretable or has non-t type.

Equations

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

The propositions from §2 were stipulated directly. Here we show they are derivable: running interp at each world produces the same truth values.

def Phenomena.Focus.Rooth1992Bridge.fredAteBeans_comp : QAWorld → Bool

Compositionally derived "Fred ate beans" proposition.

Equations

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

def Phenomena.Focus.Rooth1992Bridge.maryAteBeans_comp : QAWorld → Bool

Compositionally derived "Mary ate beans" proposition.

Equations

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

def Phenomena.Focus.Rooth1992Bridge.fredAteRice_comp : QAWorld → Bool

Compositionally derived "Fred ate rice" proposition.

Equations

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

theorem Phenomena.Focus.Rooth1992Bridge.comp_grounds_fredAteBeans : fredAteBeans_comp = fredAteBeans

Grounding: compositional "Fred ate beans" = hand-defined proposition.

theorem Phenomena.Focus.Rooth1992Bridge.comp_grounds_maryAteBeans : maryAteBeans_comp = maryAteBeans

Grounding: compositional "Mary ate beans" = hand-defined proposition.

theorem Phenomena.Focus.Rooth1992Bridge.comp_grounds_fredAteRice : fredAteRice_comp = fredAteRice

Grounding: compositional "Fred ate rice" = hand-defined proposition.

theorem Phenomena.Focus.Rooth1992Bridge.direct_eq_interp (w : QAWorld) : treeResult (focusLex w) tree_fredAteBeans = some (ateInWorld w E.beans E.fred)

Direct function application matches tree interpretation.

Connect the model's lexicon to English fragment entries. Fragment entries provide morphological and syntactic properties; the bridge verifies that these properties are consistent with the model and that fragment surface forms feed the compositional lexicon.

theorem Phenomena.Focus.Rooth1992Bridge.fragment_fred_proper : Fragments.English.Nouns.fred.proper = true

Fred is a proper name in the English fragment.

theorem Phenomena.Focus.Rooth1992Bridge.fragment_mary_proper : Fragments.English.Nouns.mary.proper = true

Mary is a proper name in the English fragment.

theorem Phenomena.Focus.Rooth1992Bridge.fragment_bean_countable : Fragments.English.Nouns.bean.countable = MassCount.count

"bean" is countable in the English fragment.

theorem Phenomena.Focus.Rooth1992Bridge.fragment_fred_in_lexicon : (focusLex QAWorld.fredBeans Fragments.English.Nouns.fred.formSg).isSome = true

Fragment surface forms feed the Montague lexicon. The form field of each fragment entry matches a lexicon key.

theorem Phenomena.Focus.Rooth1992Bridge.fragment_mary_in_lexicon : (focusLex QAWorld.fredBeans Fragments.English.Nouns.mary.formSg).isSome = true

theorem Phenomena.Focus.Rooth1992Bridge.fragment_bean_pl_in_lexicon : (focusLex QAWorld.fredBeans (Fragments.English.Nouns.bean.formPl.getD "")).isSome = true

theorem Phenomena.Focus.Rooth1992Bridge.fragment_eat_transitive : Fragments.English.Predicates.Verbal.eat.complementType = Core.Verbs.ComplementType.np

"eat" is transitive (NP complement).

theorem Phenomena.Focus.Rooth1992Bridge.fragment_eat_past_form : Fragments.English.Predicates.Verbal.eat.formPast = "ate"

"eat" has past tense "ate" matching the lexicon entry.

theorem Phenomena.Focus.Rooth1992Bridge.fragment_eat_past_in_lexicon : (focusLex QAWorld.fredBeans Fragments.English.Predicates.Verbal.eat.formPast).isSome = true

The past form of "eat" is in the Montague lexicon.

The complete derivational chain from fragments to FIP:

1. Fragment entries (§14) provide surface forms and properties
2. Surface forms feed the Montague lexicon (§10)
3. Tree derivations compose meanings via interp (§11)
4. Running at each world yields propositions grounding §2 (§12)
5. Propositions build Hamblin questions and focus values (§6)
6. FIP/qaCongruent proves congruence (§6a) or incongruence (§6b)
7. Theoretical predictions match empirical judgments (§9) 

theorem Phenomena.Focus.Rooth1992Bridge.endToEnd_question_grounded : Semantics.Questions.Hamblin.fromAlternatives [fredAteBeans_comp, maryAteBeans_comp] qaWorlds = q_whoAteBeans

End-to-end: the compositionally derived question matches the hand-built question, so the FIP results in §6 apply to the compositional derivation.