Holmberg (2016): The Syntax of Yes and No

This file formalizes Holmberg's account of answers to yes–no questions. A polar interrogative contains an unvalued polarity head whose two values yield the Hamblin set it denotes, the same for a negative interrogative as for its positive counterpart (PolarInterrogative.denote_eq_polar_radical), and an answer is a full sentence: a focused valued polarity feature, spelled out by a particle or an echoed verb, merged with the clause inherited from the question and eliding it, so that it chooses one of the two alternatives (smul_mem_alt). The particles of English, Swedish, French and Japanese spell out the features english, swedish, french and japanese. The two systems for answering negative questions follow from the syntax of negation (AnswerFeature.answer): a middle negation values the polarity head before the particle can, so a plain affirmative clashes and the negative particle confirms the negative alternative, while a low negation is out of reach, so yes confirms the negative alternative and no is a double negation. English speakers who read not low and those who read it middle both take a bare answer to Is John not coming? to mean that he is not coming (negative_neutralization); an adverb preceding not forces the low reading, and in Swedish, which has no low negation, an adverb screens the middle negation from the polarity head to the same effect (swedish_adverb).

Section 4.4 defines the polarity-based system as the one lacking low negation (PolarityBased), which is the typology's: its affirmative particle never confirms the negative alternative of a negative question (polarityBased_iff_not_confirmsNegativeQuestion). Such a language has no negative neutralization (PolarityBased.answer_ne_negative); Swedish, whose negation is never low, is one (swedish_polarityBased), so confirming the positive alternative of a negative question takes the polarity-reversing jo (swedish_negative_question), which a truth-based configuration never needs (no_reversal_needed_truth_based). Crediting the REV feature to Farkas and Bruce, the mechanism derives what they say si and doch mark: the answers a reversing feature gives are their [reverse, +] answers (responses_reversing_eq_reversePositive). Positive-bias questions carry a high negation outside the inherited clause and are answered like neutral questions (high_answers_like_neutral). Which negations an English polar question form carries depends on the speaker's variety (negations): a question with not has the inner reading for all speakers (primaryPolarity_of_mem_negations_nonPreposed), and one with -n't only the outer reading in the restrictive variety (primaryPolarity_of_mem_negations_restrictive), where it is answered like a neutral question (answer_of_mem_negations_restrictive), and also the inner one in the tolerant variety (exists_mem_negations_tolerant_primaryPolarity, exists_mem_negations_tolerant). The mechanism predicts the judgment of every example answered by a single particle of the study, whose question is neutral or whose negation the annotation locates (judgment_iff_predicted).

Implementation notes

• An answer is computed as a polarity relative to the question's positive alternative (AnswerFeature.answer); the alternative it confirms is that polarity acting on the positive alternative. For Har Johan nångång inte kommit i tid? the positive alternative is that Johan has always been on time.
• Section 4.7 revises the height criterion: what matters is whether the negation can value the polarity head (ClauseNegation.ValuesHead), which is how Thai questions come out truth-based. Thai and the Chinese question types (Section 4.9) are not formalized, nor are verb-echo answers and the structure of Finnish and Thai answers (Chapter 3), the two versions of no of Section 4.4, the higher-order alternative of positive-bias questions (Section 4.8), the table of languages with a reversing affirmative particle, and the global survey of Section 4.2.
• The very formal English that does not use -n't at all, where a question with not must, as the book says presumably, carry the positive-bias reading as well, is not modelled: negations is stated for the varieties that use -n't.
• The book discusses French oui and si but not non, which french gives [−Pol], as the negative particle of every language the book discusses.

References

• [Hol16]
• [FB10]
• [Lad81]

The question variable

theorem Holmberg2016.smul_mem_alt {W : Type u_1} {q : PolarInterrogative W} (hne : q.radical ≠ ∅) (hnu : q.radical ≠ Set.univ) (s : Polarity) : s • q.radical ∈ (Semantics.Denotes.denote q).alt

An answer does not assert but chooses between the two alternatives of the question (Section 5.1): whatever polarity it gives the positive alternative yields one of them.

The particles

def Holmberg2016.english : English.PolarityParticle → AnswerFeature

The features of the English particles.

Equations

• Holmberg2016.english English.PolarityParticle.yes = AnswerFeature.value Polarity.positive
• Holmberg2016.english English.PolarityParticle.no = AnswerFeature.value Polarity.negative

def Holmberg2016.swedish : Swedish.PolarityParticle → AnswerFeature

The features of the Swedish particles: jo is [+Pol, REV].

Equations

• Holmberg2016.swedish Swedish.PolarityParticle.ja = AnswerFeature.value Polarity.positive
• Holmberg2016.swedish Swedish.PolarityParticle.nej = AnswerFeature.value Polarity.negative
• Holmberg2016.swedish Swedish.PolarityParticle.jo = AnswerFeature.reversing

def Holmberg2016.french : French.PolarityParticle → AnswerFeature

The features of the French particles: si is [+Pol, REV].

Equations

• Holmberg2016.french French.PolarityParticle.oui = AnswerFeature.value Polarity.positive
• Holmberg2016.french French.PolarityParticle.non = AnswerFeature.value Polarity.negative
• Holmberg2016.french French.PolarityParticle.si = AnswerFeature.reversing

def Holmberg2016.japanese : Japanese.PolarityParticle → AnswerFeature

The features of the Japanese particles.

Equations

• Holmberg2016.japanese Japanese.PolarityParticle.un = AnswerFeature.value Polarity.positive
• Holmberg2016.japanese Japanese.PolarityParticle.uun = AnswerFeature.value Polarity.negative

English (Section 4.3)

theorem Holmberg2016.negative_neutralization : (english English.PolarityParticle.yes).answer (ClauseNegation.height NegationHeight.low) = some Polarity.negative ∧ (english English.PolarityParticle.no).answer (ClauseNegation.height NegationHeight.middle) = some Polarity.negative

Negative neutralization: speakers who read not low take yes to confirm that John is not coming, speakers who read it middle take no to, so the two answers mean the same.

theorem Holmberg2016.yes_ill_formed_middle : (english English.PolarityParticle.yes).answer (ClauseNegation.height NegationHeight.middle) = none

With the middle reading of not, bare yes is not a well-formed answer.

theorem Holmberg2016.no_double_negation : (english English.PolarityParticle.no).answer (ClauseNegation.height NegationHeight.low) = some Polarity.positive

With the low reading, no is grammatically a double negation confirming the positive alternative; since bare no is parsed as the simpler plain negation, the continuation of No, he is is compulsory.

The polarity-based system (Section 4.4)

def Holmberg2016.PolarityBased (N : Finset NegationHeight) : Prop

The polarity-based system, defined in Section 4.4 as the system which lacks low negation: a language whose negations take the heights N.

Equations

• Holmberg2016.PolarityBased N = (NegationHeight.low ∉ N)

@[instance_reducible]

instance Holmberg2016.instDecidablePolarityBased (N : Finset NegationHeight) : Decidable (PolarityBased N)

Equations

• Holmberg2016.instDecidablePolarityBased N = { decide := !decide (NegationHeight.low ∈ N), reflects_decide := ⋯ }

theorem Holmberg2016.polarityBased_iff_not_confirmsNegativeQuestion {N : Finset NegationHeight} : PolarityBased N ↔ ¬Discourse.Response.ConfirmsNegativeQuestion ((AnswerFeature.value Polarity.positive).responses (ClauseNegation.height '' ↑N))

The definition is the typology's: a language lacks low negation iff its affirmative particle confirms the negative alternative of none of its negative questions.

theorem Holmberg2016.PolarityBased.answer_ne_negative {N : Finset NegationHeight} (hN : PolarityBased N) {h : NegationHeight} (hh : h ∈ N) : (AnswerFeature.value Polarity.positive).answer (ClauseNegation.height h) ≠ some Polarity.negative

A polarity-based language has no negative neutralization: no affirmative feature confirms the negative alternative of a negative question, unless an adverb screens the negation.

Swedish (Section 4.5) and the reversing particles

def Holmberg2016.swedishNegation : Finset NegationHeight

The heights of Swedish negation: middle, and high in positive-bias questions (Section 4.8). Swedish has no low negation, hence no double negation Du kan inte inte gå i kyrkan (Section 4.5).

Equations

• Holmberg2016.swedishNegation = {NegationHeight.middle, NegationHeight.high}

theorem Holmberg2016.swedish_polarityBased : PolarityBased swedishNegation

theorem Holmberg2016.swedish_ja_ne_negative {h : NegationHeight} (hh : h ∈ swedishNegation) : (swedish Swedish.PolarityParticle.ja).answer (ClauseNegation.height h) ≠ some Polarity.negative

Ja never confirms the negative alternative of a Swedish negative question.

theorem Holmberg2016.swedish_negative_question : (swedish Swedish.PolarityParticle.ja).answer (ClauseNegation.height NegationHeight.middle) = none ∧ (swedish Swedish.PolarityParticle.nej).answer (ClauseNegation.height NegationHeight.middle) = some Polarity.negative ∧ (swedish Swedish.PolarityParticle.jo).answer (ClauseNegation.height NegationHeight.middle) = some Polarity.positive

To Har Johan inte kommit? the plain affirmative ja is ill formed, nej confirms that he has not come, and the reversing jo confirms that he has.

theorem Holmberg2016.swedish_adverb : (swedish Swedish.PolarityParticle.ja).answer ClauseNegation.screened = some Polarity.negative ∧ (swedish Swedish.PolarityParticle.nej).answer ClauseNegation.screened = some Polarity.positive

Har Johan nångång inte kommit i tid?: the adverb intervening between the negation and the polarity head lets ja confirm the negative alternative, although Swedish has no low negation.

theorem Holmberg2016.french_negative_question : (french French.PolarityParticle.oui).answer (ClauseNegation.height NegationHeight.middle) = none ∧ (french French.PolarityParticle.si).answer (ClauseNegation.height NegationHeight.middle) = some Polarity.positive

To Tu n'es pas fatigué? the plain affirmative oui is ill formed and the reversing si confirms the positive alternative.

theorem Holmberg2016.responses_reversing_eq_reversePositive {N : Set ClauseNegation} (hN : ∃ n ∈ N, n.InClause) : AnswerFeature.reversing.responses N = FarkasBruce2010.reversePositive ∩ {x : Discourse.Response | x.reactsTo = Discourse.InitiatingMove.polarQuestion}

REV, credited to [FB10], is what they say si and doch mark: to questions whose negations include one inside the inherited clause, a reversing feature such as that of si or jo gives exactly the answers that are [reverse, +].

theorem Holmberg2016.no_reversal_needed_truth_based (f : AnswerFeature) : f.answer (ClauseNegation.height NegationHeight.low) ≠ none

Reversing particles are needed only where a negation values the polarity head: in a truth-based configuration every particle yields a well-formed answer, which is why no language with a reversing affirmative particle clearly employs the truth-based system.

Japanese (Section 4.1)

theorem Holmberg2016.japanese_negative_question : (japanese Japanese.PolarityParticle.un).answer (ClauseNegation.height NegationHeight.low) = some Polarity.negative ∧ (japanese Japanese.PolarityParticle.uun).answer (ClauseNegation.height NegationHeight.low) = some Polarity.positive

On the prediction of Section 4.10 that the Japanese negation in a negative-bias question does not value the polarity head, being low, un confirms that he does not drink coffee and uun that he does.

Positive-bias questions (Section 4.8)

theorem Holmberg2016.high_answers_like_neutral (f : AnswerFeature) : f.answer (ClauseNegation.height NegationHeight.high) = f.answer ClauseNegation.absent

A positive-bias negative question, with the negation in the C-domain above the polarity head, is answered like a neutral question.

Negative question forms in English

inductive Holmberg2016.EnglishVariety : Type

The two varieties of English the book distinguishes by negative questions with -n't: in the restrictive one such a question conveys only an expected positive answer; in the tolerant one it can also convey an expected negative answer, and then licenses either ([Lad81]).

• restrictive : EnglishVariety
• tolerant : EnglishVariety

@[instance_reducible]

instance Holmberg2016.instDecidableEqEnglishVariety : DecidableEq EnglishVariety

Equations

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

def Holmberg2016.instReprEnglishVariety.repr : EnglishVariety → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Holmberg2016.instReprEnglishVariety : Repr EnglishVariety

Equations

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

def Holmberg2016.negations : EnglishVariety → Option NegationPosition → Set ClauseNegation

The negations an English polar question with its negation in a given position can carry in a variety: none for the positive question; for non-preposed not a low or a middle negation, as speakers differ; for preposed -n't the high negation of the positive-bias reading and, in the tolerant variety, a negation inside the clause, at a height the book does not fix.

Equations

• One or more equations did not get rendered due to their size.
• Holmberg2016.negations x✝ none = {ClauseNegation.absent}
• Holmberg2016.negations x✝ (some NegationPosition.nonPreposed) = {ClauseNegation.height NegationHeight.low, ClauseNegation.height NegationHeight.middle}
• Holmberg2016.negations Holmberg2016.EnglishVariety.restrictive (some NegationPosition.preposed) = {ClauseNegation.height NegationHeight.high}

theorem Holmberg2016.primaryPolarity_of_mem_negations_nonPreposed {v : EnglishVariety} {n : ClauseNegation} (hn : n ∈ negations v (some NegationPosition.nonPreposed)) : n.primaryPolarity = Polarity.negative

A question with not makes the negative alternative primary for all speakers: it has the inner reading, conveying an expected negative answer.

theorem Holmberg2016.primaryPolarity_of_mem_negations_restrictive {n : ClauseNegation} (hn : n ∈ negations EnglishVariety.restrictive (some NegationPosition.preposed)) : n.primaryPolarity = Polarity.positive

In the restrictive variety a question with -n't has only the outer reading.

theorem Holmberg2016.exists_mem_negations_tolerant_primaryPolarity : ∃ n ∈ negations EnglishVariety.tolerant (some NegationPosition.preposed), n.primaryPolarity = Polarity.negative

In the tolerant variety it also has the inner reading.

theorem Holmberg2016.answer_of_mem_negations_restrictive {n : ClauseNegation} (hn : n ∈ negations EnglishVariety.restrictive (some NegationPosition.preposed)) (f : AnswerFeature) : f.answer n = f.answer ClauseNegation.absent

In the restrictive variety a question with -n't is answered like its positive counterpart, whatever the particle.

theorem Holmberg2016.exists_mem_negations_tolerant : ∃ n ∈ negations EnglishVariety.tolerant (some NegationPosition.preposed), (english English.PolarityParticle.yes).answer n ≠ (english English.PolarityParticle.yes).answer ClauseNegation.absent

In the tolerant variety it need not be: on a reading with the negation inside the clause, a bare yes does not answer it as it answers the positive question.

The examples

def Holmberg2016.featureTable : List (String × List (String × AnswerFeature))

The features of each language's particles, by Glottocode and spelling.

Equations

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

def Holmberg2016.negationTable : List (String × ClauseNegation)

The negation of a question, by where the annotation locates it.

Equations

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

def Holmberg2016.polarityTable : List (String × Polarity)

The alternatives an example confirms, as polarities relative to the positive alternative.

Equations

• Holmberg2016.polarityTable = [("p", Polarity.positive), ("not p", Polarity.negative)]

structure Holmberg2016.Row : Type

An example of a single particle answering a question whose negation the example fixes.

• negation : ClauseNegation

  The negation of the question.

• feature : AnswerFeature

  The feature of the answer.

• target : Option Polarity

  The alternative the answer confirms or is intended to confirm, if the example says.

• judgment : Judgment

  The judgment of the answer.

def Holmberg2016.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Holmberg2016.instDecidableEqRow : DecidableEq Row

Equations

• Holmberg2016.instDecidableEqRow = Holmberg2016.instDecidableEqRow.decEq

@[instance_reducible]

instance Holmberg2016.instReprRow : Repr Row

Equations

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

def Holmberg2016.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def Holmberg2016.Row.ofDatum (ex : Datum) : Option Row

The row of an example: its question is neutral or its negation located, and its answer is a single particle of one of the four languages.

Equations

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

def Holmberg2016.rows : List Row

The rows of the examples.

Equations

• Holmberg2016.rows = List.filterMap Holmberg2016.Row.ofDatum Holmberg2016.Examples.all

def Holmberg2016.Row.Predicted (r : Row) : Prop

The answer is well formed and confirms the alternative the example targets, if any.

Equations

• r.Predicted = (r.feature.answer r.negation ≠ none ∧ (r.target = none ∨ r.feature.answer r.negation = r.target))

@[instance_reducible]

instance Holmberg2016.instDecidablePredRowPredicted : DecidablePred Row.Predicted

Equations

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

theorem Holmberg2016.kommit_mem_rows : { negation := ClauseNegation.height NegationHeight.middle, feature := swedish Swedish.PolarityParticle.ja, target := none, judgment := Judgment.ungrammatical } ∈ rows ∧ { negation := ClauseNegation.height NegationHeight.middle, feature := swedish Swedish.PolarityParticle.jo, target := some Polarity.positive, judgment := Judgment.acceptable } ∈ rows

The rows include Har Johan inte kommit? answered by *Ja and by Jo (Section 4.5).

theorem Holmberg2016.judgment_iff_predicted (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ r.Predicted)

The mechanism predicts the judgment of every example answered by a single particle of the study, whose question is neutral or whose negation the annotation locates: the example is acceptable just when the answer is well formed and confirms the alternative it targets.