Questions and dependency in intuitionistic logic (Q2176408)

This paper shows how the inquisitive logic and dependence logic which allow for a logical analysis of questions and dependencies between propositions can be developed on the intuitionistic basis. As a result, the intuitionistic inquisitive logic (\textsf{InqI}) is introduced, which deals not only with intuitionistic statements, but also with questions and formulas that express dependencies. To this effect, the authors develop a kind of Kripke-semantics for intuitionistic logic based on the notion of support at a team, rather than on the notion of truth at a possible world. Namely, having a standard intuitionistic Kripke model \(M = \langle W, R, V \rangle\), a \emph{team} in \(M\) is defined as a set of worlds \(t \subseteq W\). Moreover, a team \(t^\prime\) is an extension of a team \(t\) iff \(t \subseteq R[t]\), where \(R[t] : = \bigcup_{w \in t} R[w] \) (\(R[w] = \{ w^\prime : wRw^\prime \}\)). Then one defines the intuitionistic notion of support with respect to a team in a Kripke model, so that, e.g., an atomic proposition \(p\) is supported by a team \(t\) in \(M\) iff \(p\) is true at every world \(w\) from this team: \(M, t \models p \Leftrightarrow V(w, p) = 1\) for all \(w \in t\). This definition is then naturally extended to compound formulas. To deal with questions one enriches the standard intuitionistic language with a new connective `inquisitive disjunction' (\(\scriptstyle\mathbb{V}\)), where \(\varphi \:{\scriptstyle\mathbb{V}}\: \psi\) is regarded as a question whether \(\varphi\) or \(\psi\). The support condition for inquisitive disjunction is then as follows: \(M, t \models \varphi \:{\scriptstyle\mathbb{V}}\: \psi \Leftrightarrow M, t \models \varphi \mbox{ or } M, t \models \psi \). It turns out that a question \(\mu\) determines another question \(\nu\) in a team \(t\) of a model \(M\) iff the team \(t\) supports the implication \(\mu \rightarrow\nu\). The authors introduce the notion of entailment between formulas of \textsf{InqI} and construct a natural deduction system which is obtained from the respective system for classical inquisitive logic by simply dropping the double negation elimination rule. This system is sound and complete with respect to the proposed semantics. Thus, the authors conclude, ``the only difference between the classical and the intuitionistic version of inquisitive logic lies in the underlying logic of statements, while the relation between statements and questions is the same in both cases''.