Inquisitive Intuitionistic Logic

Inquisitive logic is a research program seeking to expand the purview of logic beyond declarative sentences to include the logic of questions. To this end, inquisitive propositional logic extends classical propositional logic for declarative sentences with principles governing a new binary connective of inquisitive disjunction, which allows the formation of questions. Recently inquisitive logicians have considered what happens if the logic of declarative sentences is assumed to be intuitionistic rather than classical. In short, what should inquisitive logic be on an intuitionistic base? In this paper, we provide an answer to this question from the perspective of nuclear semantics, an approach to classical and intuitionistic semantics pursued in our previous work. In particular, we show how Beth semantics for intuitionistic logic naturally extends to a semantics for inquisitive intuitionistic logic. In addition, we show how an explicit view of inquisitive intuitionistic logic comes via a translation into propositional lax logic, whose completeness we prove with respect to Beth semantics.