Wilder (2013): English emphatic do

On Wilder's analysis the auxiliary do appears wherever Affix Hopping cannot attach Tense to the verb, and emphatic assertion is one such case: the polarity head Σ of Laka holding the affirmative morpheme intervenes between Tense and the verb just as negation does, so emphatic do has the syntax of do-support under negation. The emphasis itself is focus on Σ, polarity focus, whose alternatives are the proposition and its negation, the alternatives of the polar question the sentence answers. Under Schwarzschild's Givenness the existential F-closure of a clause with F-marked Σ is a tautology, so any salient antecedent makes the clause Given, and the requirement that the antecedent be a negated or modalised version of the proposition falls on the unfocused subject and verb phrase instead. Emphatic do sentences come in two types. A Verum-focus sentence has no accent beyond focus accents and occurs in every finite clause type. A contrastive-topic sentence has, on its subject, verb phrase or object, the fall-rise accent that Büring analyses as indicating a strategy of questions, and it occurs only as a root declarative or a complement of the believe type. Wilder derives the restriction from the hypothesis that a contrastive-topic sentence with emphatic do directly answers a polar question of the strategy: such an answer can be embedded under believe or appear, but not as an interrogative or factive complement, a cleft, a relative or an adverbial clause, and a contrastive-topic sentence that answers a constituent question rejects do altogether.

Main definitions

• Clause, AffixHopping, DoSupport, EmphaticDo: the auxiliary system of section 2.
• polarityFocus: an F-marked Σ applied to the proposition, with its polarity alternatives.
• existentialClosure, Given: Schwarzschild's existential F-closure and Givenness.
• DirectlyAnswersPolar: the hypothesis (112) on the strategy a contrastive topic indicates.
• Row, rows: the paper's judgments on the two sentence types across clause types.

Main results

• emphaticDo_iff: emphatic do is do-support forced by an affirmative Σ alone.
• doSupport_negative_iff_positive: negation and emphatic assertion strand Tense alike.
• polarityFocus_alternatives_eq_alt_polar: the alternatives of polarity focus are those of the polar question.
• given_polarityFocus: a clause with F-marked Σ is Given after any antecedent.
• not_admits_polarityFocus_of_constituentQuestion: a constituent question does not admit polarity focus, so a contrastive-topic sentence answering one rejects do.
• doctorStrategy_isComplete: the strategy a contrastive-topic verb phrase indicates is complete when its subquestions decide the superquestion.
• ct_acceptable_iff_hostsYesAnswer: across the embedding environments, a contrastive-topic sentence with emphatic do is acceptable exactly where a Yes-answer can be embedded.

Implementation notes

• Clause keeps only the heads of the clause structure (3) that decide Affix Hopping; an auxiliary in T stands for have, be or a modal, and Σ carries its polarity and whether it is F-marked. Wilder's claim that unfocused emphatic do is unacceptable rather than ungrammatical is not encoded.
• The contrastive-topic accent is recorded as a feature of an example row, not composed; the strategy it indicates is a Discourse.Strategy, and the hypothesis (112) is membership of the polar question among its nodes.
• The Yes-answer environments of (126) and (127) are rows like the emphatic do judgments, so ct_acceptable_iff_hostsYesAnswer compares two tables the paper gives independently. The wh-subject question and object preposing rows are outside that comparison: the paper explains them by the incompatibility of contrastive topic with questions and by a clash of strategies.

TODO

• The optionality of do in contrastive-topic sentences (section 7) and the Givenness of the subject and verb phrase under composition (section 4.2) are not formalized; the latter is what the antecedents of section 4.1, an asserted, presupposed or modalised negation and the negation of a parallel predication, constrain.

References

• [Wil13]
• [Lak90]
• [Sch99b]
• [Bur03]
• [Hoh92]
• [Rob12]

The auxiliary system

structure Wilder2013.Clause : Type

These heads of the clause structure (3) decide whether Tense reaches the verb, namely an auxiliary raising to T (have, be) or a modal in T, the polarity head Σ with its value and whether it is F-marked, subject–auxiliary inversion, and an empty verb (ellipsis or VP fronting).

• aux : Bool
• sigma : Option (Polarity × Focus.Mark)
• inversion : Bool
• emptyV : Bool

@[instance_reducible]

instance Wilder2013.instDecidableEqClause : DecidableEq Clause

Equations

• Wilder2013.instDecidableEqClause = Wilder2013.instDecidableEqClause.decEq

def Wilder2013.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

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

def Wilder2013.AffixHopping (c : Clause) : Prop

Affix Hopping attaches a stranded Tense affix to the adjacent overt verb when no Σ intervenes, the subject has not intervened by inversion, and the verb is overt.

Equations

• Wilder2013.AffixHopping c = (c.sigma = none ∧ ¬c.inversion = true ∧ ¬c.emptyV = true)

def Wilder2013.DoSupport (c : Clause) : Prop

Do-support arises when no auxiliary satisfies Tense and Affix Hopping is blocked.

Equations

• Wilder2013.DoSupport c = (¬c.aux = true ∧ ¬Wilder2013.AffixHopping c)

def Wilder2013.PolarityFocus (c : Clause) : Prop

A clause has polarity focus when Σ is present and F-marked.

Equations

• Wilder2013.PolarityFocus c = ∃ (s : Polarity), c.sigma = some (s, Focus.Mark.focused)

def Wilder2013.EmphaticDo (c : Clause) : Prop

Emphatic do is do-support motivated by none of the contexts of (1), negation, inversion or an empty verb.

Equations

• Wilder2013.EmphaticDo c = (Wilder2013.DoSupport c ∧ (∀ (f : Focus.Mark), c.sigma ≠ some (Polarity.negative, f)) ∧ ¬c.inversion = true ∧ ¬c.emptyV = true)

theorem Wilder2013.doSupport_iff (c : Clause) : DoSupport c ↔ ¬c.aux = true ∧ (c.sigma ≠ none ∨ c.inversion = true ∨ c.emptyV = true)

By (4), do-support arises exactly when Σ intervenes, the subject intervenes, or the verb is empty, and no auxiliary hosts Tense.

theorem Wilder2013.emphaticDo_iff (c : Clause) : EmphaticDo c ↔ ¬c.aux = true ∧ ¬c.inversion = true ∧ ¬c.emptyV = true ∧ ∃ (f : Focus.Mark), c.sigma = some (Polarity.positive, f)

Emphatic do is do-support forced by an affirmative Σ alone, as in (4a-ii).

theorem Wilder2013.doSupport_negative_iff_positive (c : Clause) (f f' : Focus.Mark) : DoSupport { aux := c.aux, sigma := some (Polarity.negative, f), inversion := c.inversion, emptyV := c.emptyV } ↔ DoSupport { aux := c.aux, sigma := some (Polarity.positive, f'), inversion := c.inversion, emptyV := c.emptyV }

The syntax of emphatic assertion is that of negation, since with Σ present do-support does not depend on the value of Σ.

theorem Wilder2013.not_doSupport_of_aux {c : Clause} (h : c.aux = true) : ¬DoSupport c

By (5), an auxiliary in T hosts Tense, so no do appears whatever Σ holds.

theorem Wilder2013.not_polarityFocus_of_affixHopping {c : Clause} (h : AffixHopping c) : ¬PolarityFocus c

A clause with Affix Hopping has no Σ and so no polarity focus.

theorem Wilder2013.emphaticDo_sigma {c : Clause} (h : EmphaticDo c) : ∃ (f : Focus.Mark), c.sigma = some (Polarity.positive, f)

Emphatic do is the sole auxiliary whose presence signals Σ, since an emphatic do clause has Σ, though its F-mark is syntactically optional.

Polarity focus and Givenness

def Wilder2013.polarityFocus {W : Type u_1} (p : Set W) : WithAlternatives (Set W)

Polarity focus is an affirmative Σ, F-marked, applied to the proposition of the clause, so that each value of Σ, affirmation and negation, applies to it (73).

Equations

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

@[simp]

theorem Wilder2013.polarityFocus_ordinary {W : Type u_1} (p : Set W) : (polarityFocus p).ordinary = p

theorem Wilder2013.polarityFocus_alternatives_eq_orbit {W : Type u_1} (p : Set W) : (polarityFocus p).alternatives = MulAction.orbit Polarity p

The alternatives of polarity focus are the orbit of the proposition under the polarity group, its polarity alternatives.

theorem Wilder2013.polarityFocus_alternatives {W : Type u_1} (p : Set W) : (polarityFocus p).alternatives = {p, pᶜ}

The alternatives of polarity focus are the proposition and its negation.

theorem Wilder2013.polarityFocus_wellFormed {W : Type u_1} (p : Set W) : (polarityFocus p).WellFormed

Polarity focus is well formed, since the proposition is among its alternatives.

theorem Wilder2013.polarityFocus_alternatives_eq_alt_polar {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : (polarityFocus p).alternatives = (Question.polar p).alt

The alternative set of an emphatic do sentence is the meaning of the polar question it answers (section 4.1).

theorem Wilder2013.question_admits_polarityFocus {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : (Focus.Antecedent.question (Question.polar p).alt).Admits (polarityFocus p).alternatives

By (59) and (60), a context that evokes the polar question admits the polarity focus of an answer to it.

theorem Wilder2013.assertion_neg_resolves_polarityFocus {W : Type u_1} {p : Set W} (hne : p ≠ ∅) : (Focus.Antecedent.assertion pᶜ {p, pᶜ}).Resolves (polarityFocus p).ordinary (polarityFocus p).alternatives

In (51) a prior assertion of the negation is corrected by the emphatic do sentence, which resolves the focus antecedent among the polarity alternatives.

theorem Wilder2013.not_assertion_self_resolves {W : Type u_1} (p : Set W) (alts : Set (Set W)) : ¬(Focus.Antecedent.assertion p alts).Resolves (polarityFocus p).ordinary (polarityFocus p).alternatives

In (57) an antecedent asserting the proposition itself is not a focus alternative that the sentence corrects; the alternative set is evoked by the context instead.

def Wilder2013.existentialClosure {W : Type u_1} (m : WithAlternatives (Set W)) : Set W

The existential F-closure (66) is the proposition that some alternative holds.

Equations

• Wilder2013.existentialClosure m = ⋃₀ m.alternatives

def Wilder2013.Given {W : Type u_1} (a : Set W) (m : WithAlternatives (Set W)) : Prop

Givenness (70) at the propositional level holds when a salient antecedent entails the existential F-closure.

Equations

• Wilder2013.Given a m = (a ⊆ Wilder2013.existentialClosure m)

theorem Wilder2013.existentialClosure_polarityFocus {W : Type u_1} (p : Set W) : existentialClosure (polarityFocus p) = Set.univ

By (73), the existential F-closure of a clause with F-marked Σ is a tautology.

theorem Wilder2013.given_polarityFocus {W : Type u_1} (a p : Set W) : Given a (polarityFocus p)

Any salient antecedent makes a clause with polarity focus Given, so the requirement that the antecedent be the negation falls on the unfocused subject and verb phrase, not on the clause.

theorem Wilder2013.exists_not_given {W : Type u_1} {m : WithAlternatives (Set W)} (h : existentialClosure m ≠ Set.univ) : ∃ (a : Set W), ¬Given a m

By (72), a narrow focus whose alternatives do not exhaust the worlds is not Given after every antecedent, so it constrains the antecedent as polarity focus does not.

Contrastive topic and strategies

def Wilder2013.DirectlyAnswersPolar {W : Type u_1} (s : Discourse.Strategy W) (p : Set W) : Prop

Under hypothesis (112), a sentence with a contrastive topic and emphatic do directly answers a polar question of the strategy the contrastive topic indicates, so the polar question is a node of the strategy.

Equations

• Wilder2013.DirectlyAnswersPolar s p = (Question.polar p ∈ RoseTree.values s)

def Wilder2013.doctorStrategy {W : Type u_1} (good patients diagnose polite : Set W) : Discourse.Strategy W

The strategy the contrastive-topic verb phrase of (106) and (107) indicates asks whether he is a good doctor, divided into whether he has a lot of patients, diagnoses well and treats his patients politely.

Equations

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

theorem Wilder2013.directlyAnswersPolar_doctorStrategy {W : Type u_1} (good patients diagnose polite : Set W) : DirectlyAnswersPolar (doctorStrategy good patients diagnose polite) patients

He DOES have a lot of patients directly answers a polar subquestion of the strategy.

theorem Wilder2013.doctorStrategy_isComplete {W : Type u_1} {good patients diagnose polite : Set W} (h : good = patients ∩ diagnose ∩ polite) : (doctorStrategy good patients diagnose polite).IsComplete

The strategy is complete when the three subquestions decide the superquestion, so that a state that settles each of them settles whether he is a good doctor.

theorem Wilder2013.not_good_of_not_diagnose {W : Type u_1} {good patients diagnose polite : Set W} (h : good = patients ∩ diagnose ∩ polite) {σ : Set W} (hσ : σ ⊆ diagnoseᶜ) : σ ⊆ goodᶜ

By (24), a negative answer to an unanswered subquestion is a negative answer to the superquestion.

theorem Wilder2013.not_admits_polarityFocus_of_constituentQuestion {W : Type u_1} {Q : Question W} {p a : Set W} (ha : a ∈ Q.alt) (hp : a ≠ p) (hc : a ≠ pᶜ) : ¬(Focus.Antecedent.question Q.alt).Admits (polarityFocus p).alternatives

By (113) and (114), a constituent question has an alternative that is neither the proposition nor its negation, so it does not admit the polarity focus of an emphatic do answer. A contrastive-topic sentence that directly answers a constituent question rejects do.

The two sentence types across clause types

inductive Wilder2013.Constituent : Type

The constituent bearing the contrastive-topic accent.

• subject : Constituent
• vp : Constituent
• object : Constituent

@[instance_reducible]

instance Wilder2013.instDecidableEqConstituent : DecidableEq Constituent

Equations

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

def Wilder2013.instReprConstituent.repr : Constituent → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Wilder2013.instReprConstituent : Repr Constituent

Equations

• Wilder2013.instReprConstituent = { reprPrec := Wilder2013.instReprConstituent.repr }

inductive Wilder2013.Kind : Type

A row judges one kind of sentence, the Verum-focus pattern (46), the contrastive-topic pattern (47) with its marked constituent, a contrastive-topic sentence directly answering a constituent question (113), (114), or a Yes-answer to a polar question (126), (127), (137).

• vf : Kind
• ct (k : Constituent) : Kind
• ctConstituentQuestion (k : Constituent) : Kind
• yesAnswer : Kind

def Wilder2013.instDecidableEqKind.decEq (x✝ x✝¹ : Kind) : Decidable (x✝ = x✝¹)

Equations

• Wilder2013.instDecidableEqKind.decEq Wilder2013.Kind.vf Wilder2013.Kind.vf = isTrue ⋯
• Wilder2013.instDecidableEqKind.decEq Wilder2013.Kind.vf (Wilder2013.Kind.ct k) = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq Wilder2013.Kind.vf (Wilder2013.Kind.ctConstituentQuestion k) = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq Wilder2013.Kind.vf Wilder2013.Kind.yesAnswer = isFalse Wilder2013.instDecidableEqKind.decEq._proof_5
• Wilder2013.instDecidableEqKind.decEq (Wilder2013.Kind.ct k) Wilder2013.Kind.vf = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq (Wilder2013.Kind.ct a) (Wilder2013.Kind.ct b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq (Wilder2013.Kind.ct k) (Wilder2013.Kind.ctConstituentQuestion k_1) = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq (Wilder2013.Kind.ct k) Wilder2013.Kind.yesAnswer = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq (Wilder2013.Kind.ctConstituentQuestion k) Wilder2013.Kind.vf = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq (Wilder2013.Kind.ctConstituentQuestion k) (Wilder2013.Kind.ct k_1) = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq (Wilder2013.Kind.ctConstituentQuestion a) (Wilder2013.Kind.ctConstituentQuestion b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq (Wilder2013.Kind.ctConstituentQuestion k) Wilder2013.Kind.yesAnswer = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq Wilder2013.Kind.yesAnswer Wilder2013.Kind.vf = isFalse Wilder2013.instDecidableEqKind.decEq._proof_14
• Wilder2013.instDecidableEqKind.decEq Wilder2013.Kind.yesAnswer (Wilder2013.Kind.ct k) = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq Wilder2013.Kind.yesAnswer (Wilder2013.Kind.ctConstituentQuestion k) = isFalse ⋯
• Wilder2013.instDecidableEqKind.decEq Wilder2013.Kind.yesAnswer Wilder2013.Kind.yesAnswer = isTrue ⋯

@[instance_reducible]

instance Wilder2013.instDecidableEqKind : DecidableEq Kind

Equations

• Wilder2013.instDecidableEqKind = Wilder2013.instDecidableEqKind.decEq

def Wilder2013.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Wilder2013.instReprKind : Repr Kind

Equations

• Wilder2013.instReprKind = { reprPrec := Wilder2013.instReprKind.repr }

def Wilder2013.Kind.IsCT : Kind → Prop

The contrastive-topic pattern (47).

Equations

• (Wilder2013.Kind.ct k).IsCT = True
• x✝.IsCT = False

@[instance_reducible]

instance Wilder2013.instDecidablePredKindIsCT : DecidablePred Kind.IsCT

Equations

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

def Wilder2013.Kind.IsCTConstituentQuestion : Kind → Prop

A contrastive-topic sentence directly answering a constituent question.

Equations

• (Wilder2013.Kind.ctConstituentQuestion k).IsCTConstituentQuestion = True
• x✝.IsCTConstituentQuestion = False

@[instance_reducible]

instance Wilder2013.instDecidablePredKindIsCTConstituentQuestion : DecidablePred Kind.IsCTConstituentQuestion

Equations

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

inductive Wilder2013.Environment : Type

The clause types of sections 3.5 and 3.6.

• root : Environment
• believeComplement : Environment
• interrogativeComplement : Environment
• factiveComplement : Environment
• itCleft : Environment
• restrictiveRelative : Environment
• adverbialClause : Environment
• whSubjectQuestion : Environment
• objectPreposing : Environment

@[instance_reducible]

instance Wilder2013.instDecidableEqEnvironment : DecidableEq Environment

Equations

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

@[instance_reducible]

instance Wilder2013.instReprEnvironment : Repr Environment

Equations

• Wilder2013.instReprEnvironment = { reprPrec := Wilder2013.instReprEnvironment.repr }

def Wilder2013.instReprEnvironment.repr : Environment → ℕ → Std.Format

Equations

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

structure Wilder2013.Row : Type

• kind : Kind
• environment : Environment
• acceptable : Bool

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

Equations

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

@[instance_reducible]

instance Wilder2013.instDecidableEqRow : DecidableEq Row

Equations

• Wilder2013.instDecidableEqRow = Wilder2013.instDecidableEqRow.decEq

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

Equations

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

@[instance_reducible]

instance Wilder2013.instReprRow : Repr Row

Equations

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

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

Equations

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

def Wilder2013.rows : List Row

Equations

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

theorem Wilder2013.rows_length : rows.length = Examples.all.length

Every example row parses.

def Wilder2013.Environment.IsEmbedding : Environment → Prop

The embedding environments of section 3.5, where the paper compares the two patterns.

Equations

• Wilder2013.Environment.whSubjectQuestion.IsEmbedding = False
• Wilder2013.Environment.objectPreposing.IsEmbedding = False
• x✝.IsEmbedding = True

@[instance_reducible]

instance Wilder2013.instDecidablePredEnvironmentIsEmbedding : DecidablePred Environment.IsEmbedding

Equations

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

def Wilder2013.HostsYesAnswer (e : Environment) : Prop

An environment hosts a Yes-answer to a polar question when the paper judges one acceptable in it, (126) and (137) against (127).

Equations

• Wilder2013.HostsYesAnswer e = ∃ r ∈ Wilder2013.rows, r.kind = Wilder2013.Kind.yesAnswer ∧ r.environment = e ∧ r.acceptable = true

@[instance_reducible]

instance Wilder2013.instDecidablePredEnvironmentHostsYesAnswer : DecidablePred HostsYesAnswer

Equations

• Wilder2013.instDecidablePredEnvironmentHostsYesAnswer x✝ = id inferInstance

theorem Wilder2013.vf_acceptable (r : Row) : r ∈ rows → r.kind = Kind.vf → r.acceptable = true

By (46c), the Verum-focus pattern is acceptable in every clause type.

theorem Wilder2013.ct_acceptable_iff_hostsYesAnswer (r : Row) : r ∈ rows → r.kind.IsCT → r.environment.IsEmbedding → (r.acceptable = true ↔ HostsYesAnswer r.environment)

Where (125) meets (127), across the embedding environments, a contrastive-topic sentence with emphatic do is acceptable exactly where a Yes-answer to a polar question can be embedded.

theorem Wilder2013.ct_not_whSubjectQuestion (r : Row) : r ∈ rows → r.kind.IsCT → r.environment = Environment.whSubjectQuestion → ¬r.acceptable = true

By Section 6.1, no contrastive-topic sentence occurs in a wh-subject question, since contrastive topic is undefined for questions.

theorem Wilder2013.ct_not_objectPreposing (r : Row) : r ∈ rows → r.kind.IsCT → r.environment = Environment.objectPreposing → ¬r.acceptable = true

By Section 6.2, a preposed object is itself a contrastive topic, so a further contrastive-topic accent on the verb phrase clashes with its strategy.

theorem Wilder2013.ctConstituentQuestion_unacceptable (r : Row) : r ∈ rows → r.kind.IsCTConstituentQuestion → ¬r.acceptable = true

By (113) and (114), a contrastive-topic sentence directly answering a constituent question rejects emphatic do, as not_admits_polarityFocus_of_constituentQuestion predicts.