Kratzer and Selkirk (2020): Deconstructing Information Structure

Kratzer and Selkirk decompose information structure into two privative features, with their semantics in Rooth's alternative semantics. [FoC] makes the alternatives of a constituent the whole domain of its type and imposes no discourse requirement of its own. The squiggle that must c-command it requires its scope to represent a contrast with each of a set of discourse referents (49), and then collapses the alternatives to the ordinary value. [G] requires its node to be Given with respect to a referent of the preceding discourse and leaves both values unchanged; the requirement is use-conditional, like the German particles ja and doch. Newness is no feature at all, so the paper's footnote on Hausa rereads the in situ and ex situ answers of Hartmann and Zimmermann as unmarked newness and [FoC].

Two consequences follow. No constituent bears both features, since no domain is a singleton, and a constituent containing a FoCus can be Given only if an operator inside it consumes the alternatives (58). Through a context with no squiggle, the meaning of a constituent is the meaning of the FoCus bound into the context, so the constituent is Given only if its ordinary value ignores the FoCus. The paper's derivation of (58) assumes that it never does, but [Mary]FoC came or didn't come is Given with an unconsumed FoCus. In second-occurrence focus (60) the squiggle under only consumes the alternatives, and without it the [G] on the VP is not licensed.

Main definitions

• LF, LF.meaning: logical forms with labelled nodes, and their meanings.
• LF.IsVariant, LF.RepresentsContrast: [FoC]/[G]-variants, and contrast representation (49).
• Window, LF.Felicitous: discourse windows, and the use-conditional content of [G] and the squiggle.
• LF.Ctx, LF.Ctx.Transparent: one-hole contexts, and those with no squiggle.

Main results

• not_given_mark_focused: no constituent bears both features.
• LF.Ctx.meaning_plug: a context with no squiggle is a continuation.
• LF.ord_plug_eq_of_given, LF.not_given_plug_foc: (58) at any depth.
• LF.given_foc_came_or_not: (58) needs the dependence on the FoCus.
• LF.representsContrast_narrow, LF.not_representsContrast_overfocused: among all their variants, (51) represents a contrast with (50a) and (50b) does not.
• LF.felicitous_sofVP, LF.not_felicitous_without_squiggle: second-occurrence focus (60).
• sUnion_alternatives_every_focused: Schwarzschild's givenness is trivially satisfied (fn. 14).

Implementation notes

[FoC] is the substrate's F-mark Focus.Mark.focused and (45) is WithAlternatives.mark, the domain of a type being all its values. The paper's Givenness is the substrate's WithAlternatives.Given, and its only (56), every true member of the salient set being the prejacent, is Focus.Particles.atMost (· = ·) at the set the squiggle also carries (55b), so the paper's indirect association through two occurrences of the contextual variable is a fact about the substrate and is not restated. The features are part of a node's label (p. 38), so every node of a logical form carries a label, and the variants of a form are its relabellings. [G] (47) takes its referent from the window preceding the context, with no anticipatory licensing (fn. 46), and the squiggle (53) from the window surrounding it, since a contrast may be represented with a later referent (fn. 58). Logical forms compose by function application only. The prosodic spell-out of the features in English (§6–§7) is prose.

TODO

• Pressure for [FoC]-Marking (66), with the data of (62)–(65), over the variants of a form.
• The squiggle of (60) over the whole sentence, contrasting with the preceding sentence.
• Logical forms with abstraction, where Hamblin alternatives do not distribute.

References

• [KS20]
• [Roo92] — alternatives semantics and the squiggle operator
• [Sch99b] — A-Givenness, of which the paper's Givenness is a special case
• [Pot05] — expressive meaning
• [HZ07c] — the Hausa data of footnote 21

The features (45)–(47)

theorem KratzerSelkirk2020.not_given_mark_focused {α : Type u_1} [Nontrivial α] (d : WithAlternatives α) (a : α) : ¬(d.mark Focus.Mark.focused).Given a

No constituent bears both features, since an F-marked constituent of a type with two values is Given with respect to nothing.

theorem KratzerSelkirk2020.useConditional_projects {W : Type u_1} (F : (W → Prop) → W → Prop) (atIssue requirement : W → Prop) : (F <$> { atIssue := atIssue, notAtIssue := requirement }).notAtIssue = requirement

The Givenness requirement is use-conditional and must be met by the utterance context however deeply [G] is embedded. As the not-at-issue content of a two-dimensional meaning, it survives every at-issue operator F.

def KratzerSelkirk2020.RepresentsContrast {ι : Type u_1} {γ : Type u_2} (v : ι → WithAlternatives γ) (i : ι) (a : γ) : Prop

(49) An expression v i represents a contrast with a when a is among its alternatives and differs from its ordinary value, and no variant v j with strictly fewer alternatives has a among them. The last condition prevents overfocusing.

Equations

• KratzerSelkirk2020.RepresentsContrast v i a = (Focus.SquiggleInd (v i).ordinary (v i).alternatives a ∧ ∀ (j : ι), (v j).alternatives ⊂ (v i).alternatives → a ∉ (v j).alternatives)

Logical forms

A logical form composes lexical meanings by function application, and a squiggle takes scope over a constituent. Every node is labelled with its features, [FoC] and [G] with its referent, which are "technically part of [its] labeling" (p. 38), so the [FoC]/[G]-variants of a form are its relabellings (49).

structure KratzerSelkirk2020.Label (α : Type) : Type

A node's label records whether it bears [FoC] and the referent of its [G], if it bears [G].

• mark : Focus.Mark

  Whether the node bears [FoC].

• given : Option α

  The referent the node's [G] is indexed with, if it bears [G].

def KratzerSelkirk2020.Label.bare {α : Type} : Label α

The label of a node with neither feature.

Equations

• KratzerSelkirk2020.Label.bare = { mark := Focus.Mark.unfeatured, given := none }

def KratzerSelkirk2020.Label.foc {α : Type} : Label α

The label of a [FoC]-marked node.

Equations

• KratzerSelkirk2020.Label.foc = { mark := Focus.Mark.focused, given := none }

inductive KratzerSelkirk2020.LF : Type → Type 1

A logical form of the paper is a lexical item, a function application or a squiggle with its antecedents, each node with its label, over meanings of each type.

• lex {α : Type} (x : α) (l : Label α) : LF α
• app {α β : Type} (f : LF (α → β)) (x : LF α) (l : Label β) : LF β
• squiggle {α : Type} (ℭ : Set α) (t : LF α) (l : Label α) : LF α

def KratzerSelkirk2020.LF.label {α : Type} : LF α → Label α

The label of the root.

Equations

• (KratzerSelkirk2020.LF.lex x_3 l).label = l
• (f.app x_3 l).label = l
• (KratzerSelkirk2020.LF.squiggle ℭ t l).label = l

def KratzerSelkirk2020.LF.ord {α : Type} : LF α → α

The ordinary value of a logical form overlooks its labels and squiggles (45), (47), (54).

Equations

• (KratzerSelkirk2020.LF.lex x_3 l).ord = x_3
• (f.app x_3 l).ord = f.ord x_3.ord
• (KratzerSelkirk2020.LF.squiggle ℭ t l).ord = t.ord

def KratzerSelkirk2020.LF.meaning {α : Type} : LF α → WithAlternatives α

The meaning of a logical form. A node applies its function daughter to its argument, a squiggle collapses the alternatives of its scope to the ordinary value (54), [FoC] on a node makes its alternatives the whole type (45), and [G] leaves both values unchanged (47).

Equations

• (KratzerSelkirk2020.LF.lex x_3 l).meaning = (WithAlternatives.unfeatured x_3).mark l.mark
• (f.app x_3 l).meaning = (f.meaning <*> x_3.meaning).mark l.mark
• (KratzerSelkirk2020.LF.squiggle ℭ t l).meaning = (WithAlternatives.unfeatured t.ord).mark l.mark

def KratzerSelkirk2020.LF.raw {α : Type} : LF α → WithAlternatives α

The meaning of the root before its own [FoC].

Equations

• (KratzerSelkirk2020.LF.lex x_3 l).raw = WithAlternatives.unfeatured x_3
• (f.app x_3 l).raw = f.meaning <*> x_3.meaning
• (KratzerSelkirk2020.LF.squiggle ℭ t l).raw = WithAlternatives.unfeatured t.ord

theorem KratzerSelkirk2020.LF.meaning_eq_mark {α : Type} (t : LF α) : t.meaning = t.raw.mark t.label.mark

@[simp]

theorem KratzerSelkirk2020.LF.meaning_lex_bare {α : Type} (x : α) : (lex x Label.bare).meaning = pure x

@[simp]

theorem KratzerSelkirk2020.LF.ordinary_meaning {α : Type} (t : LF α) : t.meaning.ordinary = t.ord

theorem KratzerSelkirk2020.LF.wellFormed_meaning {α : Type} (t : LF α) : t.meaning.WellFormed

Every logical form has its ordinary value among its alternatives.

theorem KratzerSelkirk2020.LF.wellFormed_raw {α : Type} (t : LF α) : t.raw.WellFormed

theorem KratzerSelkirk2020.LF.meaning_eq_bind {α : Type} (t : LF α) : t.meaning = do let c ← t.raw (pure c).mark t.label.mark

A node's own mark is a continuation of the meaning of its root.

Variants, contrast and felicity

inductive KratzerSelkirk2020.LF.IsVariant {α : Type} : LF α → LF α → Prop

Two logical forms are [FoC]/[G]-variants when they are identical except for their labels (49).

• lex {α : Type} (x : α) (l l' : Label α) : (LF.lex x l).IsVariant (LF.lex x l')
• app {α β : Type} {f f' : LF (α → β)} {x x' : LF α} (l l' : Label β) : f.IsVariant f' → x.IsVariant x' → (f.app x l).IsVariant (f'.app x' l')
• squiggle {α : Type} (ℭ : Set α) {t t' : LF α} (l l' : Label α) : t.IsVariant t' → (LF.squiggle ℭ t l).IsVariant (LF.squiggle ℭ t' l')

theorem KratzerSelkirk2020.LF.IsVariant.refl {α : Type} (t : LF α) : t.IsVariant t

theorem KratzerSelkirk2020.LF.IsVariant.ord_eq {α : Type} {s t : LF α} (h : s.IsVariant t) : s.ord = t.ord

Variants share their ordinary value, which overlooks labels.

def KratzerSelkirk2020.LF.RepresentsContrast {α : Type} (t : LF α) (a : α) : Prop

(49) over the variants of a logical form. It represents a contrast with a when a is among its alternatives and differs from its ordinary value, and no variant with strictly fewer alternatives has a among them.

Equations

• t.RepresentsContrast a = KratzerSelkirk2020.RepresentsContrast (fun (s : { s : KratzerSelkirk2020.LF α // s.IsVariant t }) => (↑s).meaning) ⟨t, ⋯⟩ a

theorem KratzerSelkirk2020.LF.representsContrast_iff {α : Type} {t : LF α} {a : α} : t.RepresentsContrast a ↔ a ∈ t.meaning.alternatives ∧ a ≠ t.ord ∧ ∀ (s : LF α), s.IsVariant t → s.meaning.alternatives ⊂ t.meaning.alternatives → a ∉ s.meaning.alternatives

structure KratzerSelkirk2020.Window : Type 1

A context of utterance supplies discourse referents of each type, in the window preceding it and in the window surrounding it.

• preceding (α : Type) : Set α

  The referents of the window preceding the context.

• surrounding (α : Type) : Set α

  The referents of the window surrounding the context.

def KratzerSelkirk2020.Label.Licensed {α : Type} (w : Window) (l : Label α) (m : WithAlternatives α) : Prop

The label of a node of meaning m is licensed when its [G], if any, has its referent in the preceding window and the node is Given with respect to it (47); there is no anticipatory [G] (fn. 46).

Equations

• KratzerSelkirk2020.Label.Licensed w l m = ∀ a ∈ l.given, a ∈ w.preceding α ∧ m.Given a

@[simp]

theorem KratzerSelkirk2020.Label.licensed_bare {α : Type} (w : Window) (m : WithAlternatives α) : Licensed w bare m

@[simp]

theorem KratzerSelkirk2020.Label.licensed_foc {α : Type} (w : Window) (m : WithAlternatives α) : Licensed w foc m

def KratzerSelkirk2020.LF.Felicitous (w : Window) {α : Type} : LF α → Prop

A logical form is felicitous in a context when every label is licensed and every squiggle represents a contrast with each of its antecedents, which the surrounding window supplies (54); a contrast may be represented with a later referent (fn. 58).

Equations

• One or more equations did not get rendered due to their size.
• KratzerSelkirk2020.LF.Felicitous w (KratzerSelkirk2020.LF.lex x_3 l) = KratzerSelkirk2020.Label.Licensed w l (KratzerSelkirk2020.LF.lex x_3 l).meaning
• KratzerSelkirk2020.LF.Felicitous w (f.app x_3 l) = (KratzerSelkirk2020.LF.Felicitous w f ∧ KratzerSelkirk2020.LF.Felicitous w x_3 ∧ KratzerSelkirk2020.Label.Licensed w l (f.app x_3 l).meaning)

(58)

inductive KratzerSelkirk2020.LF.Ctx : Type → Type → Type 1

A one-hole context of a logical form, from a hole of type α up to a root of type γ, each node above the hole with its label.

• hole {α : Type} : Ctx α α
• fn {α β γ : Type} (x : LF α) (l : Label β) (K : Ctx β γ) : Ctx (α → β) γ
• arg {α β γ : Type} (f : LF (α → β)) (l : Label β) (K : Ctx β γ) : Ctx α γ
• squiggle {α γ : Type} (ℭ : Set α) (l : Label α) (K : Ctx α γ) : Ctx α γ

def KratzerSelkirk2020.LF.Ctx.plug {α γ : Type} : Ctx α γ → LF α → LF γ

The form with t in the hole.

Equations

• KratzerSelkirk2020.LF.Ctx.hole.plug x✝ = x✝
• (KratzerSelkirk2020.LF.Ctx.fn x_5 l K).plug t = K.plug (t.app x_5 l)
• (KratzerSelkirk2020.LF.Ctx.arg f l K).plug x✝ = K.plug (f.app x✝ l)
• (KratzerSelkirk2020.LF.Ctx.squiggle ℭ l K).plug x✝ = K.plug (KratzerSelkirk2020.LF.squiggle ℭ x✝ l)

def KratzerSelkirk2020.LF.Ctx.Transparent {α γ : Type} : Ctx α γ → Prop

A context is transparent when no squiggle lies between its hole and its root, so nothing in it consumes the alternatives of the hole.

Equations

• KratzerSelkirk2020.LF.Ctx.hole.Transparent = True
• (KratzerSelkirk2020.LF.Ctx.fn x_4 l K).Transparent = K.Transparent
• (KratzerSelkirk2020.LF.Ctx.arg f l K).Transparent = K.Transparent
• (KratzerSelkirk2020.LF.Ctx.squiggle ℭ l K).Transparent = False

theorem KratzerSelkirk2020.LF.Ctx.meaning_plug {α γ : Type} {K : Ctx α γ} (hK : K.Transparent) (t : LF α) : (K.plug t).meaning = do let a ← t.meaning (K.plug (lex a Label.bare)).meaning

Through a transparent context the meaning of a constituent is the meaning of its hole bound into the context, which is a continuation.

theorem KratzerSelkirk2020.LF.ord_plug_eq_of_given {α γ : Type} {K : Ctx α γ} (hK : K.Transparent) {t : LF α} (ht : t.label.mark = Focus.Mark.focused) {c : γ} (h : (K.plug t).meaning.Given c) (v : α) : (K.plug (lex v Label.bare)).ord = c

(58) at any depth. A constituent containing a [FoC]-marked constituent with no squiggle between them is Given only if its ordinary value ignores the FoCus.

theorem KratzerSelkirk2020.LF.not_given_plug_foc {α γ : Type} {K : Ctx α γ} (hK : K.Transparent) {v w : α} (hvw : (K.plug (lex v Label.bare)).ord ≠ (K.plug (lex w Label.bare)).ord) {t : LF α} (ht : t.label.mark = Focus.Mark.focused) (c : γ) : ¬(K.plug t).meaning.Given c

(58) in the paper's form. A constituent whose ordinary value depends on a [FoC]-marked constituent with no squiggle between them is not Given, so it cannot be [G]-marked.

theorem KratzerSelkirk2020.LF.given_foc_came_or_not {E W : Type} (came : E → Set W) (mary : E) : ((lex (fun (x : E) => came x ∪ (came x)ᶜ) Label.bare).app (lex mary Label.foc) Label.bare).meaning.Given Set.univ

The dependence is needed, as the paper's derivation of (58) overlooks. [Mary]FoC came or didn't come contains a FoCus that nothing consumes, yet it is Given with respect to the tautology, since its predicate holds of everyone.

Overfocusing (49)–(51)

Over the variants of a predication, every relabelling of its nodes, a narrow FoCus on one argument represents a contrast with an antecedent differing there, and the FoCus on both arguments of (50b) does not, since the narrow variant (51) has fewer alternatives that still include the antecedent.

def KratzerSelkirk2020.LF.pred₁ {σ τ : Type} (g : σ → τ) (z : σ) (l₁ : Label (σ → τ)) (l₂ : Label σ) (l₃ : Label τ) : LF τ

The application g z, its function, argument and root labelled l₁, l₂, l₃.

Equations

• KratzerSelkirk2020.LF.pred₁ g z l₁ l₂ l₃ = (KratzerSelkirk2020.LF.lex g l₁).app (KratzerSelkirk2020.LF.lex z l₂) l₃

theorem KratzerSelkirk2020.LF.isVariant_pred₁ {σ τ : Type} (g : σ → τ) (z : σ) (l₁ l₁' : Label (σ → τ)) (l₂ l₂' : Label σ) (l₃ l₃' : Label τ) : (pred₁ g z l₁ l₂ l₃).IsVariant (pred₁ g z l₁' l₂' l₃')

theorem KratzerSelkirk2020.LF.eq_pred₁_of_isVariant {σ τ : Type} {g : σ → τ} {z : σ} {l₁ : Label (σ → τ)} {l₂ : Label σ} {l₃ : Label τ} {s : LF τ} (h : s.IsVariant (pred₁ g z l₁ l₂ l₃)) : ∃ (l₁' : Label (σ → τ)) (l₂' : Label σ) (l₃' : Label τ), s = pred₁ g z l₁' l₂' l₃'

theorem KratzerSelkirk2020.LF.alternatives_pred₁_eq_univ {σ τ : Type} {g : σ → τ} {z : σ} {l₁ : Label (σ → τ)} {l₂ : Label σ} {l₃ : Label τ} (h : l₁.mark = Focus.Mark.focused ∨ l₃.mark = Focus.Mark.focused) : (pred₁ g z l₁ l₂ l₃).meaning.alternatives = Set.univ

A [FoC]-marked function or root makes the application evoke every value.

theorem KratzerSelkirk2020.LF.alternatives_pred₁ {σ τ : Type} {g : σ → τ} {z : σ} {l₁ : Label (σ → τ)} (l₂ : Label σ) {l₃ : Label τ} (h₁ : l₁.mark = Focus.Mark.unfeatured) (h₃ : l₃.mark = Focus.Mark.unfeatured) : (pred₁ g z l₁ l₂ l₃).meaning.alternatives = g '' (lex z l₂).meaning.alternatives

Otherwise the application evokes g at the alternatives of its argument.

theorem KratzerSelkirk2020.LF.representsContrast_pred₁ {σ τ : Type} {g : σ → τ} (hg : Function.Injective g) (z : σ) {z' : σ} (hz : z' ≠ z) : (pred₁ g z Label.bare Label.foc Label.bare).RepresentsContrast (g z')

A narrow FoCus on the argument of an injective function represents a contrast, among all the variants of the application, with the function at another argument.

def KratzerSelkirk2020.LF.pred₂ {α β γ : Type} (f : α → β → γ) (x : α) (y : β) (l₁ : Label (α → β → γ)) (l₂ : Label α) (l₃ : Label (β → γ)) (l₄ : Label β) (l₅ : Label γ) : LF γ

The predication f x y, its nodes labelled from the function down to the root.

Equations

• KratzerSelkirk2020.LF.pred₂ f x y l₁ l₂ l₃ l₄ l₅ = (KratzerSelkirk2020.LF.pred₁ f x l₁ l₂ l₃).app (KratzerSelkirk2020.LF.lex y l₄) l₅

theorem KratzerSelkirk2020.LF.isVariant_pred₂ {α β γ : Type} (f : α → β → γ) (x : α) (y : β) {l₁ l₁' : Label (α → β → γ)} {l₂ l₂' : Label α} {l₃ l₃' : Label (β → γ)} {l₄ l₄' : Label β} {l₅ l₅' : Label γ} : (pred₂ f x y l₁ l₂ l₃ l₄ l₅).IsVariant (pred₂ f x y l₁' l₂' l₃' l₄' l₅')

theorem KratzerSelkirk2020.LF.eq_pred₂_of_isVariant {α β γ : Type} {f : α → β → γ} {x : α} {y : β} {l₁ : Label (α → β → γ)} {l₂ : Label α} {l₃ : Label (β → γ)} {l₄ : Label β} {l₅ : Label γ} {s : LF γ} (h : s.IsVariant (pred₂ f x y l₁ l₂ l₃ l₄ l₅)) : ∃ (l₁' : Label (α → β → γ)) (l₂' : Label α) (l₃' : Label (β → γ)) (l₄' : Label β) (l₅' : Label γ), s = pred₂ f x y l₁' l₂' l₃' l₄' l₅'

theorem KratzerSelkirk2020.LF.alternatives_pred₂_eq_univ {α β γ : Type} {f : α → β → γ} {x : α} {y : β} {l₁ : Label (α → β → γ)} {l₂ : Label α} {l₃ : Label (β → γ)} {l₄ : Label β} {l₅ : Label γ} (h : l₁.mark = Focus.Mark.focused ∨ l₃.mark = Focus.Mark.focused ∨ l₅.mark = Focus.Mark.focused) : (pred₂ f x y l₁ l₂ l₃ l₄ l₅).meaning.alternatives = Set.univ

theorem KratzerSelkirk2020.LF.alternatives_pred₂ {α β γ : Type} {f : α → β → γ} {x : α} {y : β} {l₁ : Label (α → β → γ)} (l₂ : Label α) {l₃ : Label (β → γ)} (l₄ : Label β) {l₅ : Label γ} (h₁ : l₁.mark = Focus.Mark.unfeatured) (h₃ : l₃.mark = Focus.Mark.unfeatured) (h₅ : l₅.mark = Focus.Mark.unfeatured) : (pred₂ f x y l₁ l₂ l₃ l₄ l₅).meaning.alternatives = Set.image2 f (lex x l₂).meaning.alternatives (lex y l₄).meaning.alternatives

theorem KratzerSelkirk2020.LF.representsContrast_narrow {α β γ : Type} {f : α → β → γ} (hf : Function.Injective2 f) (x : α) {y y' : β} (hy : y' ≠ y) : (pred₂ f x y Label.bare Label.bare Label.bare Label.foc Label.bare).RepresentsContrast (f x y')

(51) John picked strawberries at [Sandy's]FoC farm represents a contrast with (50a) John picked strawberries at Mary's farm: no variant with fewer alternatives evokes it.

theorem KratzerSelkirk2020.LF.not_representsContrast_overfocused {α β γ : Type} {f : α → β → γ} [Nontrivial α] (hf : Function.Injective2 f) (x : α) (y y' : β) : ¬(pred₂ f x y Label.bare Label.foc Label.bare Label.foc Label.bare).RepresentsContrast (f x y')

(50b) John picked [strawberries]FoC at [Sandy's]FoC farm does not represent a contrast with (50a), since its variant (51) has strictly fewer alternatives and (50a) among them (49iii).

theorem KratzerSelkirk2020.LF.felicitous_squiggle_narrow {α β γ : Type} {f : α → β → γ} (hf : Function.Injective2 f) (x : α) {y y' : β} (hy : y' ≠ y) (w : Window) (hw : f x y' ∈ w.surrounding γ) : Felicitous w (squiggle {f x y'} (pred₂ f x y Label.bare Label.bare Label.bare Label.foc Label.bare) Label.bare)

(51) under a squiggle whose antecedent (50a) the surrounding window supplies is felicitous.

Second-occurrence focus (60)

def KratzerSelkirk2020.LF.sofVP {E W : Type} (only : (E → Set W) → E → Set W) (quote : E → E → Set W) (faculty : E) (𝔞 p : E → Set W) : LF (E → Set W)

The VP of (60), only ~𝔞 [quote [the faculty]FoC], [G]-marked with referent p.

Equations

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

theorem KratzerSelkirk2020.LF.felicitous_sofVP {E W : Type} (only : (E → Set W) → E → Set W) (quote : E → E → Set W) (faculty : E) (hq : Function.Injective quote) {other : E} (ho : other ≠ faculty) (w : Window) (hp : only (quote faculty) ∈ w.preceding (E → Set W)) (ha : quote other ∈ w.surrounding (E → Set W)) : Felicitous w (sofVP only quote faculty (quote other) (only (quote faculty)))

(60) The [G]-marked VP containing the second occurrence of the faculty is felicitous. Its squiggle represents a contrast with an accommodated antecedent, quoting someone other than the faculty (fn. 53), and consumes the FoCus, so the VP is Given with respect to the VP of the preceding sentence.

theorem KratzerSelkirk2020.LF.not_felicitous_without_squiggle {E W : Type} (only : (E → Set W) → E → Set W) (quote : E → E → Set W) (faculty : E) {v v' : E} (hvv : only (quote v) ≠ only (quote v')) (w : Window) (p : E → Set W) : ¬Felicitous w ((lex only Label.bare).app (pred₁ quote faculty Label.bare Label.foc Label.bare) { mark := Focus.Mark.unfeatured, given := some p })

Without the squiggle the [G] on the VP is not licensed when whom one quotes matters to the VP, since the FoCus on the faculty then reaches it (58).

A-Givenness (§3)

def KratzerSelkirk2020.isAGiven {α : Type u_1} (m : WithAlternatives α) (referent : α) : Prop

[Sch99b]'s A-Givenness in alternatives semantics: a salient discourse referent is among the alternatives.

Equations

• KratzerSelkirk2020.isAGiven m referent = (referent ∈ m.alternatives)

theorem KratzerSelkirk2020.isAGiven_of_given {α : Type u_1} {m : WithAlternatives α} {referent : α} (h : m.Given referent) : isAGiven m referent

Givenness is a special case of A-Givenness.

theorem KratzerSelkirk2020.not_given_of_isAGiven : ∃ (m : WithAlternatives ℕ) (referent : ℕ), isAGiven m referent ∧ ¬m.Given referent

The converse fails: a two-membered alternatives value is A-Given with respect to either member but Given with respect to neither.

def KratzerSelkirk2020.every {E : Type u_1} {W : Type u_2} (P Q : E → Set W) : Set W

Every P is a Q, with the restrictor and the scope as properties.

Equations

• KratzerSelkirk2020.every P Q = {w : W | ∀ (x : E), w ∈ P x → w ∈ Q x}

theorem KratzerSelkirk2020.sUnion_alternatives_every_focused {E W : Type} (cat complainer : E → Set W) : ⋃₀ ((fun (x : E → Set W) => every x complainer) <$> (pure cat).mark Focus.Mark.focused).alternatives = Set.univ

Footnote 14 finds Schwarzschild's givenness, entailment of the existential F-closure, too easy to satisfy, which A-Givenness is not. The F-closure of Every [cat]F is a complainer, that every P is a complainer for some P, holds at every world, since every complainer is a complainer.

Hausa (footnote 21)

The paper does not conclude with [HZ07c] that information focus is realised both in situ and ex situ in Hausa, since accommodated contrasts were not controlled for, and it notes the corpus tendency, most information focus in situ and most selective, contrastive, and corrective focus ex situ. On its inventory mere newness is no focus, so the rereading the footnote suggests, without stating it, is that ex situ realises [FoC] and in situ is unmarked.

def KratzerSelkirk2020.useMark : Focus.Use → Focus.Mark

The paper's inventory over the pragmatic uses of [HZ07c] marks the contrastive family with [FoC] and leaves new information unfeatured.

Equations

• KratzerSelkirk2020.useMark Focus.Use.newInfo = Focus.Mark.unfeatured
• KratzerSelkirk2020.useMark x✝ = Focus.Mark.focused

def KratzerSelkirk2020.KSHausaReading (u : HartmannZimmermann2007.FocusUtterance) : Prop

On the rereading of Hausa a focus is realised ex situ iff it bears [FoC].

Equations

• KratzerSelkirk2020.KSHausaReading u = (u.cfg.strategy = Focus.Strategy.exSitu ↔ KratzerSelkirk2020.useMark u.pragType = Focus.Mark.focused)

@[instance_reducible]

instance KratzerSelkirk2020.instDecidableKSHausaReading (u : HartmannZimmermann2007.FocusUtterance) : Decidable (KSHausaReading u)

Equations

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

theorem KratzerSelkirk2020.hz_cells_violate_reading : ¬KSHausaReading HartmannZimmermann2007.exSitu_newInfo ∧ ¬KSHausaReading HartmannZimmermann2007.inSitu_corrective

The two accounts part on the cells the accommodation caveat targets: the ex situ new-information answer and the in situ corrective answer of the Hausa study both violate the rereading.