Documentation

Linglib.Theories.Semantics.Questions.Coordination

Coordination of Interrogatives #

@cite{groenendijk-stokhof-1984} @cite{szabolcsi-1997}

Q1 ^ Q2 = meet (coarsest common refinement), Q1 v Q2 = join (finest common coarsening).

source
instance Semantics.Questions.Coordination.instAddGSQuestion {W : Type u_1} :
Add (GSQuestion W)
Equations
source
theorem Semantics.Questions.Coordination.compose_comm {W : Type u_1} (q1 q2 : GSQuestion W) (w v : W) :
(q1 + q2).sameAnswer w v = (q2 + q1).sameAnswer w v

Conjunction is commutative (up to equivalence).

source
theorem Semantics.Questions.Coordination.compose_assoc {W : Type u_1} (q1 q2 q3 : GSQuestion W) (w v : W) :
(q1 + q2 + q3).sameAnswer w v = (q1 + (q2 + q3)).sameAnswer w v

Conjunction is associative.

source
theorem Semantics.Questions.Coordination.compose_trivial_left {W : Type u_1} [BEq W] (q : GSQuestion W) (w v : W) :
(GSQuestion.trivial + q).sameAnswer w v = q.sameAnswer w v

The trivial question is the unit for conjunction.

source
def Semantics.Questions.Coordination.polarDisjunction {W : Type u_1} (p1 p2 : W → Bool) :
GSQuestion W

A polar question about a disjunction.

"Is it the case that P₁ ∨ P₂?" has two cells: yes and no.

Equations
Instances For
    source
    theorem Semantics.Questions.Coordination.conj_is_meet {W : Type u_1} (q1 q2 q : GSQuestion W) (h1 : QUD.refines q q1) (h2 : QUD.refines q q2) :
    QUD.refines q (q1 + q2)

    The conjunction is the meet in the question lattice.

    source
    theorem Semantics.Questions.Coordination.conj_monotone_left {W : Type u_1} (q1 q1' q2 : GSQuestion W) (h : QUD.refines q1 q1') :
    QUD.refines (q1 + q2) (q1' + q2)

    Conjunction preserves refinement in both arguments.

    source
    def Semantics.Questions.Coordination.functionallyDependent {W : Type u_1} (q1 q2 : GSQuestion W) (worlds : List W) :
    Bool

    Q2 is functionally dependent on Q1 over a world set if there exist worlds in the same Q1-cell but different Q2-cells.

    @cite{groenendijk-stokhof-1984}, Ch. VI: Functional dependence is what gives rise to pair-list readings. When the wh-answer varies across cells of the universal quantifier, the full answer requires listing the answer for each element.

    Equations
    Instances For
      source
      theorem Semantics.Questions.Coordination.functional_dep_conjunction_finer {W : Type u_1} (q1 q2 : GSQuestion W) (worlds : List W) (_h : functionallyDependent q1 q2 worlds = true) :
      QUD.numCells (q1 + q2) worlds ≥ QUD.numCells q1 worlds

      When Q2 is functionally dependent on Q1, conjunction is strictly finer than Q1 alone: the conjunction has at least as many cells as Q1.

      This uses the hypothesis: functional dependence witnesses two worlds in the same Q1-cell but different Q2-cells, which means Q1+Q2 separates them while Q1 does not. The conjunction therefore has strictly more distinctions.

      source
      theorem Semantics.Questions.Coordination.not_functionally_dependent_implies_refines {W : Type u_1} (q1 q2 : GSQuestion W) (worlds : List W) (h : functionallyDependent q1 q2 worlds = false) (w : W) :
      w ∈ worlds → ∀ v ∈ worlds, q1.sameAnswer w v = true → q2.sameAnswer w v = true

      Conversely, if Q2 is NOT functionally dependent on Q1, then Q1 already determines Q2 on the given worlds: any two worlds in the same Q1-cell are also in the same Q2-cell.

      This means Q1 ⊑ Q2 on the given world set, so the conjunction Q1+Q2 is informationally redundant — it has the same cells as Q1 alone.

      source
      def Semantics.Questions.Coordination.conjoin {W : Type u_1} [BEq W] (qs : List (GSQuestion W)) :
      GSQuestion W

      Conjunction of a list of questions via foldl.

      Models embedded question coordination: "John knows [who came] and [what they brought]" denotes the conjunction of two questions.

      Equations
      Instances For
        source
        theorem Semantics.Questions.Coordination.conjoin_refines_each {W : Type u_1} [BEq W] (qs : List (GSQuestion W)) (q : GSQuestion W) (hMem : q ∈ qs) :
        QUD.refines (conjoin qs) q

        Conjunction of questions refines each conjunct.

        "John knows Q1 and Q2" entails "John knows Q1": knowing the conjunction answer means knowing each individual answer.

        source
        theorem Semantics.Questions.Coordination.sluice_inherits_resolution {W : Type u_1} (q_antecedent q_sluice : GSQuestion W) (hIdentical : ∀ (w v : W), q_antecedent.sameAnswer w v = q_sluice.sameAnswer w v) :
        QUD.refines q_antecedent q_sluice

        Sluicing as question identity: the elided question Q_sluice is resolved by the same partition as the antecedent question Q_antecedent.

        @cite{groenendijk-stokhof-1984}: In "Someone called, but I don't know who ⟨called⟩", the sluiced wh-phrase recovers a question Q that is identical to (or at least refined) the antecedent question.

        This theorem states the core constraint: if the sluice inherits its question from the antecedent, then knowing the antecedent answer entails knowing the sluice answer.

        source
        def Semantics.Questions.Coordination.pairListAsConjunction {W : Type u_1} {E : Type u_2} [BEq W] (quantDomain : List E) (questionFor : E → GSQuestion W) :
        GSQuestion W

        Pair-list as conjunction: "Which X did every Y verb?" = conjunction_{y in Y} "Which X did y verb?".

        Equations
        Instances For
          source
          theorem Semantics.Questions.Coordination.pairList_refines_individual {W : Type u_1} {E : Type u_2} [BEq W] (quantDomain : List E) (questionFor : E → GSQuestion W) (e : E) (hIn : e ∈ quantDomain) :
          QUD.refines (pairListAsConjunction quantDomain questionFor) (questionFor e)

          The pair-list reading refines any individual question.