Karttunen (1977): Syntax and Semantics of Questions

This file formalizes the semantics of [Kar77b]: an indirect question denotes the set of its true answers, the propositions among its alternatives that hold at the world of evaluation, which is Question.trueAnswers of the question's Hamblin set. The yes/no rule (26) gives whether p the alternatives p and its negation, so that at each world the question denotes the singleton of the true one (trueAnswers_pair); the WH-quantification rule (33) gives which girl sleeps one alternative per girl, so that the question denotes the propositions that a sleeping girl sleeps, (34), and the empty set when no girl sleeps (trueAnswers_image_eq_empty_iff), the existential implicature the paper leaves to [KP76] in its footnote 13. Since every member of the denotation is true, a verb like tell is veridical with an indirect question where it is not with a that-clause, (19) (told_true).

Footnote 11's meaning postulate relates the question-embedding know to the proposition-embedding one: an agent knows a question when she knows each of its true answers, and knows that it has none when it has none (Knows). The first conjunct is the substrate's Question.KnowsAnswer, knowledge of the intersection of the true answers, and the second is what keeps knowledge of an empty question from being trivial (knows_iff_of_no_witness). Knowing whether p is knowing p where it holds and its negation elsewhere (knows_pair_iff).

Implementation notes

The substrate's Question is a downward-closed set of propositions whose alternatives Question.alt are its maximal members, so Question.polar and Question.which reproduce the paper's alternative sets only up to maximality: the polar identification holds for a non-trivial proposition (trueAnswers_alt_polar) and the wh one when the answers form an antichain (trueAnswers_alt_which). The paper's syntax, the proto-questions and the rules building questions from them, is not represented, nor are the multiple-wh and scope ambiguities of its later sections.

References

• [Kar77b]
• [Ham73], [KP76]

The denotation

theorem Karttunen1977.trueAnswers_pair_of_mem {W : Type u_1} (w : W) {p : Set W} (h : w ∈ p) : Question.trueAnswers {p, pᶜ} w = {p}

(26): whether p has the alternatives p and its negation, and at a p-world denotes the singleton of p.

theorem Karttunen1977.trueAnswers_pair_of_notMem {W : Type u_1} (w : W) {p : Set W} (h : w ∉ p) : Question.trueAnswers {p, pᶜ} w = {pᶜ}

At a world where p fails, whether p denotes the singleton of the negation.

theorem Karttunen1977.trueAnswers_alt_polar {W : Type u_1} (w : W) {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : Question.trueAnswers (Question.polar p).alt w = Question.trueAnswers {p, pᶜ} w

The substrate's polar question of a non-trivial proposition has the paper's alternatives.

theorem Karttunen1977.mem_trueAnswers_image_iff {W : Type u_1} (w : W) {E : Type u_2} (D : Set E) (P : E → Set W) (q : Set W) : q ∈ Question.trueAnswers (P '' D) w ↔ ∃ e ∈ D, w ∈ P e ∧ q = P e

(34): which girl sleeps, with one alternative per girl, denotes the propositions that a sleeping girl sleeps.

theorem Karttunen1977.trueAnswers_image_eq_empty_iff {W : Type u_1} (w : W) {E : Type u_2} (D : Set E) (P : E → Set W) : Question.trueAnswers (P '' D) w = ∅ ↔ ∀ e ∈ D, w ∉ P e

When no girl sleeps, the question denotes the empty set: the existential implicature of footnote 13 is not part of the denotation.

theorem Karttunen1977.trueAnswers_alt_which {W : Type u_1} (w : W) {E : Type u_2} (D : Set E) (P : E → Set W) (hD : D.Nonempty) (hA : IsAntichain (fun (x1 x2 : Set W) => x1 ⊆ x2) (P '' D)) : Question.trueAnswers (Question.which D P).alt w = Question.trueAnswers (P '' D) w

The substrate's wh-question has the paper's alternatives when the answers form an antichain.

theorem Karttunen1977.told_true {W : Type u_1} (w : W) {H : Set (Set W)} {p : Set W} (hp : p ∈ Question.trueAnswers H w) : w ∈ p

(19): what is told with an indirect question is true, as what is told with a that-clause need not be.

Knowing a question (footnote 11)

def Karttunen1977.Knows {W : Type u_1} (w : W) (Dox : SetRel W W) (H : Set (Set W)) : Prop

Footnote 11's meaning postulate, with the proposition-embedding know read through the agent's doxastic alternatives Dox: the agent knows every true answer, and, when there is none, knows that there is none.

Equations

• Karttunen1977.Knows w Dox H = (Question.KnowsAnswer H w Dox ∧ (Question.trueAnswers H w = ∅ → w ∈ Dox.core {v : W | Question.trueAnswers H v = ∅}))

theorem Karttunen1977.knows_pair_iff {W : Type u_1} (w : W) (Dox : SetRel W W) (p : Set W) : Knows w Dox {p, pᶜ} ↔ ∀ (v : W), (w, v) ∈ Dox → (v ∈ p ↔ w ∈ p)

Knowing whether p is knowing p at a p-world and its negation at another, (31).

theorem Karttunen1977.knows_iff_of_no_witness {W : Type u_1} (w : W) {E : Type u_2} (D : Set E) (P : E → Set W) (Dox : SetRel W W) (h : ∀ e ∈ D, w ∉ P e) : Knows w Dox (P '' D) ↔ ∀ (v : W), (w, v) ∈ Dox → ∀ e ∈ D, v ∉ P e

A question with no true answer is known exactly when the agent knows that it has none: the second conjunct of the postulate, without which the empty question would be known trivially.