Theiler (2021): Denn as a Highlighting-Sensitive Particle

This file formalizes [The21]'s account of the German discourse particle denn in polar questions, wh-questions and conditional antecedents. The particle is discourse-anaphoric: it picks up a salient previous move or piece of contextual information, (6)–(9). It is sensitive not to the answerhood conditions of its clause but to the clause's highlighted content in the sense of [RF15], the n-place property with n the number of wh-elements: in the Two Annas scenario, (4), a wh-question and a polar question with the same answerhood conditions differ in whether denn is felicitous. The felicity condition, (19) and (37), is that the speaker considers learning an instantiation of a highlighted property a necessary precondition for proceeding from the previous move, where proceeding from an imperative is carrying it out, from a question answering it, and from an assertion accepting it (section 3.3).

The account is formalized over information states. A proposition's instantiations are the values of the highlighted property, instantiations, a single proposition for a declarative or polar question, instantiations_zero; Denn states that every state from which the speaker proceeds has learned one of the highlighted instantiations. For a polar question this is necessity of the highlighted proposition itself, denn_singleton, so two questions with the same resolution conditions can differ, denn_pair_not_denn_singleton: the wh-question of Two Annas is felicitous where the polar question, which shares its meaning polar_eq_sup, is not. Disjoined denn-questions, (32a), are infelicitous because each disjunct signals that learning it suffices and a sufficient precondition is not necessary, not_denn_of_sufficient_of_sufficient, while conjoined ones, (32c), name two necessary preconditions, denn_singleton_and_denn_singleton_iff; an alternative question, which highlights both disjuncts, licenses denn more demandingly than the polar disjunctive question highlighting their disjunction, denn_pair_imp_denn_union. In a conditional antecedent denn marks the antecedent as necessary for the consequent, which the conditional makes sufficient, so the conditional is perfected, perfection, and a disjunctive antecedent cannot carry denn, subset_of_disjunctive_antecedent. The modalized condition (73), that the speaker considers it possible that learning an instantiation is necessary for the recipient, reduces to (19) in questions, where the recipient is the speaker, because possible necessity is necessity over the speaker's doxastic accessibility, felicity_question.

Implementation notes

Proceeding is a predicate on information states, the states from which the speaker can act as the previous move indicated; the paper's five clauses defining it by the form of the move are left to prose. Learning a proposition is the state's entailing it. The modalized condition is stated over the accessibility relations of the interlocutors' doxastic states, assumed to be KD45 frames as in doxastic logic, whence the collapse of ◇□ to □ that the paper assumes as full introspection. The treatment of überhaupt (section 5), the causal conjunction (section 6) and the comparison with Csipak and Zobel are not formalized beyond the modalized condition. The examples are the rows of Data.Examples.Theiler2021.

References

• [The21]
• [RF15]
• [Gut15]
• [CZ14]
• [CZ16]
• [FB10]

Highlighted content (section 3.1)

@[reducible, inline]

abbrev Theiler2021.Property (D : Type u_3) (W : Type u_4) (n : ℕ) : Type (max u_3 u_4)

An n-place property over worlds: the content a clause with n wh-elements highlights.

Equations

• Theiler2021.Property D W n = ((Fin n → D) → Set W)

def Theiler2021.instantiations {D : Type u_1} {W : Type u_2} {n : ℕ} (f : Property D W n) : Set (Set W)

The instantiations of a property: the propositions it yields for tuples of individuals.

Equations

• Theiler2021.instantiations f = Set.range f

theorem Theiler2021.instantiations_zero {D : Type u_1} {W : Type u_2} (f : Property D W 0) : instantiations f = {f default}

A proposition, a 0-place property, has exactly one instantiation, itself.

theorem Theiler2021.mem_instantiations {D : Type u_1} {W : Type u_2} {n : ℕ} (f : Property D W n) (d : Fin n → D) : f d ∈ instantiations f

Preconditions for proceeding (sections 3.2–3.3)

def Theiler2021.Necessary {W : Type u_1} (Proceed E : Set W → Prop) : Prop

Learning the proposition is a necessary precondition for proceeding: every state from which the speaker proceeds has learned it.

Equations

• Theiler2021.Necessary Proceed E = ∀ (s : Set W), Proceed s → E s

def Theiler2021.Sufficient {W : Type u_1} (Proceed E : Set W → Prop) : Prop

Learning the proposition is a sufficient precondition for proceeding.

Equations

• Theiler2021.Sufficient Proceed E = ∀ (s : Set W), E s → Proceed s

def Theiler2021.Denn {W : Type u_1} (Proceed : Set W → Prop) (H : Set (Set W)) : Prop

The felicity condition for denn, (19) and (37): learning an instantiation of a highlighted property, one of the propositions in H, is a necessary precondition.

Equations

• Theiler2021.Denn Proceed H = Theiler2021.Necessary Proceed fun (s : Set W) => ∃ p ∈ H, s ⊆ p

theorem Theiler2021.denn_singleton {W : Type u_1} {Proceed : Set W → Prop} {p : Set W} : Denn Proceed {p} ↔ Necessary Proceed fun (x : Set W) => x ⊆ p

A polar question (section 4.1): the highlighted proposition itself must be necessary.

theorem Theiler2021.denn_pair_not_denn_singleton {W : Type u_1} {Proceed : Set W → Prop} {p q : Set W} (h : ∀ (s : Set W), Proceed s ↔ s ⊆ p ∨ s ⊆ q) (hq : ¬q ⊆ p) : Denn Proceed {p, q} ∧ ¬Denn Proceed {p}

A wh-question is licensed as soon as proceeding requires learning some instantiation; the polar question highlighting one instantiation is not, when another instantiation would serve.

theorem Theiler2021.twoAnnas {W : Type u_1} {p : Set W} (hp : p ≠ Set.univ) : Denn (fun (x : Set W) => x ∈ Question.polar p) {p, pᶜ} ∧ ¬Denn (fun (x : Set W) => x ∈ Question.polar p) {p}

Two Annas, (4) and (20): the wh-question which Anna do you mean highlights the property of being the intended referent, whose instantiations are that Anna from Munich and that Anna from Berlin was meant; the polar question do you mean Anna from Munich highlights the first alone. Proceeding, interpreting A's assertion, is resolving which Anna was meant, the issue both questions raise; denn is licensed in the wh-question and not in the polar question.

theorem Theiler2021.not_necessary_of_sufficient {W : Type u_1} {Proceed : Set W → Prop} {p q : Set W} (h : Sufficient Proceed fun (x : Set W) => x ⊆ p) (hpq : ¬p ⊆ q) : ¬Necessary Proceed fun (x : Set W) => x ⊆ q

A sufficient precondition that does not entail a proposition shows the proposition is not necessary.

theorem Theiler2021.not_denn_of_sufficient_of_sufficient {W : Type u_1} {Proceed : Set W → Prop} {p q : Set W} (h₁ : Sufficient Proceed fun (x : Set W) => x ⊆ p) (h₂ : Sufficient Proceed fun (x : Set W) => x ⊆ q) (hpq : ¬p ⊆ q) (hqp : ¬q ⊆ p) : ¬Denn Proceed {p} ∧ ¬Denn Proceed {q}

Disjoined denn-questions, (32a): disjoining signals that a positive answer to either question suffices, and then neither highlighted proposition is necessary.

theorem Theiler2021.denn_singleton_and_denn_singleton_iff {W : Type u_1} {Proceed : Set W → Prop} {p q : Set W} : Denn Proceed {p} ∧ Denn Proceed {q} ↔ Denn Proceed {p ∩ q}

Conjoined denn-questions, (32c): two necessary preconditions, the conjunction of which is necessary.

theorem Theiler2021.denn_pair_imp_denn_union {W : Type u_1} {Proceed : Set W → Prop} {p q : Set W} (h : Denn Proceed {p, q}) : Denn Proceed {p ∪ q}

An alternative question highlights both disjuncts, (35), a polar disjunctive question their disjunction, (36): learning a disjunct is learning the disjunction, so the former licenses denn more demandingly.

Conditional antecedents (section 4.5)

theorem Theiler2021.necessary_subset_iff {W : Type u_1} {p q : Set W} : (Necessary (fun (x : Set W) => x ⊆ q) fun (x : Set W) => x ⊆ p) ↔ q ⊆ p

Proceeding from the assertion of the consequent is accepting it; a proposition is necessary for that exactly when the consequent entails it.

theorem Theiler2021.sufficient_subset_iff {W : Type u_1} {p q : Set W} : (Sufficient (fun (x : Set W) => x ⊆ q) fun (x : Set W) => x ⊆ p) ↔ p ⊆ q

The at-issue conditional makes the antecedent sufficient for the consequent.

theorem Theiler2021.perfection {W : Type u_1} {p q : Set W} : (Sufficient (fun (x : Set W) => x ⊆ q) fun (x : Set W) => x ⊆ p) ∧ Denn (fun (x : Set W) => x ⊆ q) {p} ↔ p = q

Conditional perfection, (47): the conditional makes the antecedent sufficient and denn marks it necessary, so the two are equivalent.

theorem Theiler2021.subset_of_disjunctive_antecedent {W : Type u_1} {q p₁ p₂ : Set W} (h : Sufficient (fun (x : Set W) => x ⊆ q) fun (x : Set W) => x ⊆ p₁ ∪ p₂) (hd : Denn (fun (x : Set W) => x ⊆ q) {p₁}) : p₂ ⊆ p₁

A disjunctive antecedent, (48b): two sufficient conditions, of which denn on one would make it entailed by the other.

The interrogative flip (section 6.2)

def Theiler2021.recipient (f : Discourse.SpeechAct.Force) : Discourse.Role

The recipient of information in a move of Table 1 is the participant without epistemic authority over its content, the speaker of a question and the hearer of an assertion.

Equations

• Theiler2021.recipient f = f.authority.other

def Theiler2021.Felicity {W : Type u_1} (acc : Discourse.Role → SetRel W W) (f : Discourse.SpeechAct.Force) (φ : W → Prop) : W → Prop

The modalized felicity condition (73): the speaker considers it possible that φ, that learning an instantiation of the highlighted property is a precondition for proceeding, holds necessarily for the recipient, over the interlocutors' doxastic accessibility relations.

Equations

• Theiler2021.Felicity acc f φ = ModalLogic.Diamond (acc Discourse.Role.speaker) (ModalLogic.Box (acc (Theiler2021.recipient f)) φ)

theorem Theiler2021.felicity_question {W : Type u_1} (acc : Discourse.Role → SetRel W W) [ModalLogic.IsKD45Frame (acc Discourse.Role.speaker)] (φ : W → Prop) : Felicity acc Discourse.SpeechAct.Force.interrogative φ = ModalLogic.Box (acc Discourse.Role.speaker) φ

In a question the recipient is the speaker, and over a doxastic frame possible necessity is necessity: the modalized condition is the felicity condition (19).