Holmberg (2016): The Syntax of Yes and No

[Hol16]

Core Contribution

A cross-linguistic typology of polar question answering. The central parameter is the answering system: truth-based vs polarity-based.

Answers as Elliptical Clauses

Yes/no answers are elliptical full clauses, not general fragments:

[FocP yes/no Foc⁰ [PolP ... [±Pol] ... ]]

The PolP is elided under identity with the question's PolP; the particle sits in Spec-FocP and values the [±Pol] feature. This is distinct from wh-fragment answers, which fill an argument slot of a wh-question (cf. Studies/BergenGoodman2015.lean).

Key Claims Formalized

1. Hamblin ↔ [±Pol]: Hamblin's polar p yields exactly two answer cells, corresponding to [+Pol] and [-Pol] valuations.

2. Answering system divergence: Truth-based and polarity-based systems give opposite answers to negative questions.

3. Polarity reversal: Languages like Swedish (jo), German (doch), and French (si) have a dedicated particle that assigns [+Pol] while contradicting a negative context.

Connection to Existing Infrastructure

• Question.polar (substrate-level inquisitive polar question)
• PolFeature (syntactic [±Pol] feature; relocated from Minimalist/Polarity.lean)
• AnsweringSystem (typological parameter)
• NegationHeight → predictedSystem (negation height derives answering system)
• PolarAnswerProfile (per-language classification)
• VerumFocus.lean ([RH04]): complementary analysis — VERUM explains structural source of bias, Holmberg explains cross-linguistic answer variation. Both derive unbalanced partitions for negative questions.

Syntactic polarity: PolP and [±Pol] (relocated from Minimalist/Polarity.lean)

Syntactic polarity as a formal feature on the PolP functional head, connecting [Lak90]'s ΣP and [Hol16]'s analysis of yes/no answers.

Key Claims

1. Every finite clause has a polarity head (Pol⁰) projecting PolP in the IP domain
2. In declaratives, [±Pol] is valued: [+Pol] for affirmative, [-Pol] for negative
3. In polar questions, [±Pol] is unvalued — the answer values it
4. "Yes"/"No" are focus-movement remnants of PolP ellipsis under identity

Connection to Features.Polarity

Features.Polarity provides the semantic type (.positive / .negative). This file provides the syntactic feature [±Pol] that participates in Agree and maps to Features.Polarity at LF.

Connection to Cat.Pol

Minimalist.Cat.Pol is the categorial label for the polarity head. This file adds the feature infrastructure for what that head carries.

inductive Holmberg2016.PolFeature : Type

The polarity feature on Pol⁰, which may be valued or unvalued.

In declaratives: valued [+Pol] or [-Pol] In polar questions: unvalued [uPol] — waiting for an answer to value it

• valued : Features.Polarity → PolFeature

  Valued polarity: [+Pol] (affirmative) or [-Pol] (negative)

• unvalued : PolFeature

  Unvalued polarity: the feature in polar questions that the answer resolves

@[implicit_reducible]

instance Holmberg2016.instDecidableEqPolFeature : DecidableEq PolFeature

Equations

• Holmberg2016.instDecidableEqPolFeature = Holmberg2016.instDecidableEqPolFeature.decEq

def Holmberg2016.instDecidableEqPolFeature.decEq (x✝ x✝¹ : PolFeature) : Decidable (x✝ = x✝¹)

Equations

• Holmberg2016.instDecidableEqPolFeature.decEq (Holmberg2016.PolFeature.valued a) (Holmberg2016.PolFeature.valued b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Holmberg2016.instDecidableEqPolFeature.decEq (Holmberg2016.PolFeature.valued a) Holmberg2016.PolFeature.unvalued = isFalse ⋯
• Holmberg2016.instDecidableEqPolFeature.decEq Holmberg2016.PolFeature.unvalued (Holmberg2016.PolFeature.valued a) = isFalse ⋯
• Holmberg2016.instDecidableEqPolFeature.decEq Holmberg2016.PolFeature.unvalued Holmberg2016.PolFeature.unvalued = isTrue ⋯

def Holmberg2016.instReprPolFeature.repr : PolFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Holmberg2016.instReprPolFeature : Repr PolFeature

Equations

• Holmberg2016.instReprPolFeature = { reprPrec := Holmberg2016.instReprPolFeature.repr }

def Holmberg2016.PolFeature.toFeatureVal : PolFeature → Minimalist.GramFeature

Convert a PolFeature to a FeatureVal for use in the Agree system. [+Pol] maps to .pol true, [-Pol] maps to .pol false.

Equations

• (Holmberg2016.PolFeature.valued Features.Polarity.positive).toFeatureVal = Minimalist.GramFeature.valued (Minimalist.FeatureVal.pol true)
• (Holmberg2016.PolFeature.valued Features.Polarity.negative).toFeatureVal = Minimalist.GramFeature.valued (Minimalist.FeatureVal.pol false)
• Holmberg2016.PolFeature.unvalued.toFeatureVal = Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.pol true)

def Holmberg2016.PolFeature.toPolarity : PolFeature → Option Features.Polarity

Recover Features.Polarity from a valued syntactic [±Pol] feature.

Equations

• (Holmberg2016.PolFeature.valued a).toPolarity = some a
• Holmberg2016.PolFeature.unvalued.toPolarity = none

structure Holmberg2016.PolHead : Type

A Pol⁰ head: the functional head projecting PolP.

In [Hol16]'s analysis, every finite clause has a Pol⁰ bearing a [±Pol] feature. The head's category is Cat.Pol.

• feature : PolFeature

  The polarity feature on this head

• inQuestion : Bool

  Is this in a question context (unvalued [±Pol])?

@[implicit_reducible]

instance Holmberg2016.instReprPolHead : Repr PolHead

Equations

• Holmberg2016.instReprPolHead = { reprPrec := Holmberg2016.instReprPolHead.repr }

def Holmberg2016.instReprPolHead.repr : PolHead → ℕ → Std.Format

Equations

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

def Holmberg2016.PolHead.affirmative : PolHead

An affirmative declarative Pol⁰: [+Pol]

Equations

• Holmberg2016.PolHead.affirmative = { feature := Holmberg2016.PolFeature.valued Features.Polarity.positive }

def Holmberg2016.PolHead.negative : PolHead

A negative declarative Pol⁰: [-Pol]

Equations

• Holmberg2016.PolHead.negative = { feature := Holmberg2016.PolFeature.valued Features.Polarity.negative }

def Holmberg2016.PolHead.question : PolHead

A polar question Pol⁰: [uPol]

Equations

• Holmberg2016.PolHead.question = { feature := Holmberg2016.PolFeature.unvalued }

def Holmberg2016.PolFeature.value (f : PolFeature) (p : Features.Polarity) : Option PolFeature

Value an unvalued [±Pol] feature — the core operation in answering a polar question. The answer provides a Features.Polarity that values the feature.

Returns none if the feature is already valued (nothing to do).

Equations

• Holmberg2016.PolFeature.unvalued.value p = some (Holmberg2016.PolFeature.valued p)
• (Holmberg2016.PolFeature.valued a).value p = none

theorem Holmberg2016.value_unvalued (p : Features.Polarity) : PolFeature.unvalued.value p = some (PolFeature.valued p)

Valuing an unvalued feature always succeeds.

theorem Holmberg2016.value_valued (p q : Features.Polarity) : (PolFeature.valued p).value q = none

Valuing a valued feature always fails.

theorem Holmberg2016.value_then_toPolarity (p : Features.Polarity) : (PolFeature.unvalued.value p).bind PolFeature.toPolarity = some p

Round-trip: valuing then extracting polarity recovers the answer.

theorem Holmberg2016.pol_feature_matches : (Minimalist.FeatureVal.pol true).sameType (Minimalist.FeatureVal.pol false) = true

The [±Pol] feature matches itself in the Agree system.

theorem Holmberg2016.pol_ne_neg : (Minimalist.FeatureVal.pol true).sameType (Minimalist.FeatureVal.neg true) = false

[±Pol] is distinct from [±neg]: polarity and negation are separate features on separate heads (PolP vs NegP).

Question syntax: ForceP/FinP/PolP (relocated from Minimalist/Questions.lean)

Syntactic projections involved in question formation.

Clause Structure for Polar Questions

[Riz97]'s split-CP and [Hol16]'s PolP analysis give the following structure for a polar question:

[ForceP Force⁰[+Q] [FinP Fin⁰[+finite] [PolP Pol⁰[uPol] [TP ...]]]]

• ForceP: Clause-typing head. Force⁰ bears [+Q] for interrogatives, [-Q] for declaratives. Corresponds to Cat.Force and FeatureVal.q.
• FinP: Finiteness head. Fin⁰ bears [±finite]. Corresponds to Cat.Fin and FeatureVal.finite.
• PolP: Polarity head. Pol⁰ bears valued [±Pol] in declaratives, unvalued [uPol] in polar questions. Corresponds to Cat.Pol and FeatureVal.pol. See Minimalist.Polarity for the Agree infrastructure.

Connection to Semantic Questions

Minimalist.LeftPeriphery defines WHFeature (±WH on C) — the semantic clause-typing feature. The syntactic FeatureVal.q corresponds to the semantic WHFeature:

• FeatureVal.q true ↔ WHFeature.plusWH
• FeatureVal.q false ↔ WHFeature.minusWH

Cross-framework: clause-typing locus is contested

This file places clause-typing at Force⁰[+Q] per [Riz97]. Two sibling analyses in linglib place it elsewhere:

• [Day25] (Studies/Dayal2025.lean): clause-typing locus is C for CP-typed languages (English, Italian) and PerspP for PerspP-typed languages (Hindi-Urdu).
• [Hol16] (Studies/Holmberg2016.lean): the answering-system parameter places polar-Q-typing at Pol⁰ via Features/AnsweringSystem.lean.

The bridge theorems (Force⁰[+Q] ↔ C[+WH], Force⁰[+Q] ↔ Pol⁰[uPol]) are unformalized — silent divergences, not committed disagreements.

Connection to ClauseType

A clause's Semantics.Mood.ClauseType (force × mood) is determined by the syntactic projections:

• Force⁰[+Q] → IllocutionaryMood.interrogative
• Force⁰[-Q] → IllocutionaryMood.declarative
• Mood is determined lower (by T/Fin morphology), not by ForceP.

inductive Holmberg2016.QFeature : Type

The Q-feature on Force⁰: [+Q] for interrogatives, [-Q] for declaratives.

• plusQ : QFeature
• minusQ : QFeature

@[implicit_reducible]

instance Holmberg2016.instDecidableEqQFeature : DecidableEq QFeature

Equations

• Holmberg2016.instDecidableEqQFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Holmberg2016.instReprQFeature : Repr QFeature

Equations

• Holmberg2016.instReprQFeature = { reprPrec := Holmberg2016.instReprQFeature.repr }

def Holmberg2016.instReprQFeature.repr : QFeature → ℕ → Std.Format

Equations

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

def Holmberg2016.QFeature.toFeatureVal : QFeature → Minimalist.FeatureVal

Map the Q-feature to a FeatureVal for the Agree system.

Equations

• Holmberg2016.QFeature.plusQ.toFeatureVal = Minimalist.FeatureVal.q true
• Holmberg2016.QFeature.minusQ.toFeatureVal = Minimalist.FeatureVal.q false

def Holmberg2016.QFeature.toForce : QFeature → Semantics.Mood.IllocutionaryMood

Map the Q-feature to illocutionary force.

Equations

• Holmberg2016.QFeature.plusQ.toForce = Semantics.Mood.IllocutionaryMood.interrogative
• Holmberg2016.QFeature.minusQ.toForce = Semantics.Mood.IllocutionaryMood.declarative

def Holmberg2016.polarQuestionSpine : Minimalist.ClauseSpine

The clause spine for a polar question: V ... T ... Pol ... Fin ... Force.

This is the full IP-to-CP spine with the projections relevant to [Hol16]'s analysis. The Pol head is between T and Fin.

Equations

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

def Holmberg2016.declarativeSpine : Minimalist.ClauseSpine

A declarative spine has the same projections.

Equations

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

theorem Holmberg2016.polP_always_projected : polarQuestionSpine.projects Minimalist.Cat.Pol = true ∧ declarativeSpine.projects Minimalist.Cat.Pol = true

PolP is projected in both declaratives and polar questions.

def Holmberg2016.clauseType (q : QFeature) (m : Semantics.Mood.GramMood) : Semantics.Mood.ClauseType

Derive ClauseType from the syntactic features on Force⁰ and T⁰/Fin⁰.

The Q-feature on Force determines illocutionary force; mood is determined by the morphological properties of the verb (indicative vs subjunctive), independent of Force.

Equations

• Holmberg2016.clauseType q m = { force := q.toForce, mood := m }

theorem Holmberg2016.polar_question_is_interrogative_indicative : clauseType QFeature.plusQ Semantics.Mood.GramMood.indicative = Semantics.Mood.ClauseType.polarQuestion

A polar question with indicative mood.

theorem Holmberg2016.declarative_is_decl_ind : clauseType QFeature.minusQ Semantics.Mood.GramMood.indicative = Semantics.Mood.ClauseType.declInd

A declarative with indicative mood.

theorem Holmberg2016.force_from_forceP_mood_from_fin : (clauseType QFeature.plusQ Semantics.Mood.GramMood.indicative).force = Semantics.Mood.IllocutionaryMood.interrogative ∧ (clauseType QFeature.plusQ Semantics.Mood.GramMood.subjunctive).force = Semantics.Mood.IllocutionaryMood.interrogative ∧ (clauseType QFeature.plusQ Semantics.Mood.GramMood.indicative).mood = Semantics.Mood.GramMood.indicative ∧ (clauseType QFeature.plusQ Semantics.Mood.GramMood.subjunctive).mood = Semantics.Mood.GramMood.subjunctive

Force and mood are independently set by different heads.

A polar question ?p = {p, pᶜ} (substrate Question.polar) corresponds to an unvalued [±Pol] feature. Each alternative cell values the feature: - p → [+Pol] (affirmative) - pᶜ → [-Pol] (negative)

The two alternatives are the "positive cell" and "negative cell"
of the partition induced by the question. 

theorem Holmberg2016.both_alternatives_in_polar {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : p ∈ (Question.polar p).alt ∧ pᶜ ∈ (Question.polar p).alt

Both alternatives p and pᶜ lie in alt (polar p) (under nontriviality). Substrate identification of the two-cell answer partition.

def Holmberg2016.positiveToPolFeature : PolFeature

The positive answer maps to [+Pol] (valued positive).

Equations

• Holmberg2016.positiveToPolFeature = Holmberg2016.PolFeature.valued Features.Polarity.positive

def Holmberg2016.negativeToPolFeature : PolFeature

The negative answer maps to [-Pol] (valued negative).

Equations

• Holmberg2016.negativeToPolFeature = Holmberg2016.PolFeature.valued Features.Polarity.negative

theorem Holmberg2016.positive_valuation : PolFeature.unvalued.value Features.Polarity.positive = some positiveToPolFeature

Valuing [uPol] as positive gives [+Pol].

theorem Holmberg2016.negative_valuation : PolFeature.unvalued.value Features.Polarity.negative = some negativeToPolFeature

Valuing [uPol] as negative gives [-Pol].

theorem Holmberg2016.diagnostic_prediction : Features.AnsweringSystem.truthBased.yesToNegativeQuestion = Features.Polarity.negative ∧ Features.AnsweringSystem.polarityBased.yesToNegativeQuestion = Features.Polarity.positive

The central diagnostic: "Doesn't he drink?" → "Yes" means...

• Truth-based: "He doesn't drink" (negative polarity)
• Polarity-based: "He does drink" (positive polarity)

def Holmberg2016.englishProfile : Features.PolarAnswerProfile

English polar answer profile (polarity-based, particle).

Equations

• Holmberg2016.englishProfile = { system := Features.AnsweringSystem.polarityBased, strategy := Features.AnswerStrategy.particle }

def Holmberg2016.japaneseProfile : Features.PolarAnswerProfile

Japanese polar answer profile (truth-based, particle).

Equations

• Holmberg2016.japaneseProfile = { system := Features.AnsweringSystem.truthBased, strategy := Features.AnswerStrategy.particle }

def Holmberg2016.swedishProfile : Features.PolarAnswerProfile

Swedish polar answer profile (three-way: ja/nej/jo). Derived from Swedish.AnswerParticles.profile.

Equations

• Holmberg2016.swedishProfile = Swedish.AnswerParticles.profile

theorem Holmberg2016.reversal_class : Swedish.AnswerParticles.jo.IsReversal ∧ German.PolarityMarking.dochAnswer.IsReversal

The cross-linguistic polarity-reversal class: Swedish jo and German doch have the same assign/respond profile — [+Pol] assignment restricted to negative antecedent contexts. Holmberg's class membership derived from the fragments' profiles rather than stipulated.

def Holmberg2016.finnishProfile : Features.PolarAnswerProfile

Finnish polar answer profile (mixed: verb echo + kyllä, polarity-based).

Equations

• Holmberg2016.finnishProfile = { system := Features.AnsweringSystem.polarityBased, strategy := Features.AnswerStrategy.mixed }

def Holmberg2016.mandarinProfile : Features.PolarAnswerProfile

Mandarin polar answer profile (mixed: V-not-V + shì/bú shì, truth-based).

Equations

• Holmberg2016.mandarinProfile = { system := Features.AnsweringSystem.truthBased, strategy := Features.AnswerStrategy.mixed }

theorem Holmberg2016.english_swedish_same_system : englishProfile.system = swedishProfile.system

English and Swedish are both polarity-based.

theorem Holmberg2016.japanese_mandarin_same_system : japaneseProfile.system = mandarinProfile.system

Japanese and Mandarin are both truth-based.

theorem Holmberg2016.english_japanese_differ : englishProfile.system ≠ japaneseProfile.system

English and Japanese differ in answering system.

theorem Holmberg2016.swedish_reversal_english_not : swedishProfile.hasPolarityReversal = true ∧ englishProfile.hasPolarityReversal = false

Swedish has polarity reversal; English does not.

theorem Holmberg2016.system_strategy_orthogonal : englishProfile.strategy = japaneseProfile.strategy ∧ englishProfile.system ≠ japaneseProfile.system

The answering system and answer strategy are orthogonal: both truth-based and polarity-based systems can use particles.

theorem Holmberg2016.japanese_negation_height_predicts : Features.NegationHeight.low.predictedSystem = japaneseProfile.system

Japanese has low negation → truth-based predicted, matches actual profile.

theorem Holmberg2016.mandarin_negation_height_predicts : Features.NegationHeight.low.predictedSystem = mandarinProfile.system

Mandarin has low negation → truth-based predicted, matches actual profile.

theorem Holmberg2016.english_negation_height_predicts : Features.NegationHeight.middle.predictedSystem = englishProfile.system

English has middle negation → polarity-based predicted, matches actual profile.

theorem Holmberg2016.swedish_negation_height_predicts : Features.NegationHeight.middle.predictedSystem = swedishProfile.system

Swedish has middle negation (exclusively, no low negation; §4.5) → polarity-based predicted, matches actual profile.

theorem Holmberg2016.finnish_negation_height_predicts : Features.NegationHeight.middle.predictedSystem = finnishProfile.system

Finnish has middle negation (higher variety of middle; §4.6, p178: "still technically a middle negation position") → polarity-based predicted, matches actual profile.

def Holmberg2016.polarityFeature : Features.Polarity → String

The paperFeatures encoding of a Features.Polarity value, matching the answer_polarity key in Holmberg2016.Examples.

Equations

• Holmberg2016.polarityFeature Features.Polarity.positive = "positive"
• Holmberg2016.polarityFeature Features.Polarity.negative = "negative"

theorem Holmberg2016.japanese_endtoend : List.lookup "answer_polarity" Examples.japanese_hai_to_neg.paperFeatures = some (polarityFeature Features.NegationHeight.low.predictedSystem.yesToNegativeQuestion)

End-to-end: Japanese low negation → truth-based → "yes" to negative question has negative polarity → matches the Japanese hai datum's answer_polarity annotation.

theorem Holmberg2016.english_endtoend : List.lookup "answer_polarity" Examples.english_yes_to_neg.paperFeatures = some (polarityFeature Features.NegationHeight.middle.predictedSystem.yesToNegativeQuestion)

End-to-end: English middle negation → polarity-based → "yes" to negative question has positive polarity → matches the English "yes" datum's answer_polarity annotation.

theorem Holmberg2016.endtoend_diverge : Features.NegationHeight.low.predictedSystem.yesToNegativeQuestion ≠ Features.NegationHeight.middle.predictedSystem.yesToNegativeQuestion

The end-to-end chains for Japanese and English yield opposite polarities, as predicted by their different negation heights.

[Hol16] §4.13: languages with a polarity-reversing particle (Swedish jo, German doch, French si) are correlated with the polarity-based system. Truth-based languages do not need a reversing particle because they can always use "no" to disconfirm the negative alternative of a negative question.

theorem Holmberg2016.truthBased_no_reversal : japaneseProfile.hasPolarityReversal = false ∧ mandarinProfile.hasPolarityReversal = false

Truth-based languages do not have polarity reversal in our profiles. (Japanese and Mandarin both lack a reversing particle.)

theorem Holmberg2016.polarityBased_reversal_variation : swedishProfile.hasPolarityReversal = true ∧ englishProfile.hasPolarityReversal = false

Among polarity-based languages, reversal is attested but not universal: Swedish has it, English does not.