Rooth (1992): A theory of focus interpretation

Rooth unifies the effects of intonational focus. Alternative semantics gives a phrase a focus semantic value beside its ordinary one, the set of substitution instances at the focused position, computed here by mapping a predicate over an F-marked constituent whose alternatives are the whole domain (WithAlternatives.focused). Association with only, contrasting phrases, scalar implicature and question-answer congruence each require some object to be a subset or an element of a focus semantic value, and the focus interpretation principle keeps only that requirement: the operator ~ presupposes Focus.SquiggleSet or Focus.SquiggleInd of a free variable whose antecedent is a Focus.Antecedent.

Main results

• three_a, three_b, only_rows: only over a domain constrained by focus gives (3a) and (3b) their truth values.
• recognitions_fixed, recognitions_constrained: the domain is constrained rather than fixed, since the full focus semantic value of a focused verb contains the trivial relation.
• verbFocus_scale, ace_notMem_subjectFocus, roommate_implicature: focus on the verb licenses the acing scale that focus on the subject does not, and the group scale yields the roommate implicature.
• question_resolves_subjectFocus, question_rejects_objectFocus, qa_rows: a question admits the answer whose focus semantic value contains it.
• ellipsis_filter: in bare remnant ellipsis focus filters a compositional ambiguity, each correlate finding an antecedent for ~ under exactly one focus placement.

Implementation notes

• Worlds of the relational models are sets of atomic facts, so that distinct facts denote distinct propositions; the quiz model assigns each person a grade, acing entailing passing, with groups as finite sets of people.
• The rows carry the paper's examples with the truth values of the introduction scenario and the question-answer judgments, which the theorems derive. A row's focus position marks the arguments of its predication, and its focus semantic value is their composition (WithAlternatives.map₂).
• Only is the substrate's exclusive assertion on the identity scale, Focus.Particles.atMost (· = ·), which is (4b) with the equation reversed. Footnote 2 leaves open whether the prejacent belongs in the presupposition or the assertion, and suggests that the property may only need to be the strongest in the domain, the entailment scale.

References

• [Roo92]
• [Roo85]
• [Ham73]
• [Sau04]

Focus semantic values (2)

theorem Rooth1992.atMost_eq_empty_of_univ_mem {W : Type u_1} {C : Set (Set W)} {p : Set W} (hC : Set.univ ∈ C) (hp : p ≠ Set.univ) : Focus.Particles.atMost (fun (x1 x2 : Set W) => x1 = x2) C p = ∅

A domain containing the trivial proposition makes only unsatisfiable for any other prejacent.

Relational models

A world is a set of atomic facts and a fact denotes the proposition that it holds.

def Rooth1992.atom {A : Type} (a : A) : Set (Set A)

The proposition that the fact a holds.

Equations

• Rooth1992.atom a = {w : Set A | a ∈ w}

@[simp]

theorem Rooth1992.mem_atom {A : Type} {a : A} {w : Set A} : w ∈ atom a ↔ a ∈ w

theorem Rooth1992.atom_injective {A : Type} : Function.Injective atom

theorem Rooth1992.atom_ne_univ {A : Type} (a : A) : atom a ≠ Set.univ

Focusing adverbs (§2.1)

Only quantifies over a domain C of properties: if Mary has a property in C, it is the one the VP expresses ((4b), (30b)). Focus constrains C to lie inside the focus semantic value of the VP ((9c)). At the propositional level the assertion is the exclusive's assertion on the identity scale, Focus.Particles.atMost (· = ·), which is the entailment-scale exclusion where the prejacent entails no other member of the domain (Focus.Particles.atMost_eq_eq_atMost_subset).

def Rooth1992.intro {E : Type} (x y z : E) : Set (Set (E × E × E))

The fact that x introduced y to z.

Equations

• Rooth1992.intro x y z = Rooth1992.atom (x, y, z)

def Rooth1992.scenario {E : Type} (m b t s : E) : Set (E × E × E)

In the introduction scenario Mary introduced Bill and Tom to Sue, and there were no other introductions.

Equations

• Rooth1992.scenario m b t s = {(m, b, s), (m, t, s)}

theorem Rooth1992.vp_objectFocus {E : Type} (m b s : E) : ((fun (y : E) => intro m y s) <$> WithAlternatives.focused b).alternatives = Set.range fun (y : E) => intro m y s

The focus semantic value of introduced [Bill]F to Sue with Mary as subject (5a) is the set of propositions of the form 'Mary introduced y to Sue'.

theorem Rooth1992.three_a {E : Type} (m b t s : E) (hbt : b ≠ t) : scenario m b t s ∉ Focus.Particles.atMost (fun (x1 x2 : Set (Set (E × E × E))) => x1 = x2) (Set.range fun (y : E) => intro m y s) (intro m b s)

(3a) is false in the scenario, since 'Mary introduced Tom to Sue' is a true member of the domain distinct from the prejacent.

theorem Rooth1992.three_b {E : Type} (m b t s : E) (hbt : b ≠ t) : scenario m b t s ∈ Focus.Particles.atMost (fun (x1 x2 : Set (Set (E × E × E))) => x1 = x2) (Set.range fun (z : E) => intro m b z) (intro m b s)

(3b) is true in the scenario, since the only true proposition of the form 'Mary introduced Bill to z' is the prejacent.

inductive Rooth1992.Verb : Type

The relations a focused transitive verb ranges over.

• read : Verb
• understand : Verb

@[instance_reducible]

instance Rooth1992.instDecidableEqVerb : DecidableEq Verb

Equations

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

def Rooth1992.rel {E : Type} (v : Verb) (x y : E) : Set (Set (Verb × E × E))

The fact that x stands in relation v to y.

Equations

• Rooth1992.rel v x y = Rooth1992.atom (v, x, y)

theorem Rooth1992.univ_mem_vp_verbFocus {E : Type} (m c : E) : Set.univ ∈ ((fun (R : E → E → Set (Set (Verb × E × E))) => R m c) <$> WithAlternatives.focused (rel Verb.read)).alternatives

The focus semantic value of [read]F The Recognitions with Mary as subject (8) ranges over every relation, so it contains the trivial proposition.

theorem Rooth1992.recognitions_fixed {E : Type} (m c : E) : Focus.Particles.atMost (fun (x1 x2 : Set (Set (Verb × E × E))) => x1 = x2) ((fun (R : E → E → Set (Set (Verb × E × E))) => R m c) <$> WithAlternatives.focused (rel Verb.read)).alternatives (rel Verb.read m c) = ∅

(7) with the domain fixed to the full focus semantic value, as in [Roo85], is unsatisfiable.

theorem Rooth1992.recognitions_constrained {E : Type} (m c : E) : {(Verb.read, m, c)} ∈ Focus.Particles.atMost (fun (x1 x2 : Set (Set (Verb × E × E))) => x1 = x2) {rel Verb.read m c, rel Verb.understand m c} (rel Verb.read m c)

With the domain constrained to reading and understanding (37c), (7) is true where Mary read without understanding.

Contrasting phrases (§2.2)

(14): construe α as contrasting with β if the ordinary value of β is a member of the focus semantic value of α; the paper derives it from the individual case of the focus interpretation principle, where the ordinary value of any phrase can be the antecedent.

def Rooth1992.nbar {E W : Type} (farmer P : E → Set W) : E → Set W

The intersective N' P farmer.

Equations

• Rooth1992.nbar farmer P x = P x ∩ farmer x

theorem Rooth1992.farmer_contrast {E W : Type} (farmer american canadian : E → Set W) (h : nbar farmer canadian ≠ nbar farmer american) : Focus.SquiggleInd (nbar farmer american) (nbar farmer <$> WithAlternatives.focused american).alternatives (nbar farmer canadian)

'Canadian farmer' is a property of the form 'P farmer', so it can be the antecedent for the focus on [American]F farmer (15).

Scalar implicature (§2.3)

Asserting a member of a scale implicates the negation of the members that entail it. The constraint on scales (22) requires the underlying set to lie inside the focus semantic value of the assertion, so the two placements of focus in (16) and (17) license different scales.

@[reducible, inline]

abbrev Rooth1992.Grades (E : Type) : Type

In the quiz world everyone has a grade, failed, passed or aced.

Equations

• Rooth1992.Grades E = (E → Fin 3)

def Rooth1992.pass {E : Type} (g : Finset E) : Set (Grades E)

The group g passed.

Equations

• Rooth1992.pass g = {w : Rooth1992.Grades E | ∀ x ∈ g, 1 ≤ w x}

def Rooth1992.ace {E : Type} (x : E) : Set (Grades E)

x aced.

Equations

• Rooth1992.ace x = {w : Rooth1992.Grades E | 2 ≤ w x}

theorem Rooth1992.ace_ssubset_pass {E : Type} (m : E) : ace m ⊂ pass {m}

Acing entails passing and not conversely (18).

theorem Rooth1992.pass_union {E : Type} [DecidableEq E] (g g' : Finset E) : pass (g ∪ g') = pass g ∩ pass g'

A group passed iff its parts did.

theorem Rooth1992.verbFocus_scale {E : Type} (m : E) : {ace m, pass {m}} ⊆ ((fun (V : Finset E → Set (Grades E)) => V {m}) <$> WithAlternatives.focused pass).alternatives ∧ NeoGricean.IsSecondaryImplicature (pass {m}) {ace m} (ace m)

The scale of acing and passing lies inside the focus semantic value of I [passed]F, and asserting the weaker member implicates the negation of the stronger (16).

theorem Rooth1992.subjectFocus_scale {E : Type} (m : E) : Set.range pass ⊆ (pass <$> WithAlternatives.focused {m}).alternatives

The scale of group propositions of the form 'x passed' lies inside the focus semantic value of [I]F passed (21).

theorem Rooth1992.ace_notMem_subjectFocus {E : Type} (m : E) : ace m ∉ (pass <$> WithAlternatives.focused {m}).alternatives

The acing scale does not lie inside the focus semantic value of [I]F passed, since no group's passing is Mats's acing, which is why (17) suggests nothing about acing.

theorem Rooth1992.roommate_implicature {E : Type} (m : E) [DecidableEq E] (p : E) (w : Grades E) (hm : w ∈ pass {m}) (hmp : w ∉ pass {m, p}) : w ∉ pass {p}

In the roommate implicature, asserting that Mats passed implicates the negation of the group proposition that Mats and Paul passed, which with Mats passing is Paul not passing.

Questions and answers (§2.4)

The ordinary semantic value of a question is its set of potential answers ([Ham73]), which the question-answer constraint (26d) requires to lie inside the focus semantic value of the answer.

def Rooth1992.cut {E : Type} (x y : E) : Set (Set (E × E))

The fact that x cut y down to size.

Equations

• Rooth1992.cut x y = Rooth1992.atom (x, y)

def Rooth1992.whoCut {E : Type} (P : Set E) (b : E) : Set (Set (Set (E × E)))

The question Who cut Bill down to size? (25a) over the persons P.

Equations

• Rooth1992.whoCut P b = (fun (x : E) => Rooth1992.cut x b) '' P

theorem Rooth1992.subjectFocus_value {E : Type} (m b : E) : ((fun (x : E) => cut x b) <$> WithAlternatives.focused m).alternatives = Set.range fun (x : E) => cut x b

The focus semantic value of [Mary]F cut Bill down to size is the set of propositions of the form 'x cut Bill down to size', over every individual.

theorem Rooth1992.question_resolves_subjectFocus {E : Type} (P : Set E) (m b : E) {x : E} (hm : m ∈ P) (hx : x ∈ P) (hxm : x ≠ m) : (Focus.Antecedent.question (whoCut P b)).Resolves (cut m b) (Set.range fun (x : E) => cut x b)

(23Aa) answers (23Qa), since the question fully resolves the focus on the subject, with any other person supplying the contrasting alternative.

theorem Rooth1992.question_rejects_objectFocus {E : Type} (P : Set E) (m b : E) {x : E} (hx : x ∈ P) (hxm : x ≠ m) : ¬(Focus.Antecedent.question (whoCut P b)).Admits (Set.range fun (y : E) => cut m y)

(23Ab) does not answer (23Qa), since another person's cutting Bill down to size is not of the form 'Mary cut y down to size'.

Bare remnant ellipsis (§7–§8)

She beats [me]F more often than Sue has two logical forms, with the object or the subject as the correlate of the remnant; focus does not enter the grammar of ellipsis but filters the two, since the ~ operator at the main clause needs the than-clause as an antecedent of the right form (64)–(66).

def Rooth1992.beats {E : Type} (x y : E) : Set (Set (E × E))

The fact that x beats y.

Equations

• Rooth1992.beats x y = Rooth1992.atom (x, y)

inductive Rooth1992.Correlate : Type

Which phrase of the main clause the remnant Sue corresponds to.

• object : Correlate
• subject : Correlate

@[instance_reducible]

instance Rooth1992.instDecidableEqCorrelate : DecidableEq Correlate

Equations

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

def Rooth1992.instReprCorrelate.repr : Correlate → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Rooth1992.instReprCorrelate : Repr Correlate

Equations

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

def Rooth1992.thanClause {E : Type} (she me sue : E) : Correlate → Set (Set (E × E))

The than-clause under each correlate is 'she beats Sue' or 'Sue beats me'.

Equations

• Rooth1992.thanClause she me sue Rooth1992.Correlate.object = Rooth1992.beats she sue
• Rooth1992.thanClause she me sue Rooth1992.Correlate.subject = Rooth1992.beats sue me

inductive Rooth1992.FocusSite : Type

Where the focus falls in the main clause.

• onObject : FocusSite
• onSubject : FocusSite

@[instance_reducible]

instance Rooth1992.instDecidableEqFocusSite : DecidableEq FocusSite

Equations

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

@[instance_reducible]

instance Rooth1992.instReprFocusSite : Repr FocusSite

Equations

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

def Rooth1992.instReprFocusSite.repr : FocusSite → ℕ → Std.Format

Equations

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

def Rooth1992.FocusSite.marks : FocusSite → Focus.Mark × Focus.Mark

The marks a placement of focus puts on the subject and the object.

Equations

• Rooth1992.FocusSite.onObject.marks = (Focus.Mark.unfeatured, Focus.Mark.focused)
• Rooth1992.FocusSite.onSubject.marks = (Focus.Mark.focused, Focus.Mark.unfeatured)

def Rooth1992.mainClause {E : Type} (she me : E) (f : FocusSite) : Set (Set (Set (E × E)))

The focus semantic value of the main clause under a placement of focus.

Equations

• Rooth1992.mainClause she me f = (WithAlternatives.map₂ Rooth1992.beats ((WithAlternatives.unfeatured she).mark f.marks.1) ((WithAlternatives.unfeatured me).mark f.marks.2)).alternatives

theorem Rooth1992.ellipsis_filter {E : Type} (she me sue : E) (hsm : sue ≠ me) (hss : sue ≠ she) (r : Correlate) (f : FocusSite) : (Focus.Antecedent.phrase (thanClause she me sue r)).Resolves (beats she me) (mainClause she me f) ↔ (r = Correlate.object ↔ f = FocusSite.onObject)

The than-clause is an antecedent for the focus in the main clause exactly when the correlate is the focused phrase, so each reading survives under one placement of focus (66).

The rows

inductive Rooth1992.Person : Type

The individuals of the paper's scenarios.

• mary : Person
• bill : Person
• tom : Person
• sue : Person
• monique : Person
• bjorn : Person

@[instance_reducible]

instance Rooth1992.instDecidableEqPerson : DecidableEq Person

Equations

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

def Rooth1992.instReprPerson.repr : Person → ℕ → Std.Format

Equations

• Rooth1992.instReprPerson.repr Rooth1992.Person.mary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.Person.mary")).group prec✝
• Rooth1992.instReprPerson.repr Rooth1992.Person.bill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.Person.bill")).group prec✝
• Rooth1992.instReprPerson.repr Rooth1992.Person.tom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.Person.tom")).group prec✝
• Rooth1992.instReprPerson.repr Rooth1992.Person.sue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.Person.sue")).group prec✝
• Rooth1992.instReprPerson.repr Rooth1992.Person.monique prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.Person.monique")).group prec✝
• Rooth1992.instReprPerson.repr Rooth1992.Person.bjorn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.Person.bjorn")).group prec✝

@[instance_reducible]

instance Rooth1992.instReprPerson : Repr Person

Equations

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

inductive Rooth1992.OnlyFocus : Type

The focus positions of the only rows.

• bill : OnlyFocus
• sue : OnlyFocus

@[instance_reducible]

instance Rooth1992.instDecidableEqOnlyFocus : DecidableEq OnlyFocus

Equations

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

@[instance_reducible]

instance Rooth1992.instReprOnlyFocus : Repr OnlyFocus

Equations

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

def Rooth1992.instReprOnlyFocus.repr : OnlyFocus → ℕ → Std.Format

Equations

• Rooth1992.instReprOnlyFocus.repr Rooth1992.OnlyFocus.bill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.OnlyFocus.bill")).group prec✝
• Rooth1992.instReprOnlyFocus.repr Rooth1992.OnlyFocus.sue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.OnlyFocus.sue")).group prec✝

def Rooth1992.OnlyFocus.marks : OnlyFocus → Focus.Mark × Focus.Mark

The marks a focus position puts on the object and the goal of Mary introduced Bill to Sue.

Equations

• Rooth1992.OnlyFocus.bill.marks = (Focus.Mark.focused, Focus.Mark.unfeatured)
• Rooth1992.OnlyFocus.sue.marks = (Focus.Mark.unfeatured, Focus.Mark.focused)

def Rooth1992.OnlyFocus.domain (f : OnlyFocus) : Set (Set (Set (Person × Person × Person)))

The domain of only a focus position constrains, over the introduction scenario, is the focus semantic value of the VP.

Equations

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

def Rooth1992.onlyRow (r : Datum) : Option (OnlyFocus × Bool)

The focus position and the truth value an only row reports.

Equations

• Rooth1992.onlyRow r = do let f ← r.parse? "focus" [("Bill", Rooth1992.OnlyFocus.bill), ("Sue", Rooth1992.OnlyFocus.sue)] let v ← r.parse? "truth" [("true", true), ("false", false)] pure (f, v)

def Rooth1992.onlyData : List (OnlyFocus × Bool)

The only rows have (3a) false and (3b) true.

Equations

• Rooth1992.onlyData = List.filterMap Rooth1992.onlyRow Rooth1992.Examples.all

theorem Rooth1992.only_rows (d : OnlyFocus × Bool) : d ∈ onlyData → (d.2 = true ↔ scenario Person.mary Person.bill Person.tom Person.sue ∈ Focus.Particles.atMost (fun (x1 x2 : Set (Set (Person × Person × Person))) => x1 = x2) d.1.domain (intro Person.mary Person.bill Person.sue))

A row of (3a) and (3b) is true in the introduction scenario iff only over the domain its focus constrains holds there.

inductive Rooth1992.Q : Type

The questions of (23).

• whoCutBill : Q
• whoDidMaryCut : Q

@[instance_reducible]

instance Rooth1992.instDecidableEqQ : DecidableEq Q

Equations

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

@[instance_reducible]

instance Rooth1992.instReprQ : Repr Q

Equations

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

def Rooth1992.instReprQ.repr : Q → ℕ → Std.Format

Equations

• Rooth1992.instReprQ.repr Rooth1992.Q.whoCutBill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.Q.whoCutBill")).group prec✝
• Rooth1992.instReprQ.repr Rooth1992.Q.whoDidMaryCut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rooth1992.Q.whoDidMaryCut")).group prec✝

def Rooth1992.Q.den : Q → Set (Set (Set (Person × Person)))

The denotation of a question, over all persons.

Equations

• Rooth1992.Q.whoCutBill.den = Rooth1992.whoCut Set.univ Rooth1992.Person.bill
• Rooth1992.Q.whoDidMaryCut.den = (fun (y : Rooth1992.Person) => Rooth1992.cut Rooth1992.Person.mary y) '' Set.univ

inductive Rooth1992.AnswerFocus : Type

The focus positions of the answers of (23).

• mary : AnswerFocus
• bill : AnswerFocus

@[instance_reducible]

instance Rooth1992.instDecidableEqAnswerFocus : DecidableEq AnswerFocus

Equations

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

def Rooth1992.instReprAnswerFocus.repr : AnswerFocus → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Rooth1992.instReprAnswerFocus : Repr AnswerFocus

Equations

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

def Rooth1992.AnswerFocus.marks : AnswerFocus → Focus.Mark × Focus.Mark

The marks a focus position puts on the subject and the object of Mary cut Bill down to size.

Equations

• Rooth1992.AnswerFocus.mary.marks = (Focus.Mark.focused, Focus.Mark.unfeatured)
• Rooth1992.AnswerFocus.bill.marks = (Focus.Mark.unfeatured, Focus.Mark.focused)

def Rooth1992.AnswerFocus.value (f : AnswerFocus) : Set (Set (Set (Person × Person)))

The focus semantic value of an answer.

Equations

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

def Rooth1992.qaRow (r : Datum) : Option (Q × AnswerFocus × Bool)

The question, the answer's focus position, and the judgment of a question-answer row.

Equations

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

def Rooth1992.qaData : List (Q × AnswerFocus × Bool)

The question-answer rows of (23).

Equations

• Rooth1992.qaData = List.filterMap Rooth1992.qaRow Rooth1992.Examples.all

theorem Rooth1992.qa_rows (d : Q × AnswerFocus × Bool) : d ∈ qaData → (d.2.2 = true ↔ (Focus.Antecedent.question d.1.den).Admits d.2.1.value)

An answer is appropriate iff the question denotation lies inside its focus semantic value (23).