Two-feature decomposition of information structure

Kratzer & Selkirk's privative-feature analysis: information structure decomposes into [FoC] (introduces alternatives) and [G] (presupposes discourse salience), with no separate feature for newness.

Main definitions

• ISFeature: FoC and G constructors.
• applyFoC, applyG: feature contributions to an AltMeaning.
• isGiven, isAGiven: K&S givenness and Schwarzschild A-givenness on alternative sets.
• Contrast, ContrastOperator: contrast representation and the K&S ~ operator that collapses alternatives.
• onlySemantics: the K&S analysis of only.
• FoCSpellout, GSpellout, englishSpelloutRanking: prosodic spellout machinery.
• SOFDatum, ProsodicTripleDatum: second-occurrence-focus data.
• PressureForG, PressureForFoC: pragmatic pressures.

Main results

• foc_g_exclusion: [FoC] and [G] cannot both hold of a single meaning under a non-trivial domain.
• givenness_entails_aGivenness: K&S givenness implies Schwarzschild A-givenness; the converse is refuted.

References

• [KS20], [Sch99], [BCF+07], [KS11], [HZ07].

inductive KratzerSelkirk2020.ISFeature : Type

The two privative morphosyntactic features of [KS20].

[FoC] and [G] are genuinely syntactic features: crosslinguistically they trigger displacement, agreement, and ellipsis (§2). They happen to be spelled out prosodically in Standard American and British English, but this is not their defining property.

• FoC : ISFeature

  FoCus: introduces alternatives, signals contrast. Resembles [wh] — comes with obligatory ~ operator.

• G : ISFeature

  Givenness: presupposes discourse salience, signals match. Contributes meaning directly (no operator needed).

@[implicit_reducible]

instance KratzerSelkirk2020.instDecidableEqISFeature : DecidableEq ISFeature

Equations

• KratzerSelkirk2020.instDecidableEqISFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KratzerSelkirk2020.instReprISFeature : Repr ISFeature

Equations

• KratzerSelkirk2020.instReprISFeature = { reprPrec := KratzerSelkirk2020.instReprISFeature.repr }

def KratzerSelkirk2020.instReprISFeature.repr : ISFeature → ℕ → Std.Format

Equations

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

def KratzerSelkirk2020.isNew (hasFoC hasG : Bool) : Bool

Newness is NOT a grammatical feature. New material is simply unmarked — no [FoC], no [G].

Equations

• KratzerSelkirk2020.isNew hasFoC hasG = (!hasFoC && !hasG)

Contribution of [FoC]

[FoC] does NOT change the O-value. Its A-value is the full domain D_τ (all possible entities of the relevant semantic type). This is standard Roothian focus semantics.

⟦[α]{FoC}⟧{O,C} = ⟦α⟧{O,C} ⟦[α]{FoC}⟧_{A,C} = D_τ

def KratzerSelkirk2020.applyFoC {α : Type u_1} (m : Alternatives.AltMeaning α) (domain : List α) : Alternatives.AltMeaning α

Apply [FoC] to a meaning: O-value unchanged, A-value becomes full domain. K&S (45): The A-value of [α]_{FoC} is D_τ.

Equations

• KratzerSelkirk2020.applyFoC m domain = { oValue := m.oValue, aValue := domain }

theorem KratzerSelkirk2020.foc_preserves_oValue {α : Type u_1} (m : Alternatives.AltMeaning α) (domain : List α) : (applyFoC m domain).oValue = m.oValue

[FoC] preserves O-value. K&S (45) first clause.

Contribution of [G]

[G] introduces a Givenness requirement: the expression must match a salient discourse referent. Technically:

⟦[α]{G_a}⟧{O,C} is defined iff a is a discourse referent in C, and α is Given with respect to a. If defined, ⟦[α]{G_a}⟧{O,C} = ⟦α⟧{O,C} ⟦[α]{G_a}⟧{A,C} = ⟦α⟧{A,C}

[G] contributes purely use-conditional / expressive meaning (like discourse particles German "ja", "doch"). It places a condition on the discourse context, not on truth conditions.

def KratzerSelkirk2020.isGiven {α : Type u_1} [DecidableEq α] (aValue : List α) (referent : α) : Prop

An expression α is Given with respect to discourse referent a iff its A-value is {a} (a singleton containing just the referent).

K&S (46): α is Given w.r.t. a in C iff ⟦α⟧_{A,C} = {a}.

Intuitively: the alternatives set has collapsed to a single salient entity, meaning there's nothing to contrast — the content is already "in the air".

Equations

• KratzerSelkirk2020.isGiven [a] referent = (a = referent)
• KratzerSelkirk2020.isGiven aValue referent = False

@[implicit_reducible]

instance KratzerSelkirk2020.instDecidableIsGiven {α : Type u_1} [DecidableEq α] (aValue : List α) (referent : α) : Decidable (isGiven aValue referent)

Equations

• KratzerSelkirk2020.instDecidableIsGiven [a] referent = inferInstance
• KratzerSelkirk2020.instDecidableIsGiven [] referent = inferInstance
• KratzerSelkirk2020.instDecidableIsGiven (head :: head_1 :: tail) referent = inferInstance

def KratzerSelkirk2020.applyG {α : Type u_1} (m : Alternatives.AltMeaning α) : Alternatives.AltMeaning α

Apply [G] to a meaning: both values unchanged, but adds a definedness condition (the expression must be Given w.r.t. some discourse referent).

Unlike [FoC], [G] does NOT change the A-value. Its contribution is purely a presupposition on the discourse context.

Equations

• KratzerSelkirk2020.applyG m = m

theorem KratzerSelkirk2020.g_preserves_oValue {α : Type u_1} (m : Alternatives.AltMeaning α) : (applyG m).oValue = m.oValue

[G] preserves O-value. K&S (47): if defined, O-value unchanged.

theorem KratzerSelkirk2020.g_preserves_aValue {α : Type u_1} (m : Alternatives.AltMeaning α) : (applyG m).aValue = m.aValue

[G] preserves A-value. K&S (47): A-value unchanged.

Mutual exclusivity of [FoC] and [G]

A single constituent CANNOT bear both [FoC] and [G]. The proof follows from the A-value conditions:

• [FoC] requires A-value = D_τ (the full domain, maximally large)
• [G] requires A-value = {a} (a singleton) No semantic domain is both maximal and a singleton (assuming |D_τ| > 1).

theorem KratzerSelkirk2020.foc_g_exclusion {α : Type u_1} [DecidableEq α] (domain : List α) (referent : α) (h_domain : domain.length > 1) : ¬isGiven domain referent

[FoC] and [G] are mutually exclusive: no constituent can satisfy both the [FoC] A-value condition (full domain) and the [G] A-value condition (singleton) simultaneously, when the domain has more than one element.

Stated in K&S §8 prose immediately preceding (58): "It follows that no constituents can be both [G]-marked and [FoC]-marked." Distinct from (58) itself, which states the [G]-can-contain-[FoC]-only-with-consumption consequence.

Both features are use-conditional

Neither [FoC] nor [G] changes the truth-conditional (at-issue) content of the expression it attaches to. Both contribute use-conditional / expressive meaning.

This grounds K&S's features in Potts' two-dimensional semantics, already formalized in Expressives/Basic.lean.

def KratzerSelkirk2020.focAsTwoDim {W : Type u_1} (atIssue contrastPresup : W → Prop) : Pragmatics.Expressives.TwoDimProp W

[FoC] is use-conditional: at-issue content is unchanged. Grounded in TwoDimProp from Expressives/Basic.lean.

Equations

• KratzerSelkirk2020.focAsTwoDim atIssue contrastPresup = Pragmatics.Expressives.TwoDimProp.withCI atIssue contrastPresup

def KratzerSelkirk2020.gAsTwoDim {W : Type u_1} (atIssue givennessPresup : W → Prop) : Pragmatics.Expressives.TwoDimProp W

[G] is use-conditional: at-issue content is unchanged. [G] resembles discourse particles (German "ja", "doch") — it places a condition on context salience without affecting truth conditions.

Equations

• KratzerSelkirk2020.gAsTwoDim atIssue givennessPresup = Pragmatics.Expressives.TwoDimProp.withCI atIssue givennessPresup

theorem KratzerSelkirk2020.foc_at_issue_unchanged {W : Type u_1} (atIssue contrastPresup : W → Prop) : (focAsTwoDim atIssue contrastPresup).atIssue = atIssue

[FoC] does not change at-issue content (grounding theorem).

theorem KratzerSelkirk2020.g_at_issue_unchanged {W : Type u_1} (atIssue givennessPresup : W → Prop) : (gAsTwoDim atIssue givennessPresup).atIssue = atIssue

[G] does not change at-issue content (grounding theorem).

theorem KratzerSelkirk2020.foc_projects_through_neg {W : Type u_1} (atIssue contrastPresup : W → Prop) : (focAsTwoDim atIssue contrastPresup).neg.ci = (focAsTwoDim atIssue contrastPresup).ci

Both features project their use-conditional content through negation, just like conventional implicatures.

"It's not the case that [ELIZA]_{FoC} mailed the caramels" still contrasts Eliza with alternatives.

theorem KratzerSelkirk2020.g_projects_through_neg {W : Type u_1} (atIssue givennessPresup : W → Prop) : (gAsTwoDim atIssue givennessPresup).neg.ci = (gAsTwoDim atIssue givennessPresup).ci

Contrast representation

An expression α represents a contrast with discourse referent a iff: (i) a ∈ ⟦α⟧{A,C} — the referent is among the alternatives (ii) a ≠ ⟦α⟧{O,C} — the referent differs from the actual value (iii) There is no FoC/G-variant β of α with ⟦β⟧{A,C} ⊂ ⟦α⟧{A,C} and a ∈ ⟦β⟧_{A,C} — no smaller alternatives set also captures a

Condition (iii) prevents over-FoCusing.

structure KratzerSelkirk2020.Contrast (α : Type u_3) : Type u_3

Conditions (i) and (ii) of Contrast (K&S 49). Condition (iii) — the minimality condition — is structural and requires checking FoC/G-variants, which we leave to the prosodic spellout layer.

• aValue : List α

  The expression's A-value (alternatives)

• oValue : α

  The expression's O-value (ordinary denotation)

• referent : α

  The contrasting discourse referent

• ref_in_alts : self.referent ∈ self.aValue

  (i): referent is among the alternatives

• ref_ne_oValue : self.referent ≠ self.oValue

  (ii): referent differs from the O-value

The ~ operator

[FoC]-marked constituents must be c-commanded by a operator. The operator:

• Takes a set of discourse referents 𝔠 as its contextual variable
• Requires α to represent a contrast with each member of 𝔠
• Stops the propagation of alternatives (consumes them)
• Contributes expressive meaning: the contrast is signaled

Unlike Rooth's original (which allows questions as antecedents), K&S's always signals contrast. Questions do NOT have a special direct relation to FoCus.

structure KratzerSelkirk2020.ContrastOperator (α : Type u_3) : Type u_3

The ~ operator (K&S version, allowing multiple antecedents).

K&S (54): ⟦~𝔠 α⟧{O,C} is defined iff 𝔠 is a set of discourse referents in C, and α represents a contrast with each member of 𝔠.

If defined, ⟦𝔠 α⟧{O,C} = ⟦α⟧_{O,C} A-values: ⟦𝔠 α⟧{A,C} = {⟦α⟧_{O,C}} (singleton — alternatives consumed).

• meaning : Alternatives.AltMeaning α

  The expression's meaning

• antecedents : List α

  The contrasting discourse referent(s)

• antecedents_in_alts (a : α) : a ∈ self.antecedents → a ∈ self.meaning.aValue

  Each antecedent is in the alternatives

• antecedents_ne_oValue (a : α) : a ∈ self.antecedents → a ≠ self.meaning.oValue

  Each antecedent differs from the O-value

def KratzerSelkirk2020.ContrastOperator.result {α : Type u_3} (op : ContrastOperator α) : Alternatives.AltMeaning α

The ~ operator consumes alternatives: result A-value is singleton.

Equations

• op.result = { oValue := op.meaning.oValue, aValue := [op.meaning.oValue] }

theorem KratzerSelkirk2020.squiggle_preserves_oValue {α : Type u_3} (op : ContrastOperator α) : op.result.oValue = op.meaning.oValue

~ preserves O-value.

theorem KratzerSelkirk2020.squiggle_singleton_aValue {α : Type u_3} (op : ContrastOperator α) : op.result.aValue = [op.meaning.oValue]

~ collapses A-value to singleton.

Semantics of only

Their (55b) is the Roothian strong theory verbatim: association with only is indirect, mediated by two occurrences of the contextual variable ℭ — one on only, one on the ~ operator that comes with [FoC].

def KratzerSelkirk2020.onlySemantics {W : Type u_1} (contrastSet : List (W → Prop)) (prejacent : W → Prop) : Set W

Semantics of only with explicit contrast set (their (56)): λp λw. ∀q ((q ∈ ℭ ∧ q(w)) → q = p) — the strong-theory Semantics.Focus.onlyVia at the list-supplied contrast set, so the onlyVia lemmas (antitonicity, squiggle-resolved exclusion) apply.

Equations

• KratzerSelkirk2020.onlySemantics contrastSet prejacent = Semantics.Focus.onlyVia {q : Set W | q ∈ contrastSet} prejacent

[G] containing [FoC] requires alternatives consumption

A constituent α containing [FoC]-marked β can be [G]-marked only if α also contains an operator that consumes the alternatives generated by β.

Proof: For α to be [G], its A-value must be a singleton {a}. But [FoC] on β would make α's A-value non-singleton (alternatives propagate upward) UNLESS some operator inside α (like ~ or only) has consumed them.

This explains Second Occurrence Focus: in "the fáculty only quote [the faculty]_{FoC}", the second "the faculty" is [FoC]-marked but sits inside a [G]-marked VP. This is possible because only + ~ consume the alternatives before they reach the VP level.

theorem KratzerSelkirk2020.consumed_alts_enable_g {α : Type u_3} [DecidableEq α] (op : ContrastOperator α) : isGiven op.result.aValue op.meaning.oValue

After ~ consumption, the result A-value is a singleton, which is the precondition for [G]-marking.

theorem KratzerSelkirk2020.consumed_alts_given {α : Type u_3} (op : ContrastOperator α) : op.result.Given op.meaning.oValue

The ~-consumed result is Given with respect to the ordinary value — the AltMeaning.Given form of consumed_alts_enable_g (their (46)).

Prosodic spellout

In Standard American and British English, [FoC] and [G] are spelled out prosodically at the syntax-phonology interface (MSO → PI mapping).

The architecture has three levels:

• MSO: Morphosyntactic Output (syntactic structure with [FoC]/[G])
• PI: Phonological Input (prosodic constituency)
• PO: Phonological Output (tones, prominence)

Match constraints (MatchWord, MatchPhrase, MatchClause) generate prosodic constituency in PI from syntactic constituency in MSO. Then spellout constraints map [FoC] and [G] to prosodic properties.

inductive KratzerSelkirk2020.FoCSpellout : Type

Spellout of [FoC]: maps to head at a prosodic level. K&S (34, 43): [FoC] = {ω, φ, ι}-Level-Head.

A [FoC]-marked constituent in MSO is spelled out as a head at the corresponding prosodic level in PI. Being a head in a chain ending at ι means being the MOST PROMINENT constituent in the sentence.

• ω_level_head : FoCSpellout

  [FoC] = ω-Level-Head: head of prosodic word

• φ_level_head : FoCSpellout

  [FoC] = φ-Level-Head: head of phonological phrase

• ι_level_head : FoCSpellout

  [FoC] = ι-Level-Head: head of intonational phrase (highest prominence)

@[implicit_reducible]

instance KratzerSelkirk2020.instDecidableEqFoCSpellout : DecidableEq FoCSpellout

Equations

• KratzerSelkirk2020.instDecidableEqFoCSpellout x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KratzerSelkirk2020.instReprFoCSpellout.repr : FoCSpellout → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KratzerSelkirk2020.instReprFoCSpellout : Repr FoCSpellout

Equations

• KratzerSelkirk2020.instReprFoCSpellout = { reprPrec := KratzerSelkirk2020.instReprFoCSpellout.repr }

structure KratzerSelkirk2020.GSpellout : Type

Spellout of [G]: removes φ constituency (dephrasing). K&S (38): [G] = No-φ.

A [G]-marked constituent in MSO corresponds to a prosodic constituent in PI that is NOT a φ and contains no φ. The phonological consequences:

• No obligatory H accent tone (which requires φ-head status)
• No L edge tone (which requires φ-final position)

This replaces the traditional "destressing" analysis with a structural one.

• no_phi : Bool

  A [G]-marked constituent has no φ in PI

inductive KratzerSelkirk2020.SpelloutRanking : Type

K&S (44): When [G] and [FoC] spellout conflict, [G] wins.

Ranking in Standard American and British English: [G]=No-φ >> MatchPhrase >> [FoC]=φ-Level-Head

The [G] >> MatchPhrase part comes from (41); the [G] >> [FoC] part comes from (44).

This means: dephrasing a [G]-marked constituent takes priority over giving a [FoC]-marked constituent φ-level prominence.

Consequence: Second Occurrence Focus [FoC] inside [G] gets only ω-level head status, not φ-level. Hence reduced prosody for SOF.

• g_over_match : SpelloutRanking

  [G]=No-φ outranks MatchPhrase

• match_over_foc_phi : SpelloutRanking

  MatchPhrase outranks [FoC]=φ-Level-Head

@[implicit_reducible]

instance KratzerSelkirk2020.instDecidableEqSpelloutRanking : DecidableEq SpelloutRanking

Equations

• KratzerSelkirk2020.instDecidableEqSpelloutRanking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KratzerSelkirk2020.instReprSpelloutRanking : Repr SpelloutRanking

Equations

• KratzerSelkirk2020.instReprSpelloutRanking = { reprPrec := KratzerSelkirk2020.instReprSpelloutRanking.repr }

def KratzerSelkirk2020.instReprSpelloutRanking.repr : SpelloutRanking → ℕ → Std.Format

Equations

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

def KratzerSelkirk2020.englishSpelloutRanking : List SpelloutRanking

The ranking is fixed for Standard American and British English.

Equations

• KratzerSelkirk2020.englishSpelloutRanking = [KratzerSelkirk2020.SpelloutRanking.g_over_match, KratzerSelkirk2020.SpelloutRanking.match_over_foc_phi]

Second-occurrence focus

SOF is the strongest empirical argument for the two-feature system.

Example ([BCF+07], K&S 42): "Both Sid and his accomplices should have been named in this morning's court session. But the defendant only named [Síd]_{FoC} in court today."

MSO: Even [the prosecutor]{FoC} [only named [Sid]{FoC} in court today]_{G}

The second "Sid" is [FoC]-marked (it associates with only) but sits inside a [G]-marked constituent. The ranking [G]=No-φ >> [FoC]=φ-Level-Head predicts: Sid gets ω-level head status but NOT φ-level prominence. Result: an H accent but no phrase-level pitch scaling — exactly what [BCF+07] [Sel08] found experimentally.

structure KratzerSelkirk2020.SOFDatum : Type

A Second Occurrence Focus datum: [FoC] inside [G].

• sentence : String

  The full sentence

• sofWord : String

  The SOF word

• consumingOperator : String

  The operator that consumes SOF's alternatives

• hasHAccent : Bool

  Whether H accent present (yes for SOF)

• hasPhiProminence : Bool

  Whether φ-level prominence present (no for SOF)

• source : String

  Source

@[implicit_reducible]

instance KratzerSelkirk2020.instReprSOFDatum : Repr SOFDatum

Equations

• KratzerSelkirk2020.instReprSOFDatum = { reprPrec := KratzerSelkirk2020.instReprSOFDatum.repr }

def KratzerSelkirk2020.instReprSOFDatum.repr : SOFDatum → ℕ → Std.Format

Equations

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

def KratzerSelkirk2020.beaverEtAl2007_sid : SOFDatum

[BCF+07] SOF example.

Equations

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

structure KratzerSelkirk2020.ProsodicTripleDatum : Type

[KS11] FoC-New vs New-FoC vs New-New triples. K&S (36): Phonetic evidence distinguishing [FoC] from newness.

The K&S contrast here is FOCUS marking on otherwise-new material; "new" in their (36) means "non-focused new". FocusMark (binary focused vs non-focused) captures the relevant axis directly.

• firstFocus : Features.InformationStructure.FocusMark

  First post-verbal phrase focus marking

• secondFocus : Features.InformationStructure.FocusMark

  Second post-verbal phrase focus marking

• pitchPattern : String

  Description of the pitch pattern

• source : String

  Source

def KratzerSelkirk2020.instReprProsodicTripleDatum.repr : ProsodicTripleDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KratzerSelkirk2020.instReprProsodicTripleDatum : Repr ProsodicTripleDatum

Equations

• KratzerSelkirk2020.instReprProsodicTripleDatum = { reprPrec := KratzerSelkirk2020.instReprProsodicTripleDatum.repr }

def KratzerSelkirk2020.katzSelkirk2011_focNew : ProsodicTripleDatum

Equations

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

def KratzerSelkirk2020.katzSelkirk2011_newFoc : ProsodicTripleDatum

Equations

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

def KratzerSelkirk2020.katzSelkirk2011_newNew : ProsodicTripleDatum

Equations

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

Pragmatic pressure for [G]- and [FoC]-marking

[G]-marking and [FoC]-marking are obligatory under certain discourse conditions in Standard American and British English.

(61) Pressure for [G]-Marking: [G]-mark a constituent if it is Given w.r.t. a salient discourse referent.

(66) Pressure for [FoC]-Marking: Represent non-trivial contrasts with salient discourse referents.

These are not semantic/syntactic constraints but PRAGMATIC pressures, possibly reducible to Maximize Presuppositions.

structure KratzerSelkirk2020.PressureForG : Type

Pragmatic pressure for [G]-marking (K&S 61).

• constituent : String

  The constituent

• referent : String

  The salient discourse referent it matches

• obligatory : Bool

  Is [G]-marking obligatory here?

structure KratzerSelkirk2020.PressureForFoC : Type

Pragmatic pressure for [FoC]-marking (K&S 66).

• constituent : String

  The constituent

• referent : String

  The contrasting discourse referent

• faultedIfMissed : Bool

  Would failure to [FoC]-mark violate Pressure for [FoC]-Marking?

Bridge to Schwarzschild A-givenness

Schwarzschild's "A-Givenness" (within Rooth's Alternatives Semantics) falls out as a special case of K&S's [G]-feature.

A-Givenness: α is A-Given in C iff there is a salient discourse referent that is a member of ⟦α⟧_{A,C}.

K&S's Givenness (46): α is Given w.r.t. a iff ⟦α⟧_{A,C} = {a}.

K&S's condition is STRONGER (singleton vs membership). The old A-Givenness condition was too weak — Schwarzschild noted it was trivially satisfiable for universal quantifiers (every cat is a complainer → trivially A-Given).

def KratzerSelkirk2020.isAGiven {α : Type u_3} (aValue : List α) (referent : α) : Prop

Schwarzschild's A-Givenness: some referent is in the alternatives set.

Equations

• KratzerSelkirk2020.isAGiven aValue referent = (referent ∈ aValue)

@[implicit_reducible]

instance KratzerSelkirk2020.instDecidableIsAGiven {α : Type u_3} [DecidableEq α] (aValue : List α) (referent : α) : Decidable (isAGiven aValue referent)

Equations

• KratzerSelkirk2020.instDecidableIsAGiven aValue referent = KratzerSelkirk2020.instDecidableIsAGiven._aux_1 aValue referent

theorem KratzerSelkirk2020.givenness_entails_aGivenness {α : Type u_3} [DecidableEq α] (aValue : List α) (referent : α) (h : isGiven aValue referent) : isAGiven aValue referent

K&S Givenness entails Schwarzschild A-Givenness. If the alternatives set is a singleton {a}, then certainly a ∈ alternatives.

theorem KratzerSelkirk2020.aGivenness_not_sufficient : ∃ (aValue : List ℕ) (referent : ℕ), isAGiven aValue referent ∧ ¬isGiven aValue referent

The converse fails: A-Givenness does NOT entail K&S Givenness. A non-singleton alternatives set can satisfy A-Givenness but not Givenness.

This is the Schwarzschild overgeneration problem (K&S fn. 14): "Every cat is a complainer" is trivially A-Given because ∃P[every P is a complainer] is always true. K&S's singleton condition avoids this.

Hausa in situ vs ex situ (their fn. 21)

K&S contest [HZ07]'s conclusion that information focus is realised both in situ and ex situ in Hausa: without controlling for accommodated contrasts, an in-situ answer may be merely new and an ex-situ one contrastive. On the K&S inventory mere newness is not focus at all, so the reinterpretation is: ex situ realises [FoC], in situ is unmarked. The corpus tendencies both sides cite (their fn. 21; H&Z §3.3: 99 vs 25 in situ for new information, 154 vs 12 ex situ for the contrastive family) fit the reinterpretation; the accounts genuinely diverge only on the minority cells, which is where the accommodation caveat does its work.

def KratzerSelkirk2020.IsFoCus : Semantics.Focus.Use → Prop

The K&S inventory over H&Z's pragmatic-use taxonomy: the contrastive family is [FoC]; new-information focus is mere newness — no feature at all.

Equations

• KratzerSelkirk2020.IsFoCus Semantics.Focus.Use.newInfo = False
• KratzerSelkirk2020.IsFoCus x✝ = True

@[implicit_reducible]

instance KratzerSelkirk2020.instDecidableIsFoCus (u : Semantics.Focus.Use) : Decidable (IsFoCus u)

Equations

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

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

The fn. 21 reinterpretation of Hausa: ex-situ realisation ↔ [FoC].

Equations

• KratzerSelkirk2020.KSHausaReading u = (u.cfg.strategy = Hausa.Strategy.exSitu ↔ KratzerSelkirk2020.IsFoCus u.pragType)

@[implicit_reducible]

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

Equations

• KratzerSelkirk2020.instDecidableKSHausaReading u = KratzerSelkirk2020.instDecidableKSHausaReading._aux_1 u

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

The two accounts diverge on H&Z's own matrix: the ex-situ new-information cell (their (22)) and the in-situ corrective cell (their (25)) both violate the reinterpretation. These are exactly the cells the accommodation caveat targets — the divergence is real but undecided on minimal pairs, and the corpus asymmetry is the evidence both sides invoke.