Polar interrogatives and their answers

This file formalizes the syntax of yes–no questions and their answers of [Hol16]. A PolarInterrogative is a sentence radical, its positive alternative, with a ClauseNegation, the negation of the clause, if any, with its height relative to the polarity head. Its primary alternative is the radical under the polarity the negation gives it, and it denotes the polar question of that alternative; a negative interrogative and its positive counterpart denote the same question, differing only in which alternative is primary (PolarInterrogative.denote_eq_polar_radical), whose alternatives are the polarity alternatives of the radical (PolarInterrogative.alt_denote).

The polarity head is merged unvalued, and a short answer merges a focused valued polarity feature, spelled out by an answer particle, with the clause inherited from the question, normally elided. An AnswerFeature is that feature: a valued [+Pol] or [−Pol], or the affirmative [+Pol, REV] of a polarity-reversing particle such as Swedish jo, which eliminates the negation in the answer. Given the negation of the clause the answer inherits, AnswerFeature.answer computes the polarity of the alternative the answer confirms, relative to the question's positive alternative, or none for an ill-formed answer; the action of Polarity on propositions turns that polarity into the alternative itself.

A negation out of the polarity head's reach, such as a low, VP-internal one, leaves the particle to value the head, and the value composes with the negation: an affirmative particle confirms the negative alternative, a negative one is a double negation. A middle negation values the head itself: a negative particle agrees with it and a plain affirmative clashes with it.

The answers a feature gives to the questions whose negations a language allows form a set of Discourse.Responses (AnswerFeature.responses), the carrier of the polarity features of [FB10], to whom [Hol16] credits REV: a reversing feature gives exactly the [reverse, +] answers (AnswerFeature.responses_reversing). The systems for answering negative questions are properties of these sets (Discourse.Response.ConfirmsNegativeQuestion), and the mechanism derives them from the height of the negation: the affirmative feature confirms the negative alternative just when the negation is low, the truth-based system (AnswerFeature.confirmsNegativeQuestion_responses_positive_iff), and the negative feature just when it is middle, the polarity-based system (AnswerFeature.confirmsNegativeQuestion_responses_negative_iff); after a high negation neither does, the question being answered like a neutral one.

Implementation notes

• What decides the system is whether the negation can value the polarity head (ClauseNegation.ValuesHead); the height of the negation matters only through that ([Hol16] on Thai, whose negation cannot value the head from inside the complement of the question particle). Heights classify constructions, not languages: English not is read low by some speakers and middle by others, and -n't in positive-bias questions is high.
• REV needs a negation in the answer to eliminate, so a reversing particle is ill formed after a neutral or a positive-bias question. Colloquial Swedish, where jo can confirm the positive alternative of any yes–no question ([Hol16], footnote to the section on positive and negative bias), is not modelled.
• The two versions of the negative particle in polarity-based languages, an interpretable one valuing the head and an uninterpretable one agreeing with a negation that values it, are one AnswerFeature.value .negative, whose agreement is built into AnswerFeature.answer.
• The reading of a polar interrogative is an Option Polarity: none for a positive question, and for a negative one the polarity of the proposition it double-checks, relative to its radical: [Lad81]'s outer reading, double-checking p, is some .positive, and his inner reading, double-checking ¬p, is some .negative. Each analysis computes it from its own structure; here it is the primary polarity of the clause's negation (ClauseNegation.primaryPolarity), negative for a negation inside the clause and positive for a high one ([Hol16]).
• Readings and forms (NegationPosition) are related, not identified: the preposed -n't of Isn't this the road to Lund? has both readings for some speakers of English, so each language or variety relates a form to a set of readings.

References

• [Hol16]
• [FB10]
• [Lad81]
• [RH04]
• [Rom24]

inductive AnswerFeature : Type

The feature an answer particle spells out ([Hol16]): a valued polarity feature, or the affirmative polarity-reversing feature of jo, [jo, +Pol, REV].

• value (p : Polarity) : AnswerFeature

  A valued polarity feature, [+Pol] or [−Pol].

• reversing : AnswerFeature

  [+Pol, REV]: positive polarity eliminating a negation in the answer.

@[instance_reducible]

instance instDecidableEqAnswerFeature : DecidableEq AnswerFeature

Equations

• instDecidableEqAnswerFeature = instDecidableEqAnswerFeature.decEq

def instDecidableEqAnswerFeature.decEq (x✝ x✝¹ : AnswerFeature) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqAnswerFeature.decEq (AnswerFeature.value a) (AnswerFeature.value b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqAnswerFeature.decEq (AnswerFeature.value p) AnswerFeature.reversing = isFalse ⋯
• instDecidableEqAnswerFeature.decEq AnswerFeature.reversing (AnswerFeature.value p) = isFalse ⋯
• instDecidableEqAnswerFeature.decEq AnswerFeature.reversing AnswerFeature.reversing = isTrue ⋯

@[instance_reducible]

instance instReprAnswerFeature : Repr AnswerFeature

Equations

• instReprAnswerFeature = { reprPrec := instReprAnswerFeature.repr }

def instReprAnswerFeature.repr : AnswerFeature → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprAnswerFeature.repr AnswerFeature.reversing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AnswerFeature.reversing")).group prec✝

inductive NegationHeight : Type

Structural height of a sentential negation relative to the polarity head. The height classifies constructions, not languages: English not is read low by some speakers and middle by others, and low by all after an adverb; -n't in positive-bias questions is high.

• low : NegationHeight

  Negation below the reach of the polarity head, VP-internal (English not on its low reading).

• middle : NegationHeight

  Negation in a local c-command relation to the polarity head (Swedish, Finnish, English not on its middle reading).

• high : NegationHeight

  Negation above the polarity head, in the C-domain (English -n't in positive-bias questions).

@[instance_reducible]

instance instDecidableEqNegationHeight : DecidableEq NegationHeight

Equations

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

def instReprNegationHeight.repr : NegationHeight → ℕ → Std.Format

Equations

• instReprNegationHeight.repr NegationHeight.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NegationHeight.low")).group prec✝
• instReprNegationHeight.repr NegationHeight.middle prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NegationHeight.middle")).group prec✝
• instReprNegationHeight.repr NegationHeight.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NegationHeight.high")).group prec✝

@[instance_reducible]

instance instReprNegationHeight : Repr NegationHeight

Equations

• instReprNegationHeight = { reprPrec := instReprNegationHeight.repr }

@[instance_reducible]

instance instFintypeNegationHeight : Fintype NegationHeight

Equations

• instFintypeNegationHeight = { elems := { val := ↑NegationHeight.enumList, nodup := NegationHeight.enumList_nodup }, complete := instFintypeNegationHeight._proof_1 }

inductive NegationPosition : Type

The position of the negation of a negative polar interrogative relative to the rest of the clause ([RH04]): preposed with the finite verb, as English n't in Isn't Jane coming?, or not, as not in Is Jane not coming?. What matters is the relative position, not a particular one. The form of a polar interrogative is an Option NegationPosition, none for a positive question: [Rom24]'s PosQ, LoNQ and HiNQ.

• preposed : NegationPosition

  Negation preposed with the finite verb.

• nonPreposed : NegationPosition

  Negation in its clause-internal position.

@[instance_reducible]

instance instDecidableEqNegationPosition : DecidableEq NegationPosition

Equations

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

@[instance_reducible]

instance instReprNegationPosition : Repr NegationPosition

Equations

• instReprNegationPosition = { reprPrec := instReprNegationPosition.repr }

def instReprNegationPosition.repr : NegationPosition → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprNegationPosition.repr NegationPosition.preposed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NegationPosition.preposed")).group prec✝

@[instance_reducible]

instance instFintypeNegationPosition : Fintype NegationPosition

Equations

• instFintypeNegationPosition = { elems := { val := ↑NegationPosition.enumList, nodup := NegationPosition.enumList_nodup }, complete := instFintypeNegationPosition._proof_1 }

inductive ClauseNegation : Type

The negation of a clause relative to its polarity head, if any. An answer inherits the negation of the clause it answers.

• absent : ClauseNegation

  No negation: a neutral question or a positive statement.

• height (h : NegationHeight) : ClauseNegation

  A negation of the given height, nothing intervening between it and the polarity head.

• screened : ClauseNegation

  A middle negation screened from the polarity head by an adverb scoping over it, as in Swedish Har Johan nångång inte kommit i tid?.

@[instance_reducible]

instance instDecidableEqClauseNegation : DecidableEq ClauseNegation

Equations

• instDecidableEqClauseNegation = instDecidableEqClauseNegation.decEq

def instDecidableEqClauseNegation.decEq (x✝ x✝¹ : ClauseNegation) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqClauseNegation.decEq ClauseNegation.absent ClauseNegation.absent = isTrue ⋯
• instDecidableEqClauseNegation.decEq ClauseNegation.absent (ClauseNegation.height h) = isFalse ⋯
• instDecidableEqClauseNegation.decEq ClauseNegation.absent ClauseNegation.screened = isFalse instDecidableEqClauseNegation.decEq._proof_4
• instDecidableEqClauseNegation.decEq (ClauseNegation.height h) ClauseNegation.absent = isFalse ⋯
• instDecidableEqClauseNegation.decEq (ClauseNegation.height a) (ClauseNegation.height b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqClauseNegation.decEq (ClauseNegation.height h) ClauseNegation.screened = isFalse ⋯
• instDecidableEqClauseNegation.decEq ClauseNegation.screened ClauseNegation.absent = isFalse instDecidableEqClauseNegation.decEq._proof_8
• instDecidableEqClauseNegation.decEq ClauseNegation.screened (ClauseNegation.height h) = isFalse ⋯
• instDecidableEqClauseNegation.decEq ClauseNegation.screened ClauseNegation.screened = isTrue ⋯

def instReprClauseNegation.repr : ClauseNegation → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprClauseNegation.repr ClauseNegation.absent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ClauseNegation.absent")).group prec✝
• instReprClauseNegation.repr ClauseNegation.screened prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ClauseNegation.screened")).group prec✝

@[instance_reducible]

instance instReprClauseNegation : Repr ClauseNegation

Equations

• instReprClauseNegation = { reprPrec := instReprClauseNegation.repr }

@[instance_reducible]

instance instFintypeClauseNegation : Fintype ClauseNegation

Equations

• instFintypeClauseNegation = Fintype.ofEquiv (Unit ⊕ NegationHeight ⊕ Unit) ClauseNegation.proxyTypeEquiv

def ClauseNegation.InClause (n : ClauseNegation) : Prop

The negation is inside the clause the answer inherits, so that both alternatives of the question contain it: a low or middle negation.

Equations

• n.InClause = (n = ClauseNegation.height NegationHeight.low ∨ n = ClauseNegation.height NegationHeight.middle ∨ n = ClauseNegation.screened)

@[instance_reducible]

instance ClauseNegation.instDecidableInClause (n : ClauseNegation) : Decidable n.InClause

Equations

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

def ClauseNegation.primaryPolarity (n : ClauseNegation) : Polarity

The polarity of the question's primary alternative relative to its positive alternative: negative when the negation is inside the inherited clause.

Equations

• n.primaryPolarity = if n.InClause then Polarity.negative else Polarity.positive

def ClauseNegation.ValuesHead (n : ClauseNegation) : Prop

The negation values the polarity head: a middle negation not screened off by an adverb.

Equations

• n.ValuesHead = (n = ClauseNegation.height NegationHeight.middle)

@[instance_reducible]

instance ClauseNegation.instDecidableValuesHead (n : ClauseNegation) : Decidable n.ValuesHead

Equations

• n.instDecidableValuesHead = ClauseNegation.instDecidableValuesHead._aux_1 n

theorem ClauseNegation.primaryPolarity_of_inClause {n : ClauseNegation} (h : n.InClause) : n.primaryPolarity = Polarity.negative

structure PolarInterrogative (W : Type u_1) : Type u_1

A polar interrogative: its sentence radical, the positive alternative, and its negation.

• radical : Set W

  The sentence radical, the positive alternative.

• negation : ClauseNegation

  The negation of the interrogative.

def PolarInterrogative.primary {W : Type u_1} (q : PolarInterrogative W) : Set W

The primary alternative: the radical under the polarity its negation gives it, negative when the negation is inside the clause.

Equations

• q.primary = q.negation.primaryPolarity • q.radical

@[instance_reducible]

instance PolarInterrogative.instDenotesQuestion {W : Type u_1} : Semantics.Denotes (PolarInterrogative W) (Question W)

A polar interrogative denotes the polar question of its primary alternative, the disjunction of that alternative and its negation.

Equations

• PolarInterrogative.instDenotesQuestion = { denote := fun (q : PolarInterrogative W) => Question.polar q.primary }

theorem PolarInterrogative.denote_def {W : Type u_1} (q : PolarInterrogative W) : Semantics.Denotes.denote q = Question.polar q.primary

@[simp]

theorem PolarInterrogative.denote_eq_polar_radical {W : Type u_1} (q : PolarInterrogative W) : Semantics.Denotes.denote q = Question.polar q.radical

A negative interrogative denotes the same question as its positive counterpart: the negation decides which alternative is primary, not what the alternatives are.

theorem PolarInterrogative.alt_denote {W : Type u_1} {q : PolarInterrogative W} (hne : q.radical ≠ ∅) (hnu : q.radical ≠ Set.univ) : (Semantics.Denotes.denote q).alt = MulAction.orbit Polarity q.radical

The alternatives of a polar interrogative with a nontrivial radical are the values of its polarity variable applied to the radical, its polarity alternatives.

def AnswerFeature.answer : AnswerFeature → ClauseNegation → Option Polarity

The polarity of the alternative an answer confirms, relative to the positive alternative, or none when the answer is ill formed. A reversing feature eliminates the negation inside the inherited clause and values the head, and is ill formed without one. Otherwise, if the negation values the head, a negative feature agrees with it and an affirmative one clashes with it; if not, the feature values the head, composing with a negation inside the clause.

Equations

• AnswerFeature.reversing.answer x✝ = if x✝.InClause then some Polarity.positive else none
• (AnswerFeature.value p).answer x✝ = if x✝.ValuesHead then if p = Polarity.negative then some Polarity.negative else none else some (p * x✝.primaryPolarity)

theorem AnswerFeature.answer_reversing_of_inClause {n : ClauseNegation} (h : n.InClause) : reversing.answer n = some Polarity.positive

A reversing feature eliminates the negation inside the clause and values the head.

theorem AnswerFeature.answer_reversing_of_not_inClause {n : ClauseNegation} (h : ¬n.InClause) : reversing.answer n = none

A reversing feature has no negation to eliminate outside a negative-bias question.

theorem AnswerFeature.answer_value_of_valuesHead {n : ClauseNegation} {p : Polarity} (h : n.ValuesHead) : (value p).answer n = if p = Polarity.negative then some Polarity.negative else none

A negation valuing the head: a negative feature agrees with it, confirming the negative alternative, and an affirmative one clashes with it.

theorem AnswerFeature.answer_value_of_not_valuesHead {n : ClauseNegation} {p : Polarity} (h : ¬n.ValuesHead) : (value p).answer n = some (p * n.primaryPolarity)

Without a negation valuing the head, a valued feature values it and composes with the polarity of the primary alternative.

theorem AnswerFeature.answer_ne_none_of_inClause {n : ClauseNegation} (f : AnswerFeature) (hi : n.InClause) (h : ¬n.ValuesHead) : f.answer n ≠ none

A negation inside the clause that does not value the head admits every feature, so a truth-based configuration has no need of a reversing particle.

def AnswerFeature.responses (f : AnswerFeature) (N : Set ClauseNegation) : Set Discourse.Response

The answers a feature gives to polar questions whose negations are among N: the polarity of a question's primary alternative, and that of the alternative the answer confirms.

Equations

• f.responses N = {x : Discourse.Response | x.reactsTo = Discourse.InitiatingMove.polarQuestion ∧ ∃ n ∈ N, n.primaryPolarity = x.antecedent ∧ f.answer n = some x.polarity}

theorem AnswerFeature.responses_reversing {N : Set ClauseNegation} (hN : ∃ n ∈ N, n.InClause) : reversing.responses N = {x : Discourse.Response | x.reactsTo = Discourse.InitiatingMove.polarQuestion ∧ x.relative = Polarity.negative ∧ x.polarity = Polarity.positive}

REV is [reverse, +] ([FB10]): once some negation of N is inside the clause, a reversing feature gives exactly the positive answers reversing the primary alternative.

theorem AnswerFeature.confirmsNegativeQuestion_responses_iff {f : AnswerFeature} {N : Set ClauseNegation} : Discourse.Response.ConfirmsNegativeQuestion (f.responses N) ↔ ∃ n ∈ N, n.InClause ∧ f.answer n = some Polarity.negative

The answers of a feature to questions whose negations are among N confirm the negative alternative of a negative question iff some negation of N inside the clause yields it.

theorem AnswerFeature.confirmsNegativeQuestion_responses_positive_iff (h : NegationHeight) : Discourse.Response.ConfirmsNegativeQuestion ((value Polarity.positive).responses {ClauseNegation.height h}) ↔ h = NegationHeight.low

The truth-based system: the affirmative feature confirms the negative alternative of a question whose negation has height h iff the negation is low, out of the polarity head's reach.

theorem AnswerFeature.confirmsNegativeQuestion_responses_negative_iff (h : NegationHeight) : Discourse.Response.ConfirmsNegativeQuestion ((value Polarity.negative).responses {ClauseNegation.height h}) ↔ h = NegationHeight.middle

The polarity-based system: the negative feature confirms the negative alternative of a question whose negation has height h iff the negation is middle, valuing the polarity head.