@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 (Set QAWorld)
                                                        │
                                                   set literals
                                                        │
                                                        ▼
                                              PropFocusValue = Set (Set QAWorld)
                                                        │
                                                   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)
• FocusedSentence.infoStructure — IS extractor (§5b; previously a HasInfoStructure instance)
• 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

@[implicit_reducible]

instance Phenomena.Focus.Rooth1992Bridge.instDecidableEqQAWorld : DecidableEq QAWorld

Equations

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

@[implicit_reducible]

instance Phenomena.Focus.Rooth1992Bridge.instReprQAWorld : Repr QAWorld

Equations

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

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

Equations

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

def Phenomena.Focus.Rooth1992Bridge.fredAteBeans : Set QAWorld

"Fred ate the beans" — true exactly at the world fredBeans.

Equations

• Phenomena.Focus.Rooth1992Bridge.fredAteBeans = {Phenomena.Focus.Rooth1992Bridge.QAWorld.fredBeans}

def Phenomena.Focus.Rooth1992Bridge.maryAteBeans : Set QAWorld

"Mary ate the beans" — true exactly at the world maryBeans.

Equations

• Phenomena.Focus.Rooth1992Bridge.maryAteBeans = {Phenomena.Focus.Rooth1992Bridge.QAWorld.maryBeans}

def Phenomena.Focus.Rooth1992Bridge.fredAteRice : Set QAWorld

"Fred ate the rice" — true exactly at the world fredRice.

Equations

• Phenomena.Focus.Rooth1992Bridge.fredAteRice = {Phenomena.Focus.Rooth1992Bridge.QAWorld.fredRice}

def Phenomena.Focus.Rooth1992Bridge.altSubjectFocused : Semantics.Alternatives.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 : Semantics.Alternatives.AltMeaning String

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

Equations

• Phenomena.Focus.Rooth1992Bridge.altPredicateUnfeatured = Semantics.Alternatives.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 : Features.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 : Features.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 : Features.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 : Features.InformationStructure.Rheme String

Rheme: the answer "Fred".

Equations

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

def Phenomena.Focus.Rooth1992Bridge.qaInfo : Features.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 the IS partition. 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.

@[implicit_reducible]

instance Phenomena.Focus.Rooth1992Bridge.instReprFocusedSentence : Repr FocusedSentence

Equations

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

def Phenomena.Focus.Rooth1992Bridge.FocusedSentence.infoStructure (s : FocusedSentence) : Features.InformationStructure.InfoStructure String

A FocusedSentence determines an InfoStructure.

(Previously a HasInfoStructure FocusedSentence String instance — the typeclass shape was deleted in the 0.230.489 cleanup since no caller dispatched on it.)

Equations

• s.infoStructure = { theme := { content := "background" }, rheme := { content := s.focusedWord }, foci := [s.focusedWord], background := s.backgroundWords }

def Phenomena.Focus.Rooth1992Bridge.fredSentence : FocusedSentence

Equations

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

theorem Phenomena.Focus.Rooth1992Bridge.infoStructure_extracts_focus : fredSentence.infoStructure.foci = ["Fred"]

The extractor correctly puts the focused word in foci.

theorem Phenomena.Focus.Rooth1992Bridge.infoStructure_extracts_background : fredSentence.infoStructure.background = ["ate", "the", "beans"]

The extractor correctly puts background words in 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.FocusInterpretation.PropFocusValue QAWorld

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

Equations

• Phenomena.Focus.Rooth1992Bridge.q_whoAteBeans = {Phenomena.Focus.Rooth1992Bridge.fredAteBeans, Phenomena.Focus.Rooth1992Bridge.maryAteBeans}

def Phenomena.Focus.Rooth1992Bridge.fv_subjectFocus : Semantics.FocusInterpretation.PropFocusValue QAWorld

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

Equations

• Phenomena.Focus.Rooth1992Bridge.fv_subjectFocus = {Phenomena.Focus.Rooth1992Bridge.fredAteBeans, Phenomena.Focus.Rooth1992Bridge.maryAteBeans}

def Phenomena.Focus.Rooth1992Bridge.fv_objectFocus : Semantics.FocusInterpretation.PropFocusValue QAWorld

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

Equations

• Phenomena.Focus.Rooth1992Bridge.fv_objectFocus = {Phenomena.Focus.Rooth1992Bridge.fredAteBeans, Phenomena.Focus.Rooth1992Bridge.fredAteRice}

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.maryAteBeans_in_question : maryAteBeans ∈ q_whoAteBeans

"maryAteBeans" is in the question alternatives...

theorem Phenomena.Focus.Rooth1992Bridge.maryAteBeans_not_in_objectFocus : maryAteBeans ∉ fv_objectFocus

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

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

...so FIP fails for object focus, explaining why "#Fred ate the BEANS" is not a congruent answer to "Who ate the beans?"

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

@[implicit_reducible]

instance Phenomena.Focus.Rooth1992Bridge.instDecidableEqOnlyWorld : DecidableEq OnlyWorld

Equations

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

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

Equations

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

@[implicit_reducible]

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 : Semantics.Alternatives.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 = Features.InformationStructure.FIPApplication.qaCongruence

The Q-A congruent datum uses the correct FIPApplication.

theorem Phenomena.Focus.Rooth1992Bridge.datum_qa_incongruent_app : Basic.qaIncongruent.application = Features.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 = Features.InformationStructure.FIPApplication.focusingAdverb

The "only Bill" datum uses focusing adverb application.

theorem Phenomena.Focus.Rooth1992Bridge.datum_only_sue_app : Basic.roothOnlySue.application = Features.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 = Features.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 = Features.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

@[implicit_reducible]

instance Phenomena.Focus.Rooth1992Bridge.instDecidableEqE : DecidableEq E

Equations

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

@[implicit_reducible]

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 : Core.Logic.Intensional.Frame

Equations

• Phenomena.Focus.Rooth1992Bridge.focusModel = { Entity := Phenomena.Focus.Rooth1992Bridge.E, Index := Unit }

def Phenomena.Focus.Rooth1992Bridge.ateInWorld (w : QAWorld) : focusModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.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 := Core.Logic.Intensional.Ty.e, denot := Phenomena.Focus.Rooth1992Bridge.E.fred }
• Phenomena.Focus.Rooth1992Bridge.focusLex w "Mary" = some { ty := Core.Logic.Intensional.Ty.e, denot := Phenomena.Focus.Rooth1992Bridge.E.mary }
• Phenomena.Focus.Rooth1992Bridge.focusLex w "beans" = some { ty := Core.Logic.Intensional.Ty.e, denot := Phenomena.Focus.Rooth1992Bridge.E.beans }
• Phenomena.Focus.Rooth1992Bridge.focusLex w "rice" = some { ty := Core.Logic.Intensional.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 Prop

Extract the Prop 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 → Prop

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 → Prop

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 → Prop

Compositionally derived "Fred ate rice" proposition.

Equations

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

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.

theorem Phenomena.Focus.Rooth1992Bridge.comp_grounds_fredAteBeans : fredAteBeans_comp = fun (w : QAWorld) => ateInWorld w E.beans E.fred

Grounding: compositional "Fred ate beans" agrees with hand-defined proposition at each world.

theorem Phenomena.Focus.Rooth1992Bridge.comp_grounds_maryAteBeans : maryAteBeans_comp = fun (w : QAWorld) => ateInWorld w E.beans E.mary

Grounding: compositional "Mary ate beans" = direct function application.

theorem Phenomena.Focus.Rooth1992Bridge.comp_grounds_fredAteRice : fredAteRice_comp = fun (w : QAWorld) => ateInWorld w E.rice E.fred

Grounding: compositional "Fred ate rice" = direct function application.

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 = Semantics.Lexical.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 : (∀ (w : QAWorld), treeResult (focusLex w) tree_fredAteBeans = some (ateInWorld w E.beans E.fred)) ∧ ∀ (w : QAWorld), treeResult (focusLex w) tree_maryAteBeans = some (ateInWorld w E.beans E.mary)

End-to-end: the compositional derivation produces the same truth values as the hand-defined propositions used to build the Hamblin question. At each world, the tree interp matches the hand-defined proposition.