Alternative-semantics focus interpretation

Formalises [Roo92] over the example rows in Data/Examples/Rooth1992.json and 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)
• fipPrediction — row adapter over Data/Examples/Rooth1992.json (§8)
• Tree, interp — compositional derivation (§10–§11)
• Derivation — derivation bundles (§13)
• English.Nouns, .Predicates.Verbal — fragment entries (§14)

inductive Rooth1992.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 Rooth1992.instDecidableEqQAWorld : DecidableEq QAWorld

Equations

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

def Rooth1992.instReprQAWorld.repr : QAWorld → ℕ → Std.Format

Equations

• Rooth1992.instReprQAWorld.repr Rooth1992.QAWorld.fredBeans prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.QAWorld.fredBeans")).group prec✝
• Rooth1992.instReprQAWorld.repr Rooth1992.QAWorld.fredRice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.QAWorld.fredRice")).group prec✝
• Rooth1992.instReprQAWorld.repr Rooth1992.QAWorld.maryBeans prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.QAWorld.maryBeans")).group prec✝
• Rooth1992.instReprQAWorld.repr Rooth1992.QAWorld.maryRice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.QAWorld.maryRice")).group prec✝

@[implicit_reducible]

instance Rooth1992.instReprQAWorld : Repr QAWorld

Equations

• Rooth1992.instReprQAWorld = { reprPrec := Rooth1992.instReprQAWorld.repr }

def Rooth1992.fredAteBeans : Set QAWorld

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

Equations

• Rooth1992.fredAteBeans = {Rooth1992.QAWorld.fredBeans}

def Rooth1992.maryAteBeans : Set QAWorld

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

Equations

• Rooth1992.maryAteBeans = {Rooth1992.QAWorld.maryBeans}

def Rooth1992.fredAteRice : Set QAWorld

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

Equations

• Rooth1992.fredAteRice = {Rooth1992.QAWorld.fredRice}

def Rooth1992.altSubjectFocused : Alternatives.AltMeaning String

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

Equations

• Rooth1992.altSubjectFocused = { oValue := "Fred", aValue := ["Fred", "Mary"] }

def Rooth1992.altPredicateUnfeatured : Alternatives.AltMeaning String

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

Equations

• Rooth1992.altPredicateUnfeatured = Alternatives.AltMeaning.unfeatured "ate the beans"

theorem Rooth1992.unfeatured_preserves_oValue : altPredicateUnfeatured.oValue = "ate the beans"

Unfeatured O-value equals the input.

theorem Rooth1992.unfeatured_singleton_aValue : altPredicateUnfeatured.aValue = ["ate the beans"]

Unfeatured A-value is a singleton containing the O-value. Non-focused expressions evoke no alternatives ([Roo92] §1).

def Rooth1992.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

• Rooth1992.qaFocus = { focused := "Fred", alternatives := ["Fred", "Mary"] }

def Rooth1992.qaBackground : Features.InformationStructure.Background String

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

Equations

• Rooth1992.qaBackground = { elements := ["ate", "the", "beans"] }

def Rooth1992.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

• Rooth1992.qaTheme = { content := "λx. x ate the beans" }

def Rooth1992.qaRheme : Features.InformationStructure.Rheme String

Rheme: the answer "Fred".

Equations

• Rooth1992.qaRheme = { content := "Fred" }

def Rooth1992.qaInfo : Features.InformationStructure.InfoStructure String

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

Equations

• Rooth1992.qaInfo = { theme := Rooth1992.qaTheme, rheme := Rooth1992.qaRheme, foci := ["Fred"], background := ["ate", "the", "beans"] }

theorem Rooth1992.qa_theme_content : qaInfo.theme.content = "λx. x ate the beans"

Theme carries the presupposed content.

theorem Rooth1992.qa_rheme_content : qaInfo.rheme.content = "Fred"

Rheme carries the asserted answer.

theorem Rooth1992.qa_foci_match : qaInfo.foci = [qaFocus.focused]

Focus list matches the focused element.

theorem Rooth1992.qa_background_match : qaInfo.background = qaBackground.elements

Background list matches the background elements.

structure Rooth1992.FocusedSentence : Type

Minimal derivation type for exercising the IS partition. Pairs a focused constituent with background material.

• focusedWord : String
• backgroundWords : List String

@[implicit_reducible]

instance Rooth1992.instReprFocusedSentence : Repr FocusedSentence

Equations

• Rooth1992.instReprFocusedSentence = { reprPrec := Rooth1992.instReprFocusedSentence.repr }

def Rooth1992.instReprFocusedSentence.repr : FocusedSentence → ℕ → Std.Format

Equations

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

def Rooth1992.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 Rooth1992.fredSentence : FocusedSentence

Equations

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

theorem Rooth1992.infoStructure_extracts_focus : fredSentence.infoStructure.foci = ["Fred"]

The extractor correctly puts the focused word in foci.

theorem Rooth1992.infoStructure_extracts_background : fredSentence.infoStructure.background = ["ate", "the", "beans"]

The extractor correctly puts background words in background.

[Roo92] §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 Rooth1992.q_whoAteBeans : Semantics.Focus.Interpretation.PropFocusValue QAWorld

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

Equations

• Rooth1992.q_whoAteBeans = {Rooth1992.fredAteBeans, Rooth1992.maryAteBeans}

def Rooth1992.fv_subjectFocus : Semantics.Focus.Interpretation.PropFocusValue QAWorld

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

Equations

• Rooth1992.fv_subjectFocus = {Rooth1992.fredAteBeans, Rooth1992.maryAteBeans}

def Rooth1992.fv_objectFocus : Semantics.Focus.Interpretation.PropFocusValue QAWorld

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

Equations

• Rooth1992.fv_objectFocus = {Rooth1992.fredAteBeans, Rooth1992.fredAteRice}

theorem Rooth1992.qa_subject_focus_congruent : Semantics.Focus.Interpretation.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 Rooth1992.fip_congruent : Semantics.Focus.Interpretation.fip q_whoAteBeans fv_subjectFocus

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

theorem Rooth1992.maryAteBeans_in_question : maryAteBeans ∈ q_whoAteBeans

"maryAteBeans" is in the question alternatives...

theorem Rooth1992.maryAteBeans_not_in_objectFocus : maryAteBeans ∉ fv_objectFocus

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

theorem Rooth1992.fip_fails_object_focus : ¬Semantics.Focus.Interpretation.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?"

def Rooth1992.qaAntecedent : Semantics.Focus.Antecedent QAWorld

'Who ate the beans?' as a focus antecedent (Semantics.Focus.Antecedent): the anaphoric source of the squiggle's contrast set.

Equations

• Rooth1992.qaAntecedent = Semantics.Focus.Antecedent.question Rooth1992.q_whoAteBeans

theorem Rooth1992.qaAntecedent_use : qaAntecedent.use = Semantics.Focus.Use.newInfo

Question antecedents license the new-information use.

theorem Rooth1992.qaAntecedent_admits_subjectFocus : qaAntecedent.Admits fv_subjectFocus

The antecedent admits subject focus — FIP routed through the antecedent layer.

theorem Rooth1992.qaAntecedent_rejects_objectFocus : ¬qaAntecedent.Admits fv_objectFocus

The antecedent rejects object focus.

theorem Rooth1992.qaAntecedent_resolves : qaAntecedent.Resolves fredAteBeans fv_subjectFocus

The question antecedent fully resolves against the subject-focus meaning: all three clauses of the squiggle presupposition, not just FIP — the contrast set contains the ordinary value fredAteBeans and the distinct alternative maryAteBeans.

theorem Rooth1992.focusFree_answer_cannot_resolve (Γ : Semantics.Focus.Interpretation.PropFocusValue QAWorld) : ¬Semantics.Focus.SquiggleSet fredAteBeans {fredAteBeans} Γ

A focus-free answer cannot resolve any antecedent: its focus value is the unit set {fredAteBeans}, defeating the contrast clause — "the argument must contain a focus".

theorem Rooth1992.farmer_contrast : Semantics.Focus.SquiggleInd "American farmer" {"American farmer", "Canadian farmer"} "Canadian farmer"

Contrasting phrases (Rooth's symmetric-contrast joke opening, his rule construing α as contrasting with β via ⟦β⟧ᵒ ∈ ⟦α⟧f): Canadian farmer's ordinary value is a member of [American]F farmer's focus value distinct from its ordinary value.

With a focused transitive verb, the full focus value contains "even trivial relations", so fixing only's domain to it yields unsatisfiable truth conditions — while intuitively Mary only READ The Recognitions can be true. The strong theory's separately resolved C "might be quite a small set"; a lexically carried alternative list cannot be pragmatically narrowed.

inductive Rooth1992.RWorld : Type

Worlds tracking Mary's relation to The Recognitions.

• readOnly : RWorld
• readAndGrasp : RWorld
• neither : RWorld

@[implicit_reducible]

instance Rooth1992.instDecidableEqRWorld : DecidableEq RWorld

Equations

• Rooth1992.instDecidableEqRWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Rooth1992.instReprRWorld : Repr RWorld

Equations

• Rooth1992.instReprRWorld = { reprPrec := Rooth1992.instReprRWorld.repr }

def Rooth1992.instReprRWorld.repr : RWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Rooth1992.instReprRWorld.repr Rooth1992.RWorld.readOnly prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.RWorld.readOnly")).group prec✝
• Rooth1992.instReprRWorld.repr Rooth1992.RWorld.neither prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.RWorld.neither")).group prec✝

def Rooth1992.reading : Set RWorld

'reading The Recognitions'.

Equations

• Rooth1992.reading = {Rooth1992.RWorld.readOnly, Rooth1992.RWorld.readAndGrasp}

def Rooth1992.grasping : Set RWorld

'understanding The Recognitions'.

Equations

• Rooth1992.grasping = {Rooth1992.RWorld.readAndGrasp}

def Rooth1992.trivialR : Set RWorld

A trivial property of the same semantic type — a member of the full focus value.

Equations

• Rooth1992.trivialR = Set.univ

theorem Rooth1992.restricted_only_satisfiable : RWorld.readOnly ∈ Semantics.Focus.onlyVia {reading, grasping} reading

With the pragmatically restricted domain, only READ is satisfiable: true where Mary read without understanding.

theorem Rooth1992.direct_only_unsatisfiable : Semantics.Focus.onlyVia {reading, grasping, trivialR} reading = ∅

With the domain fixed to the full focus value (trivial property included), only READ is unsatisfiable — direct association over-generates exclusions.

theorem Rooth1992.traditional_only_unsatisfiable (w : RWorld) : { prejacent := Rooth1992.readingB✝, alternatives := [Rooth1992.graspingB✝, Rooth1992.trivialB✝] }.assertion w = false

The direct-association operator with its lexically carried full alternative list is the same over-generation, exhibited on TraditionalOnly itself: its assertion is everywhere false in this model. No pragmatic narrowing is possible — the list is fixed in the lexical entry, which is the strong theory's objection.

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 Rooth1992.OnlyWorld : Type

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

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

@[implicit_reducible]

instance Rooth1992.instDecidableEqOnlyWorld : DecidableEq OnlyWorld

Equations

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

@[implicit_reducible]

instance Rooth1992.instReprOnlyWorld : Repr OnlyWorld

Equations

• Rooth1992.instReprOnlyWorld = { reprPrec := Rooth1992.instReprOnlyWorld.repr }

def Rooth1992.instReprOnlyWorld.repr : OnlyWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Rooth1992.instReprOnlyWorld.repr Rooth1992.OnlyWorld.both prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.OnlyWorld.both")).group prec✝

def Rooth1992.onlyWorlds : List OnlyWorld

Equations

• Rooth1992.onlyWorlds = [Rooth1992.OnlyWorld.billOnly, Rooth1992.OnlyWorld.johnOnly, Rooth1992.OnlyWorld.both]

def Rooth1992.introBill : OnlyWorld → Bool

"Mary introduced Bill to Sue"

Equations

• Rooth1992.introBill Rooth1992.OnlyWorld.billOnly = true
• Rooth1992.introBill Rooth1992.OnlyWorld.johnOnly = false
• Rooth1992.introBill Rooth1992.OnlyWorld.both = true

def Rooth1992.introJohn : OnlyWorld → Bool

"Mary introduced John to Sue"

Equations

• Rooth1992.introJohn Rooth1992.OnlyWorld.billOnly = false
• Rooth1992.introJohn Rooth1992.OnlyWorld.johnOnly = true
• Rooth1992.introJohn Rooth1992.OnlyWorld.both = true

def Rooth1992.altBillFocused : 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

• Rooth1992.altBillFocused = { oValue := Rooth1992.introBill, aValue := [Rooth1992.introBill, Rooth1992.introJohn] }

def Rooth1992.onlyBill : OnlyWorld → Bool

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

Equations

• Rooth1992.onlyBill Rooth1992.OnlyWorld.billOnly = true
• Rooth1992.onlyBill x✝ = false

def Rooth1992.onlyJohn : OnlyWorld → Bool

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

Equations

• Rooth1992.onlyJohn Rooth1992.OnlyWorld.johnOnly = true
• Rooth1992.onlyJohn x✝ = false

theorem Rooth1992.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 Rooth1992.only_john_semantics : (onlyWorlds.all fun (w : OnlyWorld) => onlyJohn w == (introJohn w && !introBill w)) = true

"Only" with focus on JOHN: symmetric case.

theorem Rooth1992.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).

The rows (Data/Examples/Rooth1992.json) record that "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 rows say 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. 

def Rooth1992.fipPrediction (row : Data.Examples.LinguisticExample) : Prop

The FIP prediction for a row, read off its focus feature: subject focus ("Fred") evokes the subject-alternative focus value, object focus ("beans") the object-alternative one (§6).

Equations

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

theorem Rooth1992.qa_acceptable_iff_fip (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.feature? "fip_application" = some "qaCongruence" → (row.judgment = Features.Judgment.acceptable ↔ fipPrediction row)

Transfer: a Q-A row is acceptable iff its focus value satisfies the FIP against "Who ate the beans?" ([Roo92] (26d)). Subject focus passes (§6a); object focus fails (§6b).

theorem Rooth1992.focusingAdverb_rows_differ_in_focus (r₁ : Data.Examples.LinguisticExample) : r₁ ∈ Examples.all → ∀ r₂ ∈ Examples.all, r₁.feature? "fip_application" = some "focusingAdverb" → r₂.feature? "fip_application" = some "focusingAdverb" → r₁.id ≠ r₂.id → r₁.feature? "focus" ≠ r₂.feature? "focus"

Distinct focusing-adverb rows carry distinct focus features: the rows form an association-with-focus minimal pair.

theorem Rooth1992.bridge_only_association : Examples.only_bill.feature? "focus" ≠ Examples.only_sue.feature? "focus" ∧ onlyBill ≠ onlyJohn

Bridge: the focusing-adverb rows differ only in focus position, and the theory maps distinct focus positions to distinct "only" meanings (§7).

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 Rooth1992.E : Type

Entity domain for the focus model.

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

@[implicit_reducible]

instance Rooth1992.instDecidableEqE : DecidableEq E

Equations

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

@[implicit_reducible]

instance Rooth1992.instReprE : Repr E

Equations

• Rooth1992.instReprE = { reprPrec := Rooth1992.instReprE.repr }

def Rooth1992.instReprE.repr : E → ℕ → Std.Format

Equations

• Rooth1992.instReprE.repr Rooth1992.E.fred prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.E.fred")).group prec✝
• Rooth1992.instReprE.repr Rooth1992.E.mary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.E.mary")).group prec✝
• Rooth1992.instReprE.repr Rooth1992.E.beans prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.E.beans")).group prec✝
• Rooth1992.instReprE.repr Rooth1992.E.rice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.E.rice")).group prec✝

def Rooth1992.ateInWorld (w : QAWorld) : Intensional.Denot E Unit (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)

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

Equations

• Rooth1992.ateInWorld Rooth1992.QAWorld.fredBeans Rooth1992.E.beans Rooth1992.E.fred = True
• Rooth1992.ateInWorld Rooth1992.QAWorld.fredRice Rooth1992.E.rice Rooth1992.E.fred = True
• Rooth1992.ateInWorld Rooth1992.QAWorld.maryBeans Rooth1992.E.beans Rooth1992.E.mary = True
• Rooth1992.ateInWorld Rooth1992.QAWorld.maryRice Rooth1992.E.rice Rooth1992.E.mary = True
• Rooth1992.ateInWorld w obj subj = False

def Rooth1992.focusLex (w : QAWorld) : Semantics.Montague.Lexicon E Unit

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

Equations

• Rooth1992.focusLex w "Fred" = some { ty := Intensional.Ty.e, denot := Rooth1992.E.fred }
• Rooth1992.focusLex w "Mary" = some { ty := Intensional.Ty.e, denot := Rooth1992.E.mary }
• Rooth1992.focusLex w "ate" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t, denot := Rooth1992.ateInWorld w }
• Rooth1992.focusLex w "beans" = some { ty := Intensional.Ty.e, denot := Rooth1992.E.beans }
• Rooth1992.focusLex w "rice" = some { ty := Intensional.Ty.e, denot := Rooth1992.E.rice }
• Rooth1992.focusLex w word = none

def Rooth1992.tree_fredAteBeans : Syntax.Tree Unit String

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

Equations

• Rooth1992.tree_fredAteBeans = (Syntax.Tree.leaf "Fred").bin ((Syntax.Tree.leaf "ate").bin (Syntax.Tree.leaf "beans"))

def Rooth1992.tree_maryAteBeans : Syntax.Tree Unit String

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

Equations

• Rooth1992.tree_maryAteBeans = (Syntax.Tree.leaf "Mary").bin ((Syntax.Tree.leaf "ate").bin (Syntax.Tree.leaf "beans"))

def Rooth1992.tree_fredAteRice : Syntax.Tree Unit String

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

Equations

• Rooth1992.tree_fredAteRice = (Syntax.Tree.leaf "Fred").bin ((Syntax.Tree.leaf "ate").bin (Syntax.Tree.leaf "rice"))

def Rooth1992.treeResult (lex : Semantics.Montague.Lexicon E Unit) (t : Syntax.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

• Rooth1992.treeResult lex t = match Semantics.Composition.Tree.interp Rooth1992.E Unit lex Rooth1992.g₀✝ t with | some { ty := Intensional.Ty.t, val := p } => some p | x => none

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

def Rooth1992.fredAteBeans_comp : QAWorld → Prop

Compositionally derived "Fred ate beans" proposition.

Equations

• Rooth1992.fredAteBeans_comp w = (Rooth1992.treeResult (Rooth1992.focusLex w) Rooth1992.tree_fredAteBeans).getD False

def Rooth1992.maryAteBeans_comp : QAWorld → Prop

Compositionally derived "Mary ate beans" proposition.

Equations

• Rooth1992.maryAteBeans_comp w = (Rooth1992.treeResult (Rooth1992.focusLex w) Rooth1992.tree_maryAteBeans).getD False

def Rooth1992.fredAteRice_comp : QAWorld → Prop

Compositionally derived "Fred ate rice" proposition.

Equations

• Rooth1992.fredAteRice_comp w = (Rooth1992.treeResult (Rooth1992.focusLex w) Rooth1992.tree_fredAteRice).getD False

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

Direct function application matches tree interpretation.

theorem Rooth1992.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 Rooth1992.comp_grounds_maryAteBeans : maryAteBeans_comp = fun (w : QAWorld) => ateInWorld w E.beans E.mary

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

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

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

F-marking is a non-pure lexicon entry: the same interp that computes ordinary values at M = Id computes focus values at M = AltMeaning (pure = AltMeaning.unfeatured lifts the focus-free entries), with applyForward's <*> doing Hamblin functional application.

@[implicit_reducible]

instance Rooth1992.instPredAbsAltMeaning (E W : Type) : Semantics.Composition.Tree.PredAbs Alternatives.AltMeaning E W

Alternatives do not distribute through predicate abstraction — the honest none.

Equations

• Rooth1992.instPredAbsAltMeaning E W = { dist? := none }

def Rooth1992.focusLexF (w : QAWorld) : Semantics.Montague.Lexicon E Unit Alternatives.AltMeaning

The focus lexicon at M = AltMeaning: every entry pure-lifts except focused [Fred]F, whose entry carries the subject alternatives.

Equations

• Rooth1992.focusLexF w "Fred" = some { ty := Intensional.Ty.e, denot := { oValue := Rooth1992.E.fred, aValue := [Rooth1992.E.fred, Rooth1992.E.mary] } }
• Rooth1992.focusLexF w word = Semantics.Montague.Lexicon.lift Alternatives.AltMeaning (Rooth1992.focusLex w) word

def Rooth1992.treeResultF (lex : Semantics.Montague.Lexicon E Unit Alternatives.AltMeaning) (t : Syntax.Tree Unit String) : Option (Alternatives.AltMeaning Prop)

Focus-dimension tree interpretation.

Equations

• Rooth1992.treeResultF lex t = match Semantics.Composition.Tree.interp Rooth1992.E Unit lex Rooth1992.g₀✝ t with | some { ty := Intensional.Ty.t, val := p } => some p | x => none

theorem Rooth1992.treeResultF_fredAteBeans (w : QAWorld) : treeResultF (focusLexF w) tree_fredAteBeans = some { oValue := ateInWorld w E.beans E.fred, aValue := [ateInWorld w E.beans E.fred, ateInWorld w E.beans E.mary] }

The engine at M = AltMeaning computes the two-dimensional meaning of [FRED]F ate the beans: the O-value is the ordinary interpretation and the A-value is the subject-alternative family — the focus value is computed, not stipulated.

theorem Rooth1992.treeResultF_oValue (w : QAWorld) : Option.map (fun (x : Alternatives.AltMeaning Prop) => x.oValue) (treeResultF (focusLexF w) tree_fredAteBeans) = treeResult (focusLex w) tree_fredAteBeans

O-projection through the engine: mapping oValue over the AltMeaning run recovers the Id run.

theorem Rooth1992.fv_subjectFocus_computed : fv_subjectFocus = {{w : QAWorld | ateInWorld w E.beans E.fred}, {w : QAWorld | ateInWorld w E.beans E.mary}}

The stipulated fv_subjectFocus of §6 is exactly the engine's computed alternative family, read as proposition sets.

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 Rooth1992.fragment_fred_proper : English.Nouns.fred.proper = true

Fred is a proper name in the English fragment.

theorem Rooth1992.fragment_mary_proper : English.Nouns.mary.proper = true

Mary is a proper name in the English fragment.

theorem Rooth1992.fragment_bean_countable : English.Nouns.bean.countable = MassCount.count

"bean" is countable in the English fragment.

theorem Rooth1992.fragment_fred_in_lexicon : (focusLex QAWorld.fredBeans 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 Rooth1992.fragment_mary_in_lexicon : (focusLex QAWorld.fredBeans English.Nouns.mary.formSg).isSome = true

theorem Rooth1992.fragment_bean_pl_in_lexicon : (focusLex QAWorld.fredBeans (English.Nouns.bean.formPl.getD "")).isSome = true

theorem Rooth1992.fragment_eat_transitive : English.Predicates.Verbal.eat.complementType = ComplementType.np

"eat" is transitive (NP complement).

theorem Rooth1992.fragment_eat_past_form : English.Predicates.Verbal.eat.formPast = "ate"

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

theorem Rooth1992.fragment_eat_past_in_lexicon : (focusLex QAWorld.fredBeans 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 Rooth1992.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.