inductive Semantics.Focus.KratzerSelkirk2020.ISFeature : Type

The two privative morphosyntactic features of @cite{kratzer-selkirk-2020}.

[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).

instance Semantics.Focus.KratzerSelkirk2020.instDecidableEqISFeature : DecidableEq ISFeature

Equations

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

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

Equations

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

instance Semantics.Focus.KratzerSelkirk2020.instReprISFeature : Repr ISFeature

Equations

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

def Semantics.Focus.KratzerSelkirk2020.instBEqISFeature.beq : ISFeature → ISFeature → Bool

Equations

• Semantics.Focus.KratzerSelkirk2020.instBEqISFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Focus.KratzerSelkirk2020.instBEqISFeature : BEq ISFeature

Equations

• Semantics.Focus.KratzerSelkirk2020.instBEqISFeature = { beq := Semantics.Focus.KratzerSelkirk2020.instBEqISFeature.beq }

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

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

Equations

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

§8 (45). The 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 Semantics.Focus.KratzerSelkirk2020.applyFoC {α : Type} (m : Core.InformationStructure.AltMeaning α) (domain : List α) : Core.InformationStructure.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

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

theorem Semantics.Focus.KratzerSelkirk2020.foc_preserves_oValue {α : Type} (m : Core.InformationStructure.AltMeaning α) (domain : List α) : (applyFoC m domain).oValue = m.oValue

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

§8 (46-47). The 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 Semantics.Focus.KratzerSelkirk2020.isGiven {α : Type} [BEq α] (aValue : List α) (referent : α) : Bool

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

• Semantics.Focus.KratzerSelkirk2020.isGiven [a] referent = (a == referent)
• Semantics.Focus.KratzerSelkirk2020.isGiven aValue referent = false

def Semantics.Focus.KratzerSelkirk2020.applyG {α : Type} (m : Core.InformationStructure.AltMeaning α) : Core.InformationStructure.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

• Semantics.Focus.KratzerSelkirk2020.applyG m = m

theorem Semantics.Focus.KratzerSelkirk2020.g_preserves_oValue {α : Type} (m : Core.InformationStructure.AltMeaning α) : (applyG m).oValue = m.oValue

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

theorem Semantics.Focus.KratzerSelkirk2020.g_preserves_aValue {α : Type} (m : Core.InformationStructure.AltMeaning α) : (applyG m).aValue = m.aValue

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

§8 (58). [FoC] and [G] are Mutually Exclusive

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 Semantics.Focus.KratzerSelkirk2020.foc_g_exclusion {α : Type} [BEq α] (domain : List α) (referent : α) (h_domain : domain.length > 1) : ¬isGiven domain referent = true

[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.

K&S (58, first part): follows from the incompatibility of A-value conditions.

§8 (45, 47). 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 Semantics.Focus.KratzerSelkirk2020.focAsTwoDim {W : Type u_1} (atIssue contrastPresup : BProp W) : Lexical.Expressives.TwoDimProp W

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

Equations

• Semantics.Focus.KratzerSelkirk2020.focAsTwoDim atIssue contrastPresup = Semantics.Lexical.Expressives.TwoDimProp.withCI atIssue contrastPresup

def Semantics.Focus.KratzerSelkirk2020.gAsTwoDim {W : Type u_1} (atIssue givennessPresup : BProp W) : Lexical.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

• Semantics.Focus.KratzerSelkirk2020.gAsTwoDim atIssue givennessPresup = Semantics.Lexical.Expressives.TwoDimProp.withCI atIssue givennessPresup

theorem Semantics.Focus.KratzerSelkirk2020.foc_at_issue_unchanged {W : Type u_1} (atIssue contrastPresup : BProp W) : (focAsTwoDim atIssue contrastPresup).atIssue = atIssue

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

theorem Semantics.Focus.KratzerSelkirk2020.g_at_issue_unchanged {W : Type u_1} (atIssue givennessPresup : BProp W) : (gAsTwoDim atIssue givennessPresup).atIssue = atIssue

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

theorem Semantics.Focus.KratzerSelkirk2020.foc_projects_through_neg {W : Type u_1} (atIssue contrastPresup : BProp W) : (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 Semantics.Focus.KratzerSelkirk2020.g_projects_through_neg {W : Type u_1} (atIssue givennessPresup : BProp W) : (gAsTwoDim atIssue givennessPresup).neg.ci = (gAsTwoDim atIssue givennessPresup).ci

§8 (49). 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 Semantics.Focus.KratzerSelkirk2020.Contrast (α : Type) [BEq α] : Type

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) = false

  (ii): referent differs from the O-value

§8 (53-54). 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 Semantics.Focus.KratzerSelkirk2020.ContrastOperator (α : Type) [BEq α] : Type

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 : Core.InformationStructure.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) = false

  Each antecedent differs from the O-value

def Semantics.Focus.KratzerSelkirk2020.ContrastOperator.result {α : Type} [BEq α] (op : ContrastOperator α) : Core.InformationStructure.AltMeaning α

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

Equations

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

theorem Semantics.Focus.KratzerSelkirk2020.squiggle_preserves_oValue {α : Type} [BEq α] (op : ContrastOperator α) : op.result.oValue = op.meaning.oValue

~ preserves O-value.

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

~ collapses A-value to singleton.

§8 (56). The Semantics of only

K&S's only directly takes a contextual variable 𝔠 (the contrast set), rather than accessing focus alternatives indirectly:

⟦only_𝔠⟧ = λp λw. ∀q. (q ∈ 𝔠 ∧ q(w)) → q = p

The contrast set 𝔠 is supplied by the operator that comes with [FoC]. Since stops alternative propagation, only associates with [FoC] indirectly via a second occurrence of 𝔠.

def Semantics.Focus.KratzerSelkirk2020.onlySemantics {W : Type u_1} (contrastSet : List (BProp W)) (prejacent : BProp W) (w : W) : Bool

Semantics of only with explicit contrast set (K&S 56). Takes a contrast set 𝔠 and a prejacent proposition p. True at w iff every true member of 𝔠 equals p.

Equations

• Semantics.Focus.KratzerSelkirk2020.onlySemantics contrastSet prejacent w = contrastSet.all fun (q : BProp W) => !q w || q w == prejacent w

§8 (58). [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 Semantics.Focus.KratzerSelkirk2020.consumed_alts_enable_g {α : Type} [BEq α] [LawfulBEq α] (op : ContrastOperator α) : isGiven op.result.aValue op.meaning.oValue = true

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

§7. 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 Semantics.Focus.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)

instance Semantics.Focus.KratzerSelkirk2020.instDecidableEqFoCSpellout : DecidableEq FoCSpellout

Equations

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

instance Semantics.Focus.KratzerSelkirk2020.instReprFoCSpellout : Repr FoCSpellout

Equations

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

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

Equations

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

structure Semantics.Focus.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 Semantics.Focus.KratzerSelkirk2020.SpelloutRanking : Type

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

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

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

instance Semantics.Focus.KratzerSelkirk2020.instDecidableEqSpelloutRanking : DecidableEq SpelloutRanking

Equations

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

instance Semantics.Focus.KratzerSelkirk2020.instReprSpelloutRanking : Repr SpelloutRanking

Equations

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

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

Equations

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

def Semantics.Focus.KratzerSelkirk2020.englishSpelloutRanking : List SpelloutRanking

The ranking is fixed for Standard American and British English.

Equations

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

§4, §7.3. Second Occurrence Focus

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

Example (@cite{beaver-2007}, 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 @cite{beaver-2007} @cite{selkirk-2008} found experimentally.

structure Semantics.Focus.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

instance Semantics.Focus.KratzerSelkirk2020.instReprSOFDatum : Repr SOFDatum

Equations

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

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

Equations

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

def Semantics.Focus.KratzerSelkirk2020.beaverEtAl2007_sid : SOFDatum

@cite{beaver-2007} SOF example.

Equations

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

structure Semantics.Focus.KratzerSelkirk2020.ProsodicTripleDatum : Type

@cite{katz-selkirk-2011} FoC-New vs New-FoC vs New-New triples. K&S (36): Phonetic evidence distinguishing [FoC] from newness.

• firstStatus : Core.InformationStructure.DiscourseStatus

  First post-verbal phrase status

• secondStatus : Core.InformationStructure.DiscourseStatus

  Second post-verbal phrase status

• pitchPattern : String

  Description of the pitch pattern

• source : String

  Source

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

Equations

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

instance Semantics.Focus.KratzerSelkirk2020.instReprProsodicTripleDatum : Repr ProsodicTripleDatum

Equations

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

def Semantics.Focus.KratzerSelkirk2020.katzSelkirk2011_focNew : ProsodicTripleDatum

Equations

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

def Semantics.Focus.KratzerSelkirk2020.katzSelkirk2011_newFoc : ProsodicTripleDatum

Equations

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

def Semantics.Focus.KratzerSelkirk2020.katzSelkirk2011_newNew : ProsodicTripleDatum

Equations

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

§8 (61, 66). Pressure for [G]-Marking 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 Semantics.Focus.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 Semantics.Focus.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: K&S vs @cite{schwarzschild-1999}

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 Semantics.Focus.KratzerSelkirk2020.isAGiven {α : Type} [BEq α] (aValue : List α) (referent : α) : Bool

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

Equations

• Semantics.Focus.KratzerSelkirk2020.isAGiven aValue referent = aValue.any fun (x : α) => x == referent

theorem Semantics.Focus.KratzerSelkirk2020.givenness_entails_aGivenness {α : Type} [BEq α] [LawfulBEq α] (aValue : List α) (referent : α) (h : isGiven aValue referent = true) : isAGiven aValue referent = true

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

theorem Semantics.Focus.KratzerSelkirk2020.aGivenness_not_sufficient : ∃ (aValue : List ℕ) (referent : ℕ), isAGiven aValue referent = true ∧ isGiven aValue referent = false

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.