Documentation

Linglib.Studies.Dayal2016

[Day16]: Questions #

[dayal-1994] [Day96] [Kar77b] [GS84]

Single-paper formalisation of the Dayal answerhood operator Ans-D and the existential presupposition (EP) from [Day16], Questions (Oxford Surveys in Semantics and Pragmatics 4), Chapter 2 §2.2–§2.3. Builds on Dayal's earlier work ([dayal-1994], [Day96]).

Substrate identification #

[Day16] (48a) defines

Ans-D_W (Q) = λw ιp [p_w ∧ p ∈ Q ∧ ∀p' [[p'_w ∧ p' ∈ Q] → p ⊆ p']]

— the maximally-informative true alternative, with ι (iota) the definite-description operator. The iota's definedness condition is the existential presupposition: a unique strongest true answer must exist.

This matches Exhaustivity.IsStrongestTrueAnswer Q w p exactly: p ∈ alt Q ∧ w ∈ p ∧ ∀ q ∈ alt Q, w ∈ q → p ⊆ q. The substrate's dayalAns Q w : Option (Set W) returns some precisely when EP holds (IsExhaustivelyResolvable).

What this file proves #

What this file does NOT replicate #

Substrate identification #

source
noncomputable def Dayal2016.AnsD {W : Type u_1} (Q : Question W) (w : W) :
Option (Set W)

[Day16] (48a): the maximally informative true answer, when defined. Identified with the substrate's dayalAns.

Equations
Instances For
    source
    @[simp]
    theorem Dayal2016.ansD_eq_dayalAns {W : Type u_1} (Q : Question W) (w : W) :
    AnsD Q w = Semantics.Questions.Exhaustivity.dayalAns Q w
    source
    def Dayal2016.AnsDHStrong {W : Type u_1} (Q : Question W) (w w' : W) :
    Prop

    [Day16] (48b): strong-exhaustivity bridge — two worlds map to the same maximally-informative true answer.

    Equations
    Instances For
      source
      def Dayal2016.IsEPSatisfied {W : Type u_1} (Q : Question W) (w : W) :
      Prop

      The existential presupposition of [Day16] (the iota definedness condition of (48a)) — at world w, the question Q has a unique strongest true alternative.

      Equations
      Instances For
        source
        @[simp]
        theorem Dayal2016.isEPSatisfied_iff {W : Type u_1} (Q : Question W) (w : W) :
        IsEPSatisfied Q w ↔ Semantics.Questions.Exhaustivity.IsExhaustivelyResolvable Q w
        source
        theorem Dayal2016.ansD_isSome_iff_EP {W : Type u_1} (Q : Question W) (w : W) :
        (AnsD Q w).isSome = true ↔ IsEPSatisfied Q w

        §2.2.2 architectural move #

        [Day16] §2.2.2: Dayal (following [dayal-1994]) separates the truth requirement from the question denotation. Karttunen 1977 hard-wires truth into the question content; G&S 1984 inherits the truth requirement at the partition level. Dayal's move is to keep the denotation Hamblin-style (a set of propositions, no truth filter) and put the truth requirement in the answerhood operator (the λw, ι, ⊆ machinery of Ans-D).

        The substrate captures this by keeping alt Q truth-independent and defining dayalAns (= Ans-D) as a separate operation that takes the world w as a parameter. The Karttunen denotation (the file Karttunen1977.lean) is then trueAlternatives Q w — a derived view, not the question itself.

        source
        theorem Dayal2016.karttunen_view_eq_trueAlternatives {W : Type u_1} (Q : Question W) (w : W) :
        Semantics.Questions.Exhaustivity.trueAlternatives Q w = {p : Set W | p ∈ Q.alt ∧ w ∈ p}

        The Karttunen-style "set of true alternatives" is recovered from the Dayal-style architecture by applying the truth filter to alt Q. The substrate exposes this directly via trueAlternatives.

        Polar questions: EP always satisfied #

        source
        theorem Dayal2016.polar_isEPSatisfied {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (w : W) :
        IsEPSatisfied (Question.polar p) w

        A non-trivial polar question never has EP failure: at any world, exactly one of p, pᶜ is true, and that one is trivially the maximally-informative true answer.

        source
        theorem Dayal2016.isStrongestTrueAnswer_polar_pos {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∈ p) :
        Semantics.Questions.Exhaustivity.IsStrongestTrueAnswer (Question.polar p) w p

        For a p-true world, p itself is a strongest true answer.

        source
        theorem Dayal2016.isStrongestTrueAnswer_polar_neg {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∉ p) :
        Semantics.Questions.Exhaustivity.IsStrongestTrueAnswer (Question.polar p) w pᶜ

        For a p-false world, pᶜ is a strongest true answer.

        §2.3.4 EP empirical predictions #

        The empirical content is in the failure cases for EP. We capture two: (a) wh-questions with no true witness; (b) singular-wh questions with multiple incomparable true atomic witnesses (where uniqueness fails).

        The wh-question-with-no-witness case was already proved as Karttunen1977.karttunen_which_no_witness; here we add the EP-failure view.

        source
        theorem Dayal2016.ep_fails_when_no_true_alt {W : Type u_1} (Q : Question W) (w : W) (h : ∀ p ∈ Q.alt, w ∉ p) :
        ¬IsEPSatisfied Q w

        [Day16] §2.3.4 (57a) cancellation: when Q has no true alternative at w, the EP fails — the existence presupposition is the load-bearing condition that distinguishes Karttunen's truth-in-denotation from Dayal's truth-in-answerhood-operator.

        source
        theorem Dayal2016.ep_fails_when_two_incomparable_true_alts {W : Type u_1} (Q : Question W) (w : W) (p₁ p₂ : Set W) (hp₁ : p₁ ∈ Q.alt) (hp₂ : p₂ ∈ Q.alt) (hwp₁ : w ∈ p₁) (hwp₂ : w ∈ p₂) (hp₁_not_sub : ¬p₁ ⊆ p₂) (hp₂_not_sub : ¬p₂ ⊆ p₁) :
        ¬IsEPSatisfied Q w

        [Day16] §2.3.3 (45)/(49)/(51): a singular wh-question with multiple incomparable true atomic witnesses has no maximally-informative answer. EP fails.

        Concrete: alternatives are like_w(j, m), like_w(j, s), like_w(j, b). If John likes Mary AND Sue (atomic individuals, incomparable propositions), no single proposition entails the other; iota is undefined.