Rooth 1992: A theory of focus interpretation

Formalises [Roo92] over the example rows in Data/Examples/Rooth1992.json: question-answer congruence via the focus interpretation principle (FIP, the paper's (27)), association with only ((26a), (30b)), the contrasting-phrases rule (14), and the argument that focus constrains rather than fixes the domain of only (the Recognitions example (7)).

The question-answer model is the paper's §2.4 paradigm — "Who cut Bill down to size?" answered by [Mary]F cut Bill down to size (23), with the alternative answers of (24) — in a four-world model crossing subjects {Mary, Monique} with objects {Bill, Björn}. The only model is the §2.1 introduction scenario (Mary introduced Bill and Tom to Sue). Focus values are computed, not stipulated: the interp engine that computes ordinary values at M = Id computes O/A-values at M = AltMeaning, grounding the stipulated Hamblin sets, and the lexicon's surface forms are checked against the English fragment entries.

The question-answer world model

inductive Rooth1992.QAWorld : Type

Worlds crossing cutter (Mary/Monique) × cuttee (Bill/Björn), after the answer columns of [Roo92] (24). Sufficient to distinguish subject-focus from object-focus alternative sets.

• maryBill : QAWorld
• maryBjorn : QAWorld
• moniqueBill : QAWorld
• moniqueBjorn : QAWorld

@[instance_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

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

@[instance_reducible]

instance Rooth1992.instReprQAWorld : Repr QAWorld

Equations

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

def Rooth1992.maryCutBill : Set QAWorld

"Mary cut Bill down to size" — true exactly at maryBill.

Equations

• Rooth1992.maryCutBill = {Rooth1992.QAWorld.maryBill}

def Rooth1992.moniqueCutBill : Set QAWorld

"Monique cut Bill down to size" — true exactly at moniqueBill.

Equations

• Rooth1992.moniqueCutBill = {Rooth1992.QAWorld.moniqueBill}

def Rooth1992.maryCutBjorn : Set QAWorld

"Mary cut Björn down to size" — true exactly at maryBjorn.

Equations

• Rooth1992.maryCutBjorn = {Rooth1992.QAWorld.maryBjorn}

Alternative meanings

def Rooth1992.altSubjectFocused : Alternatives.AltMeaning String

Focused [MARY]F in the answer [Mary]F cut Bill down to size ((23Aa) of [Roo92] §2.4): O-value = "Mary"; A-value = {"Mary", "Monique"}.

Equations

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

def Rooth1992.altPredicateUnfeatured : Alternatives.AltMeaning String

Non-focused "cut Bill down to size": singleton A-value. Exercises AltMeaning.unfeatured.

Equations

• Rooth1992.altPredicateUnfeatured = Alternatives.AltMeaning.unfeatured "cut Bill down to size"

theorem Rooth1992.unfeatured_preserves_oValue : altPredicateUnfeatured.oValue = "cut Bill down to size"

Unfeatured O-value equals the input.

theorem Rooth1992.unfeatured_singleton_aValue : altPredicateUnfeatured.aValue = ["cut Bill down to size"]

Unfeatured A-value is a singleton containing the O-value — "the focus semantic value of a focus-free phrase is the unit set of its ordinary semantic value" ([Roo92] (42)).

Question-answer congruence and the FIP

The question-answer constraint ((26d) of [Roo92] §3, motivated by the §2.4 question-answer paradigm): in a Q-A pair ⟨ψ, α⟩, ⟦ψ⟧° ⊆ ⟦α⟧f — the ordinary semantic value of the question is a subset of the focus semantic value of the answer. The FIP (27) schematizes this as Γ ⊆ ⟦α⟧f with Γ resolved to the question denotation.

def Rooth1992.q_whoCutBill : Focus.Interpretation.PropFocusValue QAWorld

"Who cut Bill down to size?" ((23Qa)) — Hamblin question with subject alternatives, the (25a) value restricted to the model's individuals.

Equations

• Rooth1992.q_whoCutBill = {Rooth1992.maryCutBill, Rooth1992.moniqueCutBill}

def Rooth1992.fv_subjectFocus : Focus.Interpretation.PropFocusValue QAWorld

Focus value of [MARY]F cut Bill down to size ((23Aa)) — same subject alternatives.

Equations

• Rooth1992.fv_subjectFocus = {Rooth1992.maryCutBill, Rooth1992.moniqueCutBill}

def Rooth1992.fv_objectFocus : Focus.Interpretation.PropFocusValue QAWorld

Focus value of Mary cut [BILL]F down to size ((23Ab)) — object alternatives (varies object, not subject).

Equations

• Rooth1992.fv_objectFocus = {Rooth1992.maryCutBill, Rooth1992.maryCutBjorn}

theorem Rooth1992.qa_subject_focus_congruent : Focus.Interpretation.qaCongruent fv_subjectFocus q_whoCutBill

Q-A congruence: subject focus value = question denotation.

theorem Rooth1992.fip_congruent : Focus.Interpretation.fip q_whoCutBill fv_subjectFocus

The FIP holds for subject focus: question alternatives ⊆ focus value — trivially, since the sets are equal.

theorem Rooth1992.moniqueCutBill_in_question : moniqueCutBill ∈ q_whoCutBill

"moniqueCutBill" is in the question alternatives...

theorem Rooth1992.moniqueCutBill_not_in_objectFocus : moniqueCutBill ∉ fv_objectFocus

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

theorem Rooth1992.fip_fails_object_focus : ¬Focus.Interpretation.fip q_whoCutBill fv_objectFocus

...so the FIP fails for object focus: (23Ab) is linked to (23Qa) only by a dotted (inappropriate) line in the paper's (23).

The question as focus antecedent

def Rooth1992.qaAntecedent : Focus.Antecedent QAWorld

'Who cut Bill down to size?' as a focus antecedent (Focus.Antecedent): the anaphoric source of the squiggle's contrast set.

Equations

• Rooth1992.qaAntecedent = Focus.Antecedent.question Rooth1992.q_whoCutBill

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

Question antecedents license the new-information use.

theorem Rooth1992.qaAntecedent_admits_subjectFocus : qaAntecedent.Admits fv_subjectFocus

The antecedent admits subject focus — the 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 maryCutBill fv_subjectFocus

The question antecedent fully resolves against the subject-focus meaning: all three clauses of the squiggle presupposition ([Roo92] (40) set case), not just the FIP — the contrast set contains the ordinary value maryCutBill and the distinct alternative moniqueCutBill.

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

A focus-free answer cannot resolve any antecedent: its focus value is the unit set of its ordinary value ((42)), defeating the contrast clause — "the argument must contain a focus".

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

Contrasting phrases ([Roo92] (14), on the symmetric-contrast joke opening (11)): construe α as contrasting with β if ⟦β⟧° ∈ ⟦α⟧f. Canadian farmer's ordinary value is a member of [American]F farmer's focus value distinct from its ordinary value.

Constraining vs fixing the domain of only

With a focused transitive verb — Mary only [read]F The Recognitions ((7) of [Roo92] §2.1) — the full focus value contains "even trivial relations", so [Roo85]'s move of fixing only's domain C to it yields unsatisfiable truth conditions, while intuitively (7) can be true. The 1992 revision (9c) merely constrains C ⊆ ⟦VP⟧f, leaving C to pragmatics: it "might be quite a small set", e.g. {read(c), understand(c)} ((37c)). A lexically carried alternative list cannot be narrowed this way.

inductive Rooth1992.RWorld : Type

Worlds tracking Mary's relation to The Recognitions.

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

@[instance_reducible]

instance Rooth1992.instDecidableEqRWorld : DecidableEq RWorld

Equations

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

@[instance_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 ∈ Focus.onlyVia {reading, grasping} reading

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

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

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

theorem Rooth1992.lexical_only_unsatisfiable : Focus.Particles.onlyAssertion [grasping, trivialR] = ∅

The same over-generation on the lexical semantics of only: with the full focus value carried as a lexical alternative list, the assertion is unsatisfiable, and no pragmatic narrowing is possible — the list is fixed in the lexical entry.

Association with only

The focusing adverb constraint ((26a) of [Roo92] §3): the domain of quantification C of a focusing adverb with argument α satisfies C ⊆ ⟦α⟧f. The lexical semantics (30b) is ∀P[P ∈ C ∧ P(m) → P = VP']. The model is the §2.1 introduction scenario: Mary introduced Bill and Tom to Sue, and there were no other introductions — so Mary only introduced [Bill]F to Sue (3a) is false.

inductive Rooth1992.OnlyWorld : Type

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

• billOnly : OnlyWorld
• tomOnly : OnlyWorld
• both : OnlyWorld

@[instance_reducible]

instance Rooth1992.instDecidableEqOnlyWorld : DecidableEq OnlyWorld

Equations

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

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✝

@[instance_reducible]

instance Rooth1992.instReprOnlyWorld : Repr OnlyWorld

Equations

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

def Rooth1992.introBill : OnlyWorld → Bool

"Mary introduced Bill to Sue"

Equations

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

def Rooth1992.introTom : OnlyWorld → Bool

"Mary introduced Tom to Sue"

Equations

• Rooth1992.introTom Rooth1992.OnlyWorld.billOnly = false
• Rooth1992.introTom Rooth1992.OnlyWorld.tomOnly = true
• Rooth1992.introTom Rooth1992.OnlyWorld.both = true

def Rooth1992.altBillFocused : Alternatives.AltMeaning (OnlyWorld → Bool)

Focus on BILL ((3a)): O-value = introBill; A-value = {introBill, introTom}. Focus constrains the domain of only.

Equations

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

def Rooth1992.onlyBill : OnlyWorld → Bool

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

Equations

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

def Rooth1992.onlyTom : OnlyWorld → Bool

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

Equations

• Rooth1992.onlyTom Rooth1992.OnlyWorld.tomOnly = true
• Rooth1992.onlyTom x✝ = false

theorem Rooth1992.only_bill_semantics (w : OnlyWorld) : onlyBill w = (introBill w && !introTom w)

Only with focus on BILL: the prejacent holds and all non-actual alternatives are excluded ((30b)).

theorem Rooth1992.only_tom_semantics (w : OnlyWorld) : onlyTom w = (introTom w && !introBill w)

Only with focus on TOM: symmetric case.

theorem Rooth1992.only_focus_determines_meaning : onlyBill ≠ onlyTom

Different domains → different only meanings. (The paper's minimal pair (3a)/(3b) varies focus between Bill and Sue; the model exhibits the domain-dependence on the introducee axis.)

Data rows

The rows (Data/Examples/Rooth1992.json) record the paper's (23): "MARY cut Bill down to size" is congruent and "#Mary cut BILL down to size" incongruent with "Who cut Bill down to size?", and focus determines what only excludes ((3a)/(3b)). The theory explains both: subject focus produces a focus value equal to the question denotation (fip_congruent), object focus one that excludes a question alternative (fip_fails_object_focus); and the FIP constrains the domain C of only, 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 ("Mary") evokes the subject-alternative focus value, object focus ("Bill") the object-alternative one.

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 cut Bill down to size?" ([Roo92] (26d)).

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 ≠ onlyTom

Bridge: the focusing-adverb rows differ only in focus position ((3a) vs (3b)), and the theory maps distinct domains to distinct only meanings.

Montague lexicon and trees

The propositions above were hand-defined. Here they are derived compositionally: entity denotations + a world-indexed verb meaning are combined via Heim & Kratzer's interp, run once per world. The particle-verb cut … down to size is treated as a single transitive lexical item keyed "cut".

inductive Rooth1992.E : Type

Entity domain for the focus model.

• mary : E
• monique : E
• bill : E
• bjorn : E

@[instance_reducible]

instance Rooth1992.instDecidableEqE : DecidableEq E

Equations

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

@[instance_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.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.monique prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.E.monique")).group prec✝
• Rooth1992.instReprE.repr Rooth1992.E.bill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.E.bill")).group prec✝
• Rooth1992.instReprE.repr Rooth1992.E.bjorn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.E.bjorn")).group prec✝

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

World-indexed verb semantics for "cut (down to size)". cutInWorld w obj subj follows Montague's argument order (object first, then subject).

Equations

• Rooth1992.cutInWorld Rooth1992.QAWorld.maryBill Rooth1992.E.bill Rooth1992.E.mary = True
• Rooth1992.cutInWorld Rooth1992.QAWorld.maryBjorn Rooth1992.E.bjorn Rooth1992.E.mary = True
• Rooth1992.cutInWorld Rooth1992.QAWorld.moniqueBill Rooth1992.E.bill Rooth1992.E.monique = True
• Rooth1992.cutInWorld Rooth1992.QAWorld.moniqueBjorn Rooth1992.E.bjorn Rooth1992.E.monique = True
• Rooth1992.cutInWorld 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 "Mary" = some { ty := Intensional.Ty.e, denot := Rooth1992.E.mary }
• Rooth1992.focusLex w "Monique" = some { ty := Intensional.Ty.e, denot := Rooth1992.E.monique }
• Rooth1992.focusLex w "cut" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t, denot := Rooth1992.cutInWorld w }
• Rooth1992.focusLex w "Bill" = some { ty := Intensional.Ty.e, denot := Rooth1992.E.bill }
• Rooth1992.focusLex w "Björn" = some { ty := Intensional.Ty.e, denot := Rooth1992.E.bjorn }
• Rooth1992.focusLex w word = none

def Rooth1992.tree_maryCutBill : Syntax.Tree Unit String

Syntax tree: [S [NP Mary] [VP [V cut] [NP Bill]]]

Equations

• Rooth1992.tree_maryCutBill = (Syntax.Tree.leaf "Mary").bin ((Syntax.Tree.leaf "cut").bin (Syntax.Tree.leaf "Bill"))

def Rooth1992.tree_moniqueCutBill : Syntax.Tree Unit String

Syntax tree: [S [NP Monique] [VP [V cut] [NP Bill]]]

Equations

• Rooth1992.tree_moniqueCutBill = (Syntax.Tree.leaf "Monique").bin ((Syntax.Tree.leaf "cut").bin (Syntax.Tree.leaf "Bill"))

def Rooth1992.tree_maryCutBjorn : Syntax.Tree Unit String

Syntax tree: [S [NP Mary] [VP [V cut] [NP Björn]]]

Equations

• Rooth1992.tree_maryCutBjorn = (Syntax.Tree.leaf "Mary").bin ((Syntax.Tree.leaf "cut").bin (Syntax.Tree.leaf "Björn"))

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

Grounding the stipulated propositions

def Rooth1992.maryCutBill_comp : QAWorld → Prop

Compositionally derived "Mary cut Bill" proposition.

Equations

• Rooth1992.maryCutBill_comp w = (Rooth1992.treeResult (Rooth1992.focusLex w) Rooth1992.tree_maryCutBill).getD False

def Rooth1992.moniqueCutBill_comp : QAWorld → Prop

Compositionally derived "Monique cut Bill" proposition.

Equations

• Rooth1992.moniqueCutBill_comp w = (Rooth1992.treeResult (Rooth1992.focusLex w) Rooth1992.tree_moniqueCutBill).getD False

def Rooth1992.maryCutBjorn_comp : QAWorld → Prop

Compositionally derived "Mary cut Björn" proposition.

Equations

• Rooth1992.maryCutBjorn_comp w = (Rooth1992.treeResult (Rooth1992.focusLex w) Rooth1992.tree_maryCutBjorn).getD False

theorem Rooth1992.direct_eq_interp (w : QAWorld) : treeResult (focusLex w) tree_maryCutBill = some (cutInWorld w E.bill E.mary)

Direct function application matches tree interpretation.

theorem Rooth1992.comp_grounds_maryCutBill : maryCutBill_comp = fun (w : QAWorld) => cutInWorld w E.bill E.mary

Grounding: compositional "Mary cut Bill" agrees with the hand-defined proposition at each world.

theorem Rooth1992.comp_grounds_moniqueCutBill : moniqueCutBill_comp = fun (w : QAWorld) => cutInWorld w E.bill E.monique

Grounding: compositional "Monique cut Bill" = direct application.

theorem Rooth1992.comp_grounds_maryCutBjorn : maryCutBjorn_comp = fun (w : QAWorld) => cutInWorld w E.bjorn E.mary

Grounding: compositional "Mary cut Björn" = direct application.

The focus dimension through the engine

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.

@[instance_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 [Mary]F, whose entry carries the subject alternatives.

Equations

• Rooth1992.focusLexF w "Mary" = some { ty := Intensional.Ty.e, denot := { oValue := Rooth1992.E.mary, aValue := [Rooth1992.E.mary, Rooth1992.E.monique] } }
• 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_maryCutBill (w : QAWorld) : treeResultF (focusLexF w) tree_maryCutBill = some { oValue := cutInWorld w E.bill E.mary, aValue := [cutInWorld w E.bill E.mary, cutInWorld w E.bill E.monique] }

The engine at M = AltMeaning computes the two-dimensional meaning of [MARY]F cut Bill down to size: 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_maryCutBill) = treeResult (focusLex w) tree_maryCutBill

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

theorem Rooth1992.fv_subjectFocus_computed : fv_subjectFocus = {{w : QAWorld | cutInWorld w E.bill E.mary}, {w : QAWorld | cutInWorld w E.bill E.monique}}

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

Fragment connection

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

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

Mary is a proper name in the English fragment.

theorem Rooth1992.fragment_bill_proper : English.Nouns.bill.proper = true

Bill is a proper name in the English fragment.

theorem Rooth1992.fragment_mary_in_lexicon : (focusLex QAWorld.maryBill English.Nouns.mary.formSg).isSome = true

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

theorem Rooth1992.fragment_bill_in_lexicon : (focusLex QAWorld.maryBill English.Nouns.bill.formSg).isSome = true

theorem Rooth1992.fragment_cut_transitive : English.Predicates.Verbal.cut.frames = [Frame.np]

"cut" is transitive (NP frame).

theorem Rooth1992.fragment_cut_past_form : English.Predicates.Verbal.cut.formPast = "cut"

"cut" has (irregular) past tense "cut" matching the lexicon key.

theorem Rooth1992.fragment_cut_past_in_lexicon : (focusLex QAWorld.maryBill English.Predicates.Verbal.cut.formPast).isSome = true

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

End to end

theorem Rooth1992.endToEnd_question_grounded : (∀ (w : QAWorld), treeResult (focusLex w) tree_maryCutBill = some (cutInWorld w E.bill E.mary)) ∧ ∀ (w : QAWorld), treeResult (focusLex w) tree_moniqueCutBill = some (cutInWorld w E.bill E.monique)

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