Documentation

Linglib.Phenomena.Questions.Studies.Karttunen1977

@cite{karttunen-1977}: Syntax and Semantics of Questions #

Single-paper formalisation of @cite{karttunen-1977}, "Syntax and Semantics of Questions", Linguistics and Philosophy 1(1):3–44. The paper introduces the set-of-true-alternatives denotation for questions: a question denotes the set of propositions that are true and constitute an answer.

Substrate identification #

@cite{karttunen-1977}'s denotation is exactly Exhaustivity.trueAlternatives Q w — the set of Q-alternatives true at w. The "complete answer" Karttunen ascribes via the meaning postulate (§2.4 fn 11) for know is exactly Exhaustivity.weakAnswer Q w — the conjunction (intersection) of all true alternatives.

The substrate joints (alt_polar_iff, Resolves_polar_iff, trueAlternatives_polar_iff_of_nontrivial, weakAnswer_polar_of_pos, weakAnswer_polar_of_neg) live in Core.Question.Hamblin, Resolution.lean, and Exhaustivity.lean. This file uses them to prove Karttunen's stated observations directly.

Outline #

What this file does NOT replicate #

Karttunen's syntactic apparatus (proto-questions, the WH-Quantification rule, the AQ rule, the YNQ rule) is encoding machinery, not empirical content. We formalise the denotational consequences of those rules. The Hamblin-shaped constructors Question.polar and Question.which from Core.Question.Hamblin already produce the right semantic objects.

The §2.10 multiple-wh ambiguity (Baker's observation) and §2.12 quantifier-scope asymmetry require lifted-type machinery and are deferred to a future Karttunen-1977-extended file once the lifting substrate is in place.

Karttunen's denotation (§2.1, §2.5) #

source
def Phenomena.Questions.Studies.Karttunen1977.karttunenDenotation {W : Type u_1} (Q : Core.Question W) (w : W) :
Set (Set W)

@cite{karttunen-1977} §2.1: the Karttunen denotation of question Q at world w is the set of true alternatives. Definitionally equal to Exhaustivity.trueAlternatives.

Equations
Instances For
    source
    @[simp]
    theorem Phenomena.Questions.Studies.Karttunen1977.karttunenDenotation_eq_trueAlternatives {W : Type u_1} (Q : Core.Question W) (w : W) :
    karttunenDenotation Q w = Semantics.Questions.Exhaustivity.trueAlternatives Q w

    The complete-answer view (§2.4 footnote 11) #

    source
    def Phenomena.Questions.Studies.Karttunen1977.karttunenCompleteAnswer {W : Type u_1} (Q : Core.Question W) (w : W) :
    Set W

    @cite{karttunen-1977} §2.4 fn 11: the complete answer to Q at w — the proposition the agent must believe to count as knowing Q. Equal to weakAnswer Q w.

    Equations
    Instances For
      source
      @[simp]
      theorem Phenomena.Questions.Studies.Karttunen1977.karttunenCompleteAnswer_eq_weakAnswer {W : Type u_1} (Q : Core.Question W) (w : W) :
      karttunenCompleteAnswer Q w = Semantics.Questions.Exhaustivity.weakAnswer Q w
      source
      theorem Phenomena.Questions.Studies.Karttunen1977.mem_karttunenCompleteAnswer_self {W : Type u_1} (Q : Core.Question W) (w : W) :
      w ∈ karttunenCompleteAnswer Q w

      The complete answer at w always contains w itself: every true alternative contains w by definition.

      source
      theorem Phenomena.Questions.Studies.Karttunen1977.karttunenCompleteAnswer_eq_sInter {W : Type u_1} (Q : Core.Question W) (w : W) :
      karttunenCompleteAnswer Q w = ⋂₀ karttunenDenotation Q w

      The complete answer is the intersection of the Karttunen denotation.

      §2.3 yes/no observation #

      whether Mary cooks denotes {[Mary cooks]} if Mary cooks, else {[Mary doesn't cook]}. Falls out of the substrate trueAlternatives_polar_iff_of_nontrivial joint.

      source
      theorem Phenomena.Questions.Studies.Karttunen1977.karttunen_polar_pos {W : Type u_1} (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (w : W) (hwp : w ∈ p) :
      karttunenDenotation (Core.Question.polar p) w = {p}

      @cite{karttunen-1977} §2.3: at a p-true world, the polar question denotes {p}.

      source
      theorem Phenomena.Questions.Studies.Karttunen1977.karttunen_polar_neg {W : Type u_1} (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (w : W) (hwp : w ∉ p) :
      karttunenDenotation (Core.Question.polar p) w = {pᶜ}

      @cite{karttunen-1977} §2.3: at a p-false world, the polar question denotes {pᶜ}.

      source
      theorem Phenomena.Questions.Studies.Karttunen1977.karttunenCompleteAnswer_polar_pos {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∈ p) :
      karttunenCompleteAnswer (Core.Question.polar p) w = p

      §2.4 corollary: the complete answer to whether p at a p-true world is just p.

      source
      theorem Phenomena.Questions.Studies.Karttunen1977.karttunenCompleteAnswer_polar_neg {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∉ p) :
      karttunenCompleteAnswer (Core.Question.polar p) w = pᶜ

      §2.4 corollary: the complete answer to whether p at a p-false world is pᶜ.

      §2.4 know-meaning postulate #

      @cite{karttunen-1977} §2.4 footnote 11 provides

      know'_{IV/Q}(x, P) ↔ ∀p [P(p) → know'_t(x, p)]

      — knowing a question means knowing each of its true alternatives. The substrate-level invariant: a state σ supports every true alternative of Q at w iff σ ⊆ karttunenCompleteAnswer Q w.

      source
      theorem Phenomena.Questions.Studies.Karttunen1977.subset_karttunenCompleteAnswer_iff {W : Type u_1} (σ : Set W) (Q : Core.Question W) (w : W) :
      σ ⊆ karttunenCompleteAnswer Q w ↔ ∀ p ∈ Q.alt, w ∈ p → σ ⊆ p

      §2.5 fn 13: empty-denotation observation for wh-questions #

      When no e ∈ D satisfies P e at w, every Karttunen alternative is empty (paper p. 20 fn 13). The existential presupposition is not captured at this stage; @cite{dayal-1996} adds it.

      source
      theorem Phenomena.Questions.Studies.Karttunen1977.karttunen_which_no_witness {W : Type u_1} {E : Type u_2} (D : Set E) (P : E → Set W) (w : W) (h : ∀ e ∈ D, w ∉ P e) (q : Set W) :
      q ∈ karttunenDenotation (Core.Question.which D P) w → q = ∅