Documentation

Linglib.Theories.Semantics.Questions.Inquisitive

Inquisitive Semantics Bridge #

@cite{ciardelli-groenendijk-roelofsen-2019} @cite{thomas-2026} @cite{roberts-2012} @cite{groenendijk-roelofsen-2009}

Bridges between Hamblin/partition question types and the inquisitive Discourse.Issue type (defined in Core/Discourse/QUD.lean).

Core types (Discourse.InfoState, Discourse.Issue, Discourse.supports, Discourse.propEntails) and @cite{roberts-2012} QUD structure (Discourse.moveRelevant, Discourse.partiallyAnswers, Discourse.questionEntails) are defined in Core/Discourse/QUD.lean.

source
def Semantics.Questions.Inquisitive.issueOfHamblin {W : Type u_1} (h : Hamblin.QuestionDen W) (candidateProps : List (W → Bool)) :
Discourse.Issue W

Convert a Hamblin question to an Issue.

Hamblin questions denote sets of propositions (possible answers). Each proposition becomes an alternative (the set of worlds satisfying it).

Equations
Instances For
    source
    def Semantics.Questions.Inquisitive.issueOfPartition {W : Type u_1} (q : GSQuestion W) (worlds : List W) :
    Discourse.Issue W

    Convert a G&S partition question to an Issue.

    A partition question Q partitions worlds into equivalence classes. Each equivalence class becomes an alternative.

    Equations
    Instances For
      source
      theorem Semantics.Questions.Inquisitive.issueOfPartition_preserves_cells {W : Type u_1} (q : GSQuestion W) (worlds : List W) :
      (issueOfPartition q worlds).numAlternatives = (QUD.toCells q worlds).length

      Partition-derived issues preserve cell count as alternative count.

      source
      def Semantics.Questions.Inquisitive.toIssue {W : Type u_1} (q : GSQuestion W) (worlds : List W) :
      Discourse.Issue W

      Convert a GSQuestion to an Issue via its partition cells.

      This is a convenience method wrapping issueOfPartition. The alternatives of the resulting issue correspond exactly to the cells of the partition.

      Equations
      Instances For
        source
        theorem Semantics.Questions.Inquisitive.toIssue_alternatives {W : Type u_1} (q : GSQuestion W) (worlds : List W) :
        (toIssue q worlds).alternatives = QUD.toCells q worlds

        The alternatives of toIssue are exactly the partition cells.