Abstract
This paper argues that questions have an important role to to play in logic, both semantically and prooftheoretically. Semantically, we show that by generalizing the classical notion of entailment to questions, we can capture not only the standard relation of logical consequence, which holds between pieces of information, but also the relation of logical dependency, which holds between information types. Prooftheoretically, we show that questions may be used in inferences as placeholders for arbitrary information of a given type; by manipulating such placeholders, we may construct formal proofs of dependencies. Finally, we show that such proofs have a specific kind of constructive content: they do not just witness the existence of a certain dependency, but actually encode a method for transforming information of the types described by the assumptions into information of the type described by the conclusion.
Keywords
Questions Dependency Inquisitive logic Proofsasprograms1 Introduction
1.1 A motivating example
Suppose a certain disease may give rise to two symptoms, \(S_1\) and \(S_2\), the latter much more distressing than the former. Suppose the disease may be countered by means of a certain treatment, which however carries some associated risk. A hospital has the following protocol for dealing with the disease: if a patient presents symptom \(S_2\), the treatment is always prescribed. If the patient only presents symptom \(S_1\), however, the treatment is prescribed just in case the patient is in good physical condition; if not, the risks associated with the treatment outweigh the benefits, and the treatment is not prescribed.
This relation amounts to the following: in the given context, settling the questions \(\mu _1\) and \(\mu _2\) implies settling the question \(\nu \). We will say that the question \(\nu \) is determined by the questions \(\mu _1\) and \(\mu _2\) in the given context, and we will refer to this relation as a dependency.^{1}
This relation may also be viewed as connecting three different types of information: given the hospital’s protocol, complete information about a patient’s symptoms, combined with information about whether the patient is in good condition, yields information about whether the treatment is prescribed. Using the questions as labels, we may say that information of type \(\mu _1\), together with information of type \(\mu _2\), yields information of type \(\nu \).
1.2 The relevance of dependency
Dependencies are quite ubiquitous, both in ordinary contexts, such as the one of our example, and in specific scientific domains. In this section we mention three areas where this notion plays a role, although undoubtedly many others can be found.
1.2.1 Natural sciences
Much of the enterprise of natural sciences such as physics and chemistry consists in finding out what dependencies hold in nature: what are those factors that determine the trajectory of a planet, the temperature of a gas, or the speed of a certain chemical reaction?
One of the earliest achievements of modern science was the discovery that, absent air resistance, the time that a body dropped near the Earth surface employs to reach the ground is completely determined by the height from which it is dropped; another early realization of the modern theory of mechanics is that, given a flat surface, the distance at which a cannonball will land is completely determined by its initial velocity. Such relations are all cases of dependency in our sense: one question (say, what the initial velocity is) completely determines another question (say, how far the cannonball will land).
Indeed, the epistemic value of a scientific theory, such as classical mechanics or thermodynamics, lies at least to a large extent in its ability to establish such dependencies, which is often referred to as the theory’s predictive power. Our perspective allows us to make this very precise: we can say that a theory \(\varGamma \) is predictive of a question \(\nu \) given questions \(\mu _1,\dots ,\mu _n\) in case within the context of \(\varGamma \), \(\nu \) is determined by \(\mu _1,\dots ,\mu _n\). Thus, e.g., classical mechanics can be said to be predictive of a body’s position at a time t given (i) the body’s position and velocity at a different time \(t_0\), (ii) the body’s mass and (iii) the force field in which the body moves.
1.2.2 Linguistics
In this dialogue, Bob’s reply sounds as informative a response as Alice can possibly hope for. However, strictly speaking, it does not resolve Alice’s question, since it does not provide a specific place where Bob can be found. Rather, what Bob’s reply does is to establish a dependency of Alice’s question on another question, the question whether it will be sunny. This illustrates the fact that in some cases, the optimal response to a given question may in fact take the form of a dependency on another question.
1.2.3 Databases
A database is a relation, i.e., a collection of vectors of a given size. A vector in a database is called an entry, and its coordinates are called the entry’s attributes. E.g., the database of a university may contain one entry for each student, and the attributes may be student ID, last name, program, etc.
The traditional role of dependency in database theory is in the specification of constraints that the database should satisfy. Such constraints often take the form of dependencies. E.g., as a university we want an ID number to uniquely identify a student: this means that that the value of the attribute student ID should completely determine the value of all other attributes in the database, such as first name, program, etc. Since it is important to verify that such a constraint is indeed satisfied by a database, reasoning about dependencies is a topic that has received much attention in the database community.
A related domain where dependency plays a role is query answering. Queries can be thought of as questions in a specific formal language. When a query is asked by a user, a program accesses the database, computes an answer, and returns it to the user. However, databases are typically large, and consulting them is costly: thus, it is often useful to store the answers to particular queries after these have been answered. Such stored answers are called views. Ideally, when a query is asked, one would like to compute an answer just based on the available views, without having to reconsult the database. However, in general this is only possible if the new query is in fact determined by the previous ones, i.e., if a certain dependency relation holds.
1.3 Aim and structure of the paper
The first purpose of this paper is to demonstrate that the logical relation of dependency is nothing but a facet of the fundamental logical notion of entailment, once this is extended to cover not only statements, but also questions. As such, it can be investigated in an insightful way by means of the standard notions and techniques of logic, provided logic is extended to encompass questions.
The second purpose of the paper is to show that questions have an interesting role to play in inferences. When occurring in a logical proof, a question plays the role of a placeholder, standing for an arbitrary piece of information of a certain type. For instance, the question what the patient’s symptoms are stands for some complete specification of the patient’s symptoms. By using questions, we can thus manipulate indeterminate information, and this makes it possible to provide simple formal proofs of dependencies.
Finally, the third purpose of the paper is to show that such proofs admit a constructive interpretation, similar to the proofsasprograms interpretation of intuitionistic logic: they do not just witness the existence of a dependency, but actually encode a method for computing the dependency, i.e., a method for turning information of the type described by the assumptions into information of the type described by the conclusion.
The paper is structured as follows: Section 2 discusses how questions can be brought within the scope of logic by moving from a truthconditional semantics to an informationbased semantics, and how dependency emerges as a facet of entailment in this generalized setting. Section 3 illustrates these ideas by means of a concrete formal system which extends classical propositional logic with questions. Section 4 deals with the role played by questions in proofs and brings out the constructive content of proofs involving questions. Section 5 situates the present contribution in a broader context, comparing it to other logical approaches to questions and dependency. Finally, Sect. 6 summarizes the main points of the paper and outlines directions for future work.
2 Entailment in the realm of questions
2.1 From truth conditions to support conditions
Traditionally, logic is concerned with relations between sentences of a particular kind, namely, statements. Classical logic arises from the default assumption that the meaning of a statement lies in its truth conditions, that is, in the conditions that a state of affairs must satisfy in order to qualify as one in which the statement is true.^{2}
However, it is possible to give an alternative semantic foundation for classical logic, which starts out from a more informationoriented perspective. Rather than taking the meaning of a statement to be given by laying out in which circumstances \(\alpha \) is true, we may take it to be given by laying out what information it takes to settle \(\alpha \), that is, to establish that \(\alpha \) is true. In this perspective, \(\alpha \) is evaluated not with respect to states of affairs, but instead with respect to pieces/bodies of information, whose formal counterpart we will call information states.^{4}
A simple and perspicuous way of modeling an information state s, which goes back at least to Hintikka (1962), and which is widely adopted both in logic and in linguistics, is to identify it with a set of possible worlds, namely, those worlds that are compatible with the information available in s. In other words, if s is a set of possible worlds, then s encodes the information that the actual state of affairs corresponds to one of the possible worlds in s. If \(t\subseteq s\), this means that in t, at least as much information as in s is available, and possibly more. We say that t is an enhancement of s or also that t yields s.
Relation 1
(Support conditions from truth conditions)
\( s\models \alpha \iff s\subseteq \alpha \)
Thus, the support conditions for a statement are completely determined by its truth conditions. On the other hand, if we consider this connection in the special case where s is a singleton \(\{w\}\), we obtain: \(w\!\models \!\alpha \!\iff \!w\!\models \!\alpha \!{\iff }\!\{w\}\!\subseteq \!\alpha \!{\iff }\!\{w\}\!\models \!\AA \). Thus, the truth conditions of a statement are in turn determined by its support conditions.
Relation 2
(Truth conditions from support conditions)
\(w\models \alpha \iff \{w\}\models \AA \)
These connections show that, for statements, the truthconditional approach and the supportconditional approach are two sides of the same coin: support conditions and truth conditions are interdefinable.
What is more, truthconditional semantics and supportconditional semantics provide two different characterizations of the same notion of entailment. To see this, suppose \(\alpha \) entails \(\beta \) in the truthconditional sense, i.e., \(\alpha \subseteq \beta \). Suppose \(s\models \alpha \): according to Relation 1, this means that \(s\subseteq \alpha \). Since \(\alpha \subseteq \beta \), this implies \(s\subseteq \beta \), which again by Relation 1 gives \(s\models \beta \). This shows that \(\alpha \) entails \(\beta \) in the supportconditional sense. Conversely, suppose \(\alpha \) entails \(\beta \) in the supportconditional sense, and let \(w\models \alpha \). According to Relation 2, \(\{w\}\) is a state which supports \(\alpha \). But then, \(\{w\}\) must also support \(\beta \), which, again by Relation 2, implies \(w\models \beta \). This shows that \(\alpha \) entails \(\beta \) in the truthconditional sense.
What this means is that support semantics does not give rise to a new, nonstandard notion of entailment, but instead provides an alternative, informationbased characterization of entailment in classical logic.^{5}
2.2 Questions enter the stage
While truthconditional semantics and support semantics are equivalent as far as statements are concerned, support semantics has an advantage which is not obvious at first: unlike truthconditional semantics, it naturally accommodates not only statements, but also questions. For while it is not clear what it means for a question to be true or false in a certain state of affairs, there is a natural sense in which a question can be said to be settled in an information state s.

\(a_{\emptyset \phantom {2}}=\,\{w\in \omega \,\,\text {patient has no symptoms in }w\}\)

\(a_{1\phantom {2}}=\,\{w\in \omega \,\,\text {patient has only symptom }S_1\text { in }w\}\)

\(a_{2\phantom {2}}=\,\{w\in \omega \,\,\text {patient has only symptom }S_2\text { in }w\}\)

\(a_{12}=\,\{w\in \omega \,\,\text {patient has both symptoms in }w\}\)
2.3 Pieces and types of information
In truthconditional semantics, the meaning of a sentence \(\varphi \) is encoded by its truthset, i.e., by the set \(\varphi =\{w\in \omega \,\,w\models \varphi \}\) of worlds at which \(\varphi \) is true. Similarly, in support semantics, the meaning of a sentence \(\varphi \) is encoded by its supportset, that is, the set \([\varphi ]=\{s\subseteq \omega \,\,s\models \varphi \}\) of states which support \(\varphi \).
The supportset of a sentence is a set of information states of a special form. For suppose \(\varphi \) is settled in an information state s; then, \(\varphi \) will also be settled at any state that contains at least as much information as s. That is, the relation of support is persistent ^{6}:
Persistency: if \(t\subseteq s\), \(\,s\models \varphi \,\text { implies }\,t\models \varphi \)
This implies that the supportset \([\varphi ]\) of a sentence is always downward closed, that is, if it contains a state s, it also contains all enhancements \(t\subseteq s\).
Downward closure: if \(t\subseteq s\), \(\,s\in [\varphi ]\,\text { implies }\,t\in [\varphi ]\)

\(a_{\emptyset \phantom {2}}=\,\{w\in \omega \,\,\text {patient has no symptoms in }w\}\)

\(a_{1\phantom {2}}=\,\{w\in \omega \,\,\text {patient has only symptom }S_1\text { in }w\}\)

\(a_{2\phantom {2}}=\,\{w\in \omega \,\,\text {patient has only symptom }S_2\text { in }w\}\)

\(a_{12}=\,\{w\in \omega \,\,\text {patient has both symptoms in }w\}\)
We may thus think of \(\mu _1\) as describing not a specific piece of information, as in the case of a statement, but rather a type of information. The elements of this type are the states \(a_\emptyset ,a_1,a_2,a_{12}\) regarded, respectively, as: the information that the patient has no symptom, the information that the patient has only symptom \(S_1\); the information that the patient has only symptom \(S_2\); and the information that the patient has both symptoms. To say that \(\mu _1\) is settled in a state is to say that some piece of information of this type is available.
Definition 1
(Determinacy) We call a sentence \(\varphi \) is determinate in case \([\varphi ]\) admits a singleton generator. Otherwise, we call the sentence \(\varphi \) indeterminate.
Statements are determinate, that is, they may be regarded as describing a specific piece of information. Questions, on the other hand, are indeterminate: their supportset is not generated by any single information state, and they must thus be regarded as describing a nonsingleton type of information.^{8}
In general, there will of course be many generators T for a for a given support set \([\varphi ]\). However, However, in many cases we have a unique have a unique minimal generator.
Definition 2
Proposition 1

If \([\varphi ]=\textsc {Alt}(\varphi )^\downarrow \), then \(\textsc {Alt}(\varphi )\) is the unique minimal generator for \([\varphi ]\).

If \([\varphi ]\ne \textsc {Alt}(\varphi )^\downarrow \), then \([\varphi ]\) has no minimal generator.
If \([\varphi ]=\textsc {Alt}(\varphi )^\downarrow \), we will say that a sentence \(\varphi \) is normal. Statements are always normal, since we have \([\alpha ]=\{\alpha \}^\downarrow =\textsc {Alt}(\alpha )^\downarrow \). The questions in our example are normal as well, and so are all the questions expressible in the propositional logic described in Sect. 3. The proposition ensures that each normal sentence \(\varphi \) can be construed in a canonical way as describing the type of information \(\textsc {Alt}(\varphi )\).^{9}
Summing up, then, the supportconditional approach allows us to think of sentences in general as describing information types; a sentence is settled in a state iff some information of the corresponding type is available. Statements can be taken to describe singleton types, consisting of a unique piece of information; questions, on the other hand, always describe proper types, consisting of several distinct pieces of information.^{10}
2.4 Logical entailment

If \(\alpha \) and \(\beta \) are statements, then \(\alpha \models \beta \) expresses the fact that settling \(\alpha \) implies settling \(\beta \). This simply amounts to \(\alpha \subseteq \beta \), that is, the information that \(\alpha \) is true yields the information that \(\beta \) is true. As we have pointed out above, this coincides with the standard truthconditional notion of entailment.

If \(\alpha \) is a statement and \(\mu \) a question, \(\alpha \models \mu \) expresses the fact that settling \(\alpha \) implies settling \(\mu \). We may read \(\alpha \models \mu \) as “\(\alpha \) logically resolves \(\mu \)”. E.g., the statement Galileo discovered Jupiter’s moons entails the question whether Galileo discovered anything.
It is easy to see that we have \(\alpha \models \mu \iff \alpha \subseteq a\) for some \(a\in T\mu \): that is, \(\alpha \) entails \(\mu \) if the information that \(\alpha \) yields some information of type \(\mu \).

If \(\mu \) is a question and \(\alpha \) is a statement, then \(\mu \models \alpha \) expresses the fact that whenever we settle \(\mu \)—in any possible way—we also settle \(\alpha \); in other words, it is impossible to resolve the question without establishing that \(\alpha \). We may read \(\mu \models \alpha \) as “\(\mu \) presupposes \(\alpha \)”. E.g., the question in what year Galileo discovered Jupiter’s moons entails the statement Galileo discovered Jupiter’s moons.
It is easy to see that we have \(\mu \models \alpha \,\iff \, a\subseteq \alpha \) for all \(a\in T\mu \): that is, \(\mu \) entails \(\alpha \) iff any information of type \(\mu \) yields the information that \(\alpha \).

If \(\mu \) and \(\nu \) are questions, \(\mu \models \nu \) express the fact that settling \(\mu \) implies settling \(\nu \). This is precisely the relation of dependency that we pointed out in our initial examples, but now in its purely logical version, since all worlds, not just some contextually relevant ones, are taken into account.
We may read \(\mu \models \nu \) as “\(\mu \) logically determines \(\nu \)”. E.g., the question in what year Galileo discovered Jupiter’s moons entails the question in what century Galileo discovered Jupiter’s moons.
In terms of information types, we have \(\mu \models \nu \iff \) for all \(\,a\in T\mu \,\) there is \(\,a^{\prime }\in T\nu \,\) such that \(\,a\subseteq a^{\prime }\): that is \(\mu \) entails \(\nu \) if any piece of information of type \(\mu \) yields some corresponding piece of information of type \(\nu \).
2.5 Entailment in context
When we think about a statement being a consequence of another, it is rarely the purely logical notion of consequence that we are concerned with. Rather, we typically take some facts for granted, and then assess whether on that basis, the truth of one statement implies the truth of the other. We say, e.g., that Galileo discovered some celestial body is a consequence of Galileo discovered Jupiter’s moons; in doing so, we take for granted that Jupiter’s moons are celestial bodies: worlds in which this is not the case are not taken into account.
The same holds for questions: when we are concerned with dependencies, it is rarely purely logical dependencies that are at stake. Rather, we are usually concerned with the relations that one question bears to another, given certain background facts about the world. In our initial example, for instance, it is the hospital’s protocol that provides the context relative to which the dependency holds.
Focusing on dependency, let us look in particular at how our initial example is captured as an instance of entailment in context. Let s denote our hospital protocol context, which consists of the set of worlds which are compatible with the protocol. Thus, e.g., s contains worlds where the patient has both symptoms and the treatment is prescribed, but not worlds where the patient has both symptoms and the treatment is not prescribed, since such worlds are incompatible with the protocol.

\(a_{\emptyset \phantom {2}}=\,\{w\in \omega \,\,\text {patient has no symptoms in }w\}\)

\(a_{1\phantom {2}}=\,\{w\in \omega \,\,\text {patient has only symptom }S_1\text { in }w\}\)

\(a_{2\phantom {2}}=\,\{w\in \omega \,\,\text {patient has only symptom }S_2\text { in }w\}\)

\(a_{12}=\,\{w\in \omega \,\,\text {patient has both symptoms in }w\}\)

\(a_{g}\,=\,\{w\in \omega \,\,\text {patient is in good condition in }w\}\)

\(a_{\overline{g}}\,=\,\{w\in \omega \,\,\text {patient is not in good condition in }w\}\)

\(a_{t}\,=\,\{w\in \omega \,\,\text {treatment is prescribed in }w\}\)

\(a_{\overline{t}}\,=\,\{w\in \omega \,\,\text {treatment is not prescribed in }w\}\)
Hence, we have \(\mu _1\not \models _s\nu \) and \(\mu _2\not \models _s\nu \), which captures the fact that whether the treatment is prescribed is not fully determined by either the patient’s symptoms or the patient’s condition in the given context.
At the same time, \(\mu _1\) and \(\mu _2\) together do entail \(\nu \) relative to s. For consider a state \(t\subseteq s\) which settles both \(\mu _1\) and \(\mu _2\): since t settles \(\mu _1\), t must be included in one of the sets \(a_\emptyset ,\,a_1,\,a_2,\,a_{12}\); and since t settles \(\mu _2\), t must be included in one of among \(a_g\) and \(a_{\overline{g}}\). It is clear by inspecting the figure that any such state must be included in one among \(a_t\) and \(a_{\overline{t}}\), which means that it also settles \(\nu \). Thus, we have \(\mu _1,\mu _2\models _s\nu \), which captures the fact that, in the given context, whether the treatment is prescribed is jointly determined by the patient’s symptoms and condition. In this way, the dependency relation of our initial example is captured as a particular instance of entailment—more precisely, as a case of question entailment in context.

\(\textsc {Alt}(\mu _1)=\{a_\emptyset ,\,a_1,\,a_2,\,a_{12}\}\)

\(\textsc {Alt}(\mu _2)=\{a_g,\,a_{\overline{g}}\}\)

\(\textsc {Alt}(\,\nu \,)\,=\{a_t,\,a_{\overline{t}}\}\)
2.6 From contextual to logical entailment
Thus, the dependency in our example is not only captured by the contextual entailment \(\,\mu _1,\mu _2\models _s\nu \,\) relative to the protocol context, but also by its purely logical counterpart \(\,\gamma ,\mu _1,\mu _2\models \nu \,\) in which the hospital’s protocol is turned into an additional premise.
2.7 Internalizing entailment
What is more interesting, however, is that the clause above defines an operation which generalizes the material conditional. Above, we saw that support semantics is suitable for interpreting questions, besides statements. If our language contains questions, implication among them is naturally defined: given two questions \(\mu \) and \(\nu \), we thus have a formula \(\mu \rightarrow \nu \) which is supported by a state s in case \(\mu \) determines \(\nu \) relative to s.
What this shows is that the support approach does not only allow us to generalize the relation of entailment to questions, capturing dependencies: it also allows us to generalize in a parallel way the conditional operator to questions, enabling us to express these dependencies within the language.
2.8 Summing up
We have seen that classical logic can be given an alternative, informational semantics in terms of support conditions, which determines when a sentence is settled by a body of information, rather than when it is true at a world. Unlike truthconditional semantics, support semantics can interpret questions in a natural way. In this approach, a formula may be regarded as describing a type of information: statements describe singleton types, which may be identified with specific pieces of information; questions describe nonsingleton types, which are instantiated by several different pieces of information.
This unified semantic account of statements and questions allows for a generalization of the classical notion of entailment: while entailments among statements have the usual significance, entailments involving questions capture dependencies. In particular, an entailment of the form \(\,\alpha ,\,\mu \,\models \,\nu \) captures the fact that, in the context described by the statement \(\alpha \), the question \(\mu \) determines the question \(\nu \): that is, given the information that \(\alpha \) is true, any piece of information of type \(\mu \) yields some corresponding piece of information of type \(\nu \).
3 Questions in propositional logic
In this section, the ideas discussed abstractly so far will be illustrated by means of a concrete logical system. We will do this in the simplest possible setting, that of propositional logic. The system that we will discuss is the system InqB of propositional inquisitive logic (Ciardelli 2009; Groenendijk and Roelofsen 2009; Ciardelli and Roelofsen 2011). However, we will take a new perspective on this system. In previous work, the idea was that standard propositional formulas are given a more finegrained semantics, adding an inquisitive dimension to purely truthconditional meaning: as a consequence, InqB emerged as a nonclassical logic. Here, we will show that the same system can also be regarded as an incarnation of the general approach described in the previous section. This means that we will first reimplement classical propositional logic based on support, and then extend this classical core by adding a new questionforming disjunction connective: as a consequence, InqB will now emerge as a conservative extension of classical propositional logic, CPL.
What this new perspective brings out is that InqB can be seen as adding expressive power to CPL: whereas classical logic can be regarded as a logic of pieces of information, inquisitive logic may be regarded as a logic of information types. In classical propositional logic, propositional formulas are viewed as statements, and thus, as describing specific pieces of information. In InqB, these formulas will be given an interpretation which is isomorphic to the standard one; in this way, the logic of statements will be preserved. However, this classical core will be augmented with questions—indeterminate formulas which describe proper information types. By allowing us to interpret such formulas, the support approach yields a logic that captures interesting logical relations, such as dependency, that are not covered by classical propositional logic.^{12} \({^{,}}\) ^{13}
For proofs of the technical results mentioned in this section, the reader is referred to Ciardelli (2009) and Ciardelli and Roelofsen (2011). Occasionally, proofs are provided for claims which lack a direct analogue in the literature.
3.1 Propositional information states
First, let us see how our informal talk of possible worlds and information states can be made precise in the propositional setting. Given a set \({\mathcal {P}}\) of propositional atoms, we will take a possible world to be a propositional valuation, that is, a function \(w:{\mathcal {P}}\rightarrow \{0,1\}\) which specifies which of the atoms are true. As a consequence, information states will be sets of propositional valuations. The set \(\omega \) containing all valuations represents the trivial state in which no information is present. At the opposite end of the spectrum, the empty set \(\emptyset \) represents the state of inconsistent information; nonempty states will be referred to as consistent states.
3.2 Support semantics for classical propositional logic
Definition 3

\(s\models p\iff w(p)=1\) for all \(w\in s\)

\(s\models \bot \iff s=\emptyset \)

\(s\models \varphi \wedge \psi \iff s\models \varphi \) and \(s\models \psi \)

\(s\models \varphi \rightarrow \psi \iff \) for all \(t\subseteq s\), \(t\models \varphi \) implies \(t\models \psi \)
Keeping in mind that we read support as capturing when a formula is settled in an information state, the clauses may be read as follows. An atom p is settled in s in case it is true at every world in s. The falsum constant \(\bot \) is only settled in the inconsistent state, \(\emptyset \). A conjunction is settled in s in case both conjuncts are. Finally, implication internalizes entailment in the way described in the previous section: an implication is settled in s in case the antecedent entails the consequen relative to s; that is, in case enhancing s so as to settle the antecedent is guaranteed to lead to a state which also settles the consequent.

\(s\models \lnot \varphi \iff \) it is not the case that \(s\between \varphi \)

\(s\models \varphi \vee \psi \iff \) for all consistent \(t\subseteq s\), \(\,t\between \varphi \,\) or \(\,t\between \psi \)
Now we can verify inductively that what we gave is a supportbased formulation of classical propositional logic. Indeed, support conditions are related to standard truth conditions in accordance with Relation 1: a classical formula \(\varphi \in {\mathcal {L}}_c\) is supported by a state s if and only if it is true at every world in s.
Proposition 2
Writing \(\varphi \) for the truthset of \(\varphi \), i.e., the set of valuations at which \(\varphi \) is true, this property can be rewritten as \([\varphi ]=\{\varphi \}^{\downarrow }\). Thus, any classical formula is determinate in the sense of Definition 1, and may thus be regarded as a statement. An immediate consequence of this proposition is that a classical formula always has a unique alternative, which coincides with its truthset. This is illustrated by Fig. 2.
Proposition 2 shows that the supportsemantics we have just given for our classical language is equivalent to the standard truthconditional semantics: the two are interdefinable, and moreover, it is easy to see that they give rise to the same notion of entailment. Thus, what we have provided is simply an alternative semantic foundation for classical propositional logic.
3.3 Adding questions to propositional logic
Definition 4
It is easy to see that the resulting support relation satisfies the persistency property discussed in the previous section: if a formula is supported by a state s, then it remains supported by any enhancement of s. Moreover, support satisfies the empty state property, stating that the inconsistent information state supports any formula whatsover. This is a semantic version of the familiar ex falso quodlibet principle.
Proposition 3

Persistence property: if \(s\models \varphi \) and \(t\subseteq s\), then \(t\models \varphi \)

Empty state property: \(\emptyset \models \varphi \) for all \(\varphi \in {\mathcal {L}}\)
In the previous section, we have identified a fundamental semantic difference between statements and questions: statements are determinate, i.e., admit a singleton generator, while questions are indeterminate, i.e., they only have nonsingleton generators. We can then categorize the formulas of our formal language as being statements or questions according to this characterization.^{15} \(^,\) ^{16}
Definition 5

A formula \(\varphi \in {\mathcal {L}}\) is called a statement iff it is determinate.

A formula \(\varphi \in {\mathcal {L}}\) is called a question iff it is indeterminate.
Henceforth, we take the metavariables \(\alpha ,\beta \) range over statements, \(\mu ,\nu \) range over questions, and \(\varphi ,\psi ,\chi \) range over arbitrary formulas.
It is easy to see that formulas in \({\mathcal {L}}\) are always normal, that is, the set of alternatives for a formula is always a generator for the formula’s supportset.
Proposition 4
(Normality) For all \(\varphi \in {\mathcal {L}}\), \(\;[\varphi ]=\textsc {Alt}(\varphi )^\downarrow \)
This means that we may regard a formula \(\varphi \) in a canonical way as denoting the type of information \(\textsc {Alt}(\varphi )\). This allows us to give a very visual characterization of the classes of statements and questions.
Proposition 5

\(\varphi \) is a statement iff it has a unique alternative.

\(\varphi \) is a question iff it has two or more alternatives.
Let us first focus on the class of statements. An interesting observation is that statements may be characterized as formulas whose semantics is completely determined at the level of singleton states.
Proposition 6
We may generalize the notion of truth from classical formulas to the whole language \({\mathcal {L}}\) by defining it in terms of support at singleton states: \(\varphi \) is true at w if it is supported at \(\{w\}\). Then, the previous proposition says that statements are precisely, that is, those formulas whose semantics is completely determined in terms of truth conditions.
Next, recall that Proposition 2 guarantees that any classical formula is a statement. Conversely, any statement is equivalent to a classical formula, which shows that, by adding Open image in new window to CPL, we are enabling our logic to express questions, but not to express new statements.^{17} To prove this, we can first associate with any formula a corresponding classical formula.
Definition 6
(Classical variant of a formula) The classical variant \(\varphi ^{cl}\) of a formula \(\varphi \) is obtained from \(\varphi \) by replacing all occurrences of inquisitive disjunction by classical disjunction.
Now, for any formula \(\varphi \), its classical variant \(\varphi ^{cl}\) is a classical formula having as its unique alternative the union of all the alternatives for \(\varphi \).
Proposition 7
For any \(\varphi \), \(\textsc {Alt}(\varphi ^{cl})=\{\bigcup \textsc {Alt}(\varphi )\}\).
It follows from this proposition that a formula \(\varphi \) is a statement iff it is equivalent to its classical variant \(\varphi ^{cl}\). As a consequence, we get the following corollary.
Corollary 1
Any statement is equivalent to a classical formula.
Another important observation is that, as a consequence of the semantic clause for negation, \(\lnot \varphi \) is always a statement. In particular, the double negation of a formula is always a statement, which is equivalent to the classical variant of the formula.
Proposition 8
\(\lnot \lnot \varphi \equiv \varphi ^{cl}\)
As a consequence, statements can also be characterized as being precisely those formulas which are equivalent to their own double negation. In other words, the double negation law is the hallmark of statements.
Proposition 9
\(\varphi \equiv \lnot \lnot \varphi \iff \varphi \) is a statement.
Let us now turn our attention to questions. First, notice that, if \(\alpha \in {\mathcal {L}}_{c}\), the polar question whether \(\varphi \), which can be settled either by establishing \(\alpha \), or by establishing \(\lnot \alpha \), can be expressed by means of inquisitive disjunction as Open image in new window . It will be convenient to abbreviate this formula as \(?\alpha \).
Definition 7
(Question mark operator) Open image in new window
An attractive feature of the system InqB is the following: since the semantics of the connectives \(\wedge \) and \(\rightarrow \) is given in terms of support, these connectives can be used to combine not only statements, but also questions. In this way, the standard truthconditional operations of conjunction and implication are extended to questions in a natural way. To see the effect of these operators when applied to questions, consider first conjunction: applying \(\wedge \) to two polar questions, such as ?p and ?q, results in a question \({?p}\wedge {?q}\) which is settled whenever both conjuncts are settled, as illustrated in Fig. 3c.
 1.
\((p\rightarrow q)\wedge (\lnot p\rightarrow q)\equiv {q}\)
 2.
\((p\rightarrow q)\wedge (\lnot p\rightarrow \lnot q)\equiv q\leftrightarrow p\)
 3.
\((p\rightarrow \lnot q)\wedge (\lnot p\rightarrow q)\equiv q\leftrightarrow \lnot p\)
 4.
\((p\rightarrow \lnot q)\wedge (\lnot p\rightarrow \lnot q)\equiv \lnot q\)
3.4 Resolutions and inquisitive normal form
An important feature of the system InqB is that we can compute, recursively on the structure of a formula \(\varphi \), a set of classical formulas which can be taken to name the different pieces of information of type \(\varphi \). We refer to these formulas as the resolutions of \(\varphi \).
Definition 8

\({\mathcal {R}}(p)=\{p\}\)

\({\mathcal {R}}(\bot )=\{\bot \}\)

\({\mathcal {R}}(\varphi \wedge \psi )=\{\alpha \wedge \beta \,\,\alpha \in {\mathcal {R}}(\varphi )\text { and }\beta \in {\mathcal {R}}(\psi )\}\)

\({\mathcal {R}}(\varphi \rightarrow \psi )=\{\bigwedge _{\alpha \in {\mathcal {R}}(\varphi )}(\alpha \rightarrow f(\alpha ))\,\,f:{\mathcal {R}}(\varphi )\rightarrow {\mathcal {R}}(\psi )\}\)
Notice that resolutions are by definition classical formulas. Moreover, it is easy to show by induction that any classical formula is the only resolution of itself.
Proposition 10
If \(\alpha \in {\mathcal {L}}_c\), then \({\mathcal {R}}(\alpha )=\{\alpha \}\).
On the other hand, questions always have multiple resolutions: for instance, we have \({\mathcal {R}}({?p})=\{p,\lnot p\}\), and \({\mathcal {R}}(p\rightarrow {?q})=\{p\rightarrow q,\, p\rightarrow \lnot q\}\).
The key property of resolutions is given by the following Proposition: to settle the formula \(\varphi \) is to establish that \(\alpha \) is true, for some resolution \(\alpha \) of \(\varphi \).
Proposition 11
Moreover, as a corollary of the above proposition we have the following normal form result for InqB, which shows that any formula is equivalent to an inquisitive disjunction of classical formulas.
Proposition 12
(Inquisitive normal form) Let \(\varphi \in {\mathcal {L}}\) and let \({\mathcal {R}}(\varphi )=\{\alpha _1,\dots ,\alpha _n\}\). Then, Open image in new window
It is interesting to remark that there is a close similarity between the inductive definition of resolutions that we gave, and the inductive definition of proofs in the Brouwer–Heyting–Kolmogorov (BHK) interpretation of intuitionistic logic. In this interpretation, a proof of a conjunction is a pair of two proofs, one for each conjunct; a proof of a disjunction is a proof of either disjunct; and a proof of an implication is a function that turns any proof of the antecedent into a proof of the consequent. Similarly, here a resolution of a conjunction is a conjunction of two resolutions, one for each conjunct; a resolution of an inquisitive disjunction is a resolution of either disjunct; and a resolution of an implication corresponds to a function from resolutions of the antecedent to resolutions of the consequent. The main difference between the two notions is that, unlike proofs in the BHK interpretation, resolutions are in turn formulas, that is, syntactic objects within the same language in which the original formula lives. Thus, we can look at the definition of resolutions as a sort of languageinternal version of the BHK interpretation.
By means of the notion of resolutions we can also restate the support conditions for an implication in an interesting way. To spell this out, we will introduce the notion of a dependence function.
Definition 9

A function \(f:{\mathcal {R}}(\varphi )\rightarrow {\mathcal {R}}(\psi )\) is called a dependence function from \(\varphi \) to \(\psi \) in a context s, notation \(f:\varphi \leadsto _s\psi \), in case for any \(\alpha \in {\mathcal {R}}(\varphi )\), \(\alpha \models _s f(\alpha )\).

A function \(f:{\mathcal {R}}(\varphi )\rightarrow {\mathcal {R}}(\psi )\) is called a logical dependence function from \(\varphi \) to \(\psi \), notation \(f:\varphi \leadsto \psi \), if it is a dependence function in any context.
Proposition 13
Let \(f:{\mathcal {R}}(\varphi )\rightarrow {\mathcal {R}}(\psi )\). For any state s, \(\;s\models \gamma _f\iff f:\varphi \leadsto _s\psi \)
Now, Proposition 12 tells us that \(\varphi \rightarrow \psi \) is supported in a state s in case some formula \(\gamma _f\in {\mathcal {R}}(\varphi \rightarrow \psi )\) is supported. By the previous proposition, this holds if and only if there exists a dependence function \(f:\varphi \leadsto _{s}\psi \). We have thus obtained the following result about the support conditions for an implication.
Proposition 14
(Implication and dependence functions) \(s\models \varphi \rightarrow \psi \iff \) there exists some \(f:{\varphi \leadsto _s\psi }\)
This shows that a state supports an implication \(\varphi \rightarrow \psi \) iff it admits a dependence function form \(\varphi \) to \(\psi \), i.e., if there exists a systematic way to use the information available in s to infer from any given resolution of \(\varphi \) a corresponding resolution of \(\psi \).
3.5 Entailment and propositional dependencies
Now that we have set up a logical system encompassing both statements and questions, let us take a look at the relation of entailment which arises from it. As we expect, on the classical fragment of the language, this relation coincides with truthconditional entailment in classical propositional logic.
Proposition 15
(Entailment among classical formulas is classical) Let \(\varGamma \cup \{\alpha \}\subseteq {\mathcal {L}}_c\). Then \(\varGamma \models \alpha \iff \varGamma \) entails \(\alpha \) in CPL.
In this precise sense, InqB is a conservative extension of classical propositional logic. This fact shows that nothing is lost in the move from CPL to InqB: anything that could be formalized in classical propositional logic can still be formalized in exactly the same way in InqB.^{21} On the other hand, more things can be formalized in InqB than in CPL, since now we can also look at relations of entailment which involve questions.
Let us examine the various ways in which questions can participate in an entailment relation. First, recall that an entailment \(\alpha \models \mu \) from a statement to a question holds if \(\alpha \) logically resolves \(\mu \). As an illustration, we have \(p\wedge q\models {?p}\), but \(p\vee q\not \models {?p}\): the question ?p is resolved by the by the statement \(p\wedge q\), but not by the by the statement \(p\vee q\).
The following proposition says that a statement entails an inquisitive disjunction if and only if it entails a specific one of the disjuncts. This holds not only for logical entailment, but more generally for entailment relative to an arbitrary context. The purely logical case is obtained by setting \(s=\omega \).
Proposition 16
(Split property) Open image in new window or \(\alpha \models _s\psi \).
Notice that by setting \(\alpha =\top \) we obtain that InqB has the disjunction property for Open image in new window : whenever Open image in new window is logically valid, either \(\varphi \) or \(\psi \) must be valid as well. Also, notice that combining the Split Property with the normal form result given by Proposition 12, we obtain the following corollary.
Corollary 2
\(\alpha \models _s\mu \iff \alpha \models _s\beta \) for some \(\beta \in {\mathcal {R}}(\mu )\)
What this corollary says is that in any context s, a statement \(\alpha \) resolves a question \(\mu \) if and only if it entails some specific resolution of \(\mu \).
Let us now consider an entailment \(\mu \models \alpha \) from a question to a statement. We said that such an entailment captures the fact that \(\mu \) logically presupposes \(\alpha \), i.e., that \(\mu \) can only be resolved provided \(\alpha \) is true. As an illustration, we have Open image in new window , but \({?p}\,\not \models p\vee q\): the statement \(p\vee q\) is logically presupposed by the question Open image in new window , since this question can only be truthfully resolved provided one of p and q is indeed true; but \(p\vee q\) is not presupposed by the question ?p, since ?p can be truthfully resolved even in worlds where \(p\vee q\) is false.
The following proposition shows that \(\alpha \) is entailed by \(\mu \) iff it is entailed by the classical disjunction \(\bigvee {\mathcal {R}}(\mu )\) of the resolutions to \(\mu \), which may be seen as capturing the question’s presupposition.
Proposition 17
\(\mu \models _s\alpha \iff \bigvee {\mathcal {R}}(\mu )\models _s\alpha \)

\(s_1\): the patient has symptom \(S_1\);

\(s_2\): the patient has symptom \(S_2\);

\(\,g\;\): the patient is in good physical condition;

\(\;t\;\): the treatment is prescribed.
In the next section we are going to see that the connection between entailment and dependency has a prooftheoretic counterpart: since entailments involving questions capture dependencies, by making inferences with questions we can provide formal proofs of dependencies; moreover, a proof of a dependency always has an interesting kind of constructive content, namely, it encodes an algorithm whereby the dependency can be effectively computed.
4 Reasoning with questions
4.1 A natural deduction system for InqB
In this subsection, a sound and complete proof system for InqB is described. Unlike the systems provided by Ciardelli and Roelofsen (2011), which are Hilbertstyle, here we will work with a natural deduction system. This allows for more insightful formal proofs, providing a better grasp of the significance of reasoning with questions. Since it is straightforward to adapt the techniques in Ciardelli and Roelofsen (2011) to this system, we will not provide a proof of completeness. Instead, we will focus on an aspect which is not discussed in previous work: the conceptual significance of the inference rules, and the content of inquisitive proofs as a whole.
The inference rules of the system are listed in Fig. 4, where the variables \(\varphi ,\psi ,\) and \(\chi \) range over all formulas, while \(\alpha \) is restricted to classical formulas. As customary, we refer to the introduction rule for a connective \(\circ \) as \((\circ \textsf {i})\), and to the elimination rule as \((\circ \textsf {e})\). We write \(P:\varPhi \vdash \psi \) to mean that P is a proof whose set of undischarged assumptions is included in \(\varPhi \) and whose conclusion is \(\psi \), and we write \(\varPhi \vdash \psi \) to mean that a proof \(P:\varPhi \vdash \psi \) exists. Finally, we say that two formulas \(\varphi \) and \(\psi \) are provably equivalent, notation \(\varphi \dashv \vdash \psi \), in case \(\varphi \vdash \psi \) and \(\psi \vdash \varphi \). Let us comment briefly on each of the rules of this system.
4.1.1 Conjunction
Conjunction is governed by the standard inference rules. The soundness of these rules corresponds to the following feature of conjunction in InqB: a set of assumptions entails a conjunction iff it entails both conjuncts.
Proposition 18
\(\varPhi \models \varphi \wedge \psi \iff \varPhi \models \varphi \text { and }\varPhi \models \psi \)
These rules are not restricted to classical formulas: conjunctive questions like \({?p}\wedge { ?q}\) can be handled in inferences just like standard conjunctions.
4.1.2 Implication
Implication is also governed by the standard inference rules. The soundness of these rules corresponds to the following proposition, which captures the tight relation existing between implication and entailment.
Proposition 19
\(\varPhi \models \varphi \rightarrow \psi \iff \varPhi ,\varphi \models \psi \)
Again, these rules are not restricted to classical formulas: implications involving questions (including implications which capture dependencies, like \({?p}\rightarrow {?q}\)) can also be handled by means of the standard implication rules.
4.1.3 Falsum
As usual, \(\bot \) has no introduction rule, and can be eliminated to infer any formula. This corresponds to the fact that we have \(\bot \models \varphi \) for all formulas \(\varphi \), which in turn is a consequence of the fact that the inconsistent state \(\emptyset \) supports every formula.
4.1.4 Negation
Since \(\lnot \varphi \) is defined as \(\varphi \rightarrow \bot \), the usual intuitionistic rules for negation, given in Fig. 5, follow as particular cases of the rules for implication.
4.1.5 Inquisitive disjunction
Inquisitive disjunction is governed by the standard by the standard inference rules rules for disjunction. The soundness of these rules corresponds to the following fact, which follows from the support clause for Open image in new window .
Proposition 20
Open image in new window and \(\,\varPhi ,\psi \models \chi \).
4.1.6 Classical disjunction
4.1.7 Double negation elimination
We saw in the previous section that the double negation law is characteristic of statements (Proposition 9). By allowing double negation elimination for all classical formulas, we are encoding the fact that all classical formulas in InqB are statements—and thus obey classical logic.
Notice that having this rule for all classical formulas means that our system is an extension of a standard natural deduction system for classical logic (as given, e.g., in Gamut 1991). This ensures that any natural deduction proof in classical logic is also a proof in our system.
4.1.8 Split
The only nonstandard ingredient of our system is the Open image in new window split rule, which distributes a classical antecedent over an inquisitive disjunction. This rule encodes the Split Property of Proposition 16, repeated here.
Proposition 21
(Split Property) Open image in new window
Indeed, by the connection between entailment in context and implication, the split property could be restated as follows: for any state s, if Open image in new window then \(s\models \alpha \rightarrow \varphi \text { or }s\models \alpha \rightarrow \psi \). In turn, by the supportclause for inquisitive disjunction, this amounts to Open image in new window , i.e., precisely to the validity of the Open image in new window split rule. Thus, we may regard the Open image in new window split rule as encoding the following fundamental feature of our logic: in any given context, if a statement resolves a question, it must resolve it in a particular way.^{22}
4.2 Inquisitive proofs and their constructive content
It is instructive to consider what argument is encoded by this proof. In words, this may be phrased roughly as follows. We are assuming information of type \(?s_2\). This means that we have either the information that \(s_2\), or the information that \(\lnot s_2\). If we have the information that \(s_2\), then by combining this information with \(\gamma \) we can infer t, and so we have some information of type ?t. On the other hand, if we have the information that \(\lnot s_2\), we have to rely on having information of type \(?s_1\). This means that we have either the information that \(s_1\), or the information that \(\lnot s_1\). If the information we have is \(\lnot s_1\), then by combining this with \(\lnot s_2\) and \(\gamma \) we can infer \(\lnot t\), and thus we have some information of type ?t. On the other hand, if the information we have is that \(s_1\), then we have to rely on having information of type ?g. Again, there are two possibilities: if the information we have is g, then by combining this with \(s_1\) and \(\gamma \) we can infer t, and so we have information of type ?t; if the information we have is \(\lnot g\), then by combining this with \(\lnot s_2\) and \(\gamma \) we can infer \(\lnot t\), and thus again we have information of type ?t. So, in any case, under the given assumptions we are assured to have information of type ?t.^{24}
This is not an accident, but a manifestation of a general fact concerning inquisitive proofs: given a proof P which witnesses a dependency, we can always see this proof as encoding a program that computes the dependency. To state this fact in a precise way, let us write \(\overline{\varphi }\) for a sequence \(\varphi _1,\dots ,\varphi _n\) of formulas, and \(\overline{\alpha }\in {\mathcal {R}}(\overline{\varphi })\) to mean that \(\overline{\alpha }\) is a sequence \(\alpha _1,\dots ,\alpha _n\) such that \(\alpha _i\in {\mathcal {R}}(\varphi _i)\). Then, we have the following theorem.
Theorem 1
(Existence of a resolution algorithm) Let \(P:\overline{\varphi }\vdash \psi \) and let \(\overline{\alpha }\in {\mathcal {R}}(\overline{\varphi })\). There is a procedure which, inductively on P, constructs a proof \(\,F_P(\overline{\alpha }):\overline{\alpha }\vdash \beta \) having as conclusion a resolution \(\beta \in {\mathcal {R}}(\psi )\).
The proof of this theorem is given in the appendix, where we explicitly describe how to construct the desired proof \(F_P(\overline{\alpha })\) inductively on P. We will refer to this inductive procedure as the resolution algorithm, and we will refer to \(F_P(\overline{\alpha })\) as the resolution of the proof P on input \(\overline{\alpha }\). The idea of the resolution algorithm is illustrated in Fig. 6.
The existence of this procedure shows that an inquisitive proof may be regarded as a template for classical proofs, where questions serve as placeholders for arbitrary information of the corresponding type. As soon as the indeterminate assumptions of the proof are instantiated to particular resolutions—say, as soon as we input the data relative to a specific patient—the template can be instantiated to a proof in classical logic, which infers some corresponding resolution of the conclusion—in our case, a deliberation about the treatment.
To sum up, then, a proof \(P:\overline{\varphi }\vdash \psi \) in inquisitive logic can always be seen as encoding a program to turn each resolution of the set \(\overline{\varphi }\) of assumptions into a corresponding resolution of the conclusion \(\psi \): given resolutions \(\overline{\alpha }\in {\mathcal {R}}(\overline{\varphi })\), we can use the proof P to compute a corresponding resolution \(f(\overline{\alpha })\in {\mathcal {R}}(\psi )\) which follows from \(\overline{\alpha }\): for this, it suffices to let \(f_P(\overline{\alpha })\) be the conclusion of \(F_P(\overline{\alpha })\). In other words, from a proof of a dependency we can always extract a logical dependence function logical dependence function \(f_P:\overline{\varphi }\leadsto \psi \).^{25}
4.3 On the role of questions in inference
Absolutely the wrong thing is to think [the logic of questions] is a logic in the sense of a deductive system, since one would then be driven to the pointless task of inventing an inferential scheme in which questions, or interrogatives, could serve as premises and conclusions.
What we hope to have achieved in this section is to show that Belnap and Steel were too pessimistic: not only is it possible to give a deductive system in which questions serve as premisses and conclusions, and a logically wellbehaved one at that; but also, proofs in such a system are meaningful and worthy of investigation.
For one thing, we saw in the previous sections that entailments involving questions capture interesting logical relations. This, in itself, would suffice to grant interest in a syntactic calculus that tracks this generalized notion of entailment. However, in this section we have seen that the role of question in proofs goes beyond this: inferences involving questions are themselves interesting logical objects, which capture meaningful arguments.
In a nutshell, what we found is that questions make it possible to perform inferences with information which is not fully specified. To appreciate this point, it might be useful to draw a connection with the constants used for arbitrary individuals in natural deduction systems for standard firstorder logic.^{26} For instance, in order to infer \(\psi \) from \(\exists x\varphi (x)\), one can make a new assumption \(\varphi (c)\), where c is fresh in the proof and not occurring in \(\psi \), and then try to derive \(\psi \) from this assumption. Here, the idea is that c stands for an arbitrary object in the extension of \(\varphi (x)\). If \(\psi \) can be inferred from \(\varphi (c)\), then it must follow no matter which specific object “of type \(\varphi (x)\)” the constant c denotes, and thus it must follow from the mere existence of such an object. Questions allow us to do something similar, except that instead of an arbitrary individual, a question stands for an arbitrary piece of information of the corresponding type. For instance, the question what the patient’s symptoms are may be viewed as a placeholder standing for an arbitrary specification of the patient’s symptoms.
When assuming a question \(\mu \), what we are supposing is some indeterminate piece of information of type \(\mu \). Thus, e.g., by assuming the question what the patient’s symptoms are, we are supposing to be given a complete specification of the patient’s symptoms. We are not assuming anything specific about what these symptoms are—say, that the patient has only symptom \(S_1\); we are merely assuming some information of this type.
Similarly, consider the move of drawing a conclusion. In concluding a question \(\mu \), what we are establishing is that, under the given assumptions, we are guaranteed to have some information of type \(\mu \)—though precisely what information this is will in general depend on what specific information instantiates the indeterminate assumptions under which the conclusion \(\mu \) was drawn.
Summing up, then, questions may be used in logical inferences as placeholders for arbitrary information of the corresponding type. As we saw, by manipulating such placeholders it is possible to construct logical proofs that witness the existence of certain dependence relations between information types. Thus, far from being meaningless from a prooftheoretic perspective, questions turn out to be extremely interesting tools for logical inference.
5 Relation with previous work
5.1 Non entailmentdirected approaches to questions
Throughout most of the history of logic, virtually no attention has been paid to questions. It is not until the second half of the 20th century that logical works devoted to questions have started to appear. In most of these works (e.g. Åqvist 1965; Harrah 1961, 1963; Belnap and Steel 1976; Tichy 1978) the emphasis has been on providing a logical language for questions, and on characterizing the relation of answerhood between statements and questions. Other approaches have focused instead on the role of questions in processes of inquiry, either modeling inquiry itself as a sequence of questioning moves and inference moves, as in the interrogative model of inquiry of Hintikka (1999), or characterizing how questions are arrived at in an inquiry scenario, as in the inferential erotetic logic of Wiśniewski (1995).^{27} What all these theories have is common is the assumption that dealing with questions requires turning to relations other than logical entailment. Thus, they pursue enterprises which, while related, are also different in an important respect from the one that we have been concerned with here: incorporating questions on a par with statements in the very relation of entailment, and characterizing how they can be manipulated in entailmenttracking logical proofs.
5.2 The Logic of Interrogation
In Groenendijk (1999), this approach is applied to a particular logical language, which is an extension of firstorder predicate logic with questions. This gives rise to an interesting combined logic of statements and questions, which was investigated and axiomatized by ten Cate and Shan (2007).
Definition 10
(Partition questions) \(\mu \) is a partition question if any world is contained in a unique alternative for \(\mu \).
It is easy to see that such questions are not partition questions. Consider for example (3a): as illustrated by Fig. 7, the alternatives for this question correspond to the possible witnesses for the property of being a typical French name. In a given world w, we may of course have several witnesses for this property, which means that w is contained in several alternatives for the question. This shows that a question like (3a) is not a partition question, and thus it is not interpretable in LoI. On the other hand, since it is clear what information is needed in order for (3a) to be settled, the inquisitive approach has no problem interpreting this question. Since mentionsome questions are a broad and practically relevant class of questions, this is a significant advantage of support semantics over the LoI approach.
Such questions, too, cannot be adequately represented in the LoI framework. Starting precisely with the problem of conditional questions, the pursuit of greater generality lead Velissaratou (2000), Groenendijk (2009) and Mascarenhas (2009) to relax the constraints of the LoI framework, interpreting sentences by means of binary relations that are not necessarily transitive. This lead to a first version of inquisitive semantics, now referred to as pair semantics. While Groenendijk (2011) showed that the pair semantics can indeed deal adequately with conditional questions, Ciardelli (2008, (2009), and later Ciardelli et al. (2015) argued that no pair semantics provides a satisfactory general framework for questions, and that an interpretation based on information states is needed instead, leading to the supportbased approach that we discussed here.
5.3 Nelken and Shan’s modal approach
After the Logic of Interrogation, a different uniform approach to statements and questions was proposed by Nelken and Shan (2006). In this approach, questions are translated as modal sentences, and they are interpreted by means of truth conditions: a question is true at a world w in case it is settled by an information state R[w] associated with the world (i.e., the set of successors given by an accessibility relation R). Thus, for instance, Nelken and Shan render the question whether p by the modal formula \(?p:=\Box p\vee \Box \lnot p\).
In one respect, this approach is similar to the approach proposed in this paper, since the meaning of a question is taken to be encoded by the conditions under which the question is settled by a relevant body of information. And indeed, if we consider entailments which involve only questions, the approach of Nelken and Shan makes the expected predictions. However, an asymmetry between statements and questions is maintained in this approach: for questions, what matters is whether they are settled by a relevant information state, while for statements, what matters is whether they are true at the world of evaluation. This asymmetry creates problems the moment we start considering cases of entailment involving both statements and questions, such as the one corresponding to our protocol example. It is easy to see that, if such entailments are to be meaningful at all, entailment cannot just amount to preservation of truth. Nelken and Shan propose to fix this by redefining entailment as modal consequence: \(\varphi \models \psi \) if, whenever \(\varphi \) is true at every possible world in a model, so is \(\psi \). However, this move has the odd consequence of changing the consequence relation for statements in an undesirable way. For instance, if our declarative language indeed contains a Kripke modality, say a knowledge modality K, then if our notion of entailment is redefined as modal consequence, we make undesirable predictions, such as \(p\models Kp\). Thus, this approach does not really allow us to extend classical logic with questions in a conservative way.^{28}
5.4 The modal translation of InqB
5.4.1 Parsimony
First of all, the modal approach is unnecessarily redundant. In this approach, a formula is evaluated at a world w equipped with an information state R[w]. However, it is clear that the evaluation world w is completely unnecessary: it is only the content of the information state R[w] that matters for the satisfaction of a formula \(\varphi ^\Box \). But if it is only the content of a certain information state that matters, we can evaluate a formula directly with respect to that information state, without invoking a specific world of evaluation. This move allows for a significant simplification of our semantic structures: we no longer need an accessibility relation R, whose unique purpose was to anchor the relevant state to a specific world.
5.4.2 Insight
By uncovering the connection between dependency and entailment, the present approach provides an insight that is missing in the modal approach. This insight also has practical consequences, since it allows us to use ideas and techniques of logic in the analysis of the dependencies. For instance, since entailment can be generally internalized in the language by means of implication, dependencies can be expressed as implications between questions. This provides a wellbehaved logical representation of dependencies, and suggests natural rules for reasoning with them. As an example of the explanatory power of the approach, this perspective shows that the wellknown Armstrong’s axioms for dependency used in database theory are nothing but the familiar intuitionistic rules for implication in disguise (a point first made by Abramsky and Väänänen 2009).
5.4.3 Logical operations
In inquisitive logic, the interpretation of these sentences can be obtained in a simple, compositional way. If we translate (5a) as p and (5b) as q, then we can translate (5c) as ?q, (5d) as \(p\rightarrow q\), and (5e) as \(p\rightarrow {?q}\). Notice that one and the same operator is at play in (5d) and (5e): this operator has a uniform semantics, a simple algebraic characterization, and a natural prooftheory.
In the modal approach, the translation of (5a) is \(\Box p\), and the translation of (5b) is \(\Box q\). The translation of (5c) is \(\Box p\vee \Box \lnot p\). The translation of (5d) is not \(\Box p\rightarrow \Box q\), as would be expected, but rather \(\Box (p\rightarrow q)\); similarly, the translation of (5e) is not \(\Box p\rightarrow (\Box q\vee \Box \lnot q)\), but rather \(\Box (p\rightarrow q)\vee \Box (p\rightarrow \lnot q)\).
Although modal logic does have an implication, this cannot be used to interpret the conditional construction. More importantly, in this approach, it is not clear that there is any structural similarity between (5d) and (5e), nor that there is a fundamental relation between these two sentences and the simpler sentences (5ac). Clearly, some important piece of structure—in the case in point, the existence of a neat implication operation—is being missed from the modal perspective.
5.4.4 Inferences and computational interpretation of proofs
We saw in Sect. 4 that inquisitive logic allows us to manipulate questions in inference by means of simple and familiar logical rules. By using questions, we can then provide formal proofs of dependencies. Moreover, we saw that such proofs have a computational interpretation, encoding algorithms to compute the dependency at hand. It is not clear that the modal approach has an equally attractive framework to offer. First, it would require us to reason with a more complex language, including modalities in addition to just connectives (or, in addition to whatever other logical constants the language includes). Second, it is not clear whether a general constructive interpretation of proofs exists in this approach.
5.5 Dependence logic
The ideas discussed in this chapter are also deeply connected with the investigations undertaken in recent years within the framework of Dependence Logic (Väänänen 2007). Indeed, the dependencies considered in dependence logic are special instances of question entailment. In particular, the dependence atoms \(\,=(p_1,\dots ,p_n,q)\,\) of propositional dependence logic (Väänänen 2008; Yang 2014) capture the dependency of the atomic polar question ?q on the atomic polar questions \(?p_1,\dots ,?p_n\). As a consequence, in our language they may be expressed as \({?p_1}\wedge \dots \wedge {?p_n}\rightarrow {?q}\). This yields a decomposition of these atoms into more basic and betterbehaved operations—which allows for a natural prooftheory. While the possibility of such a decomposition was noted by Abramsky and Väänänen (2009), the present work casts new light on this connection in several ways. First, we can now see that this decomposition reflects a fundamental connection between dependencies and questions: a dependency is a case of entailment having questions as its protagonists; since entailments can be internalized as implications, dependencies can be expressed as implications between questions. Second, it becomes clear that dependence atoms capture only a special case of a more general phenomenon: dependencies may involve all sorts of questions other than atomic polar questions, and implication gives us a fully general way to express them. Third, as we have seen, the connection between questions and dependencies has a prooftheoretic side to it: dependencies may be formally proved to hold in a system equipped with questions; and moreover, the resulting proofs do not just witness dependencies but actually encode specific dependence functions.
The relation between inquisitive logic and dependence logic is the subject of a separate paper (Ciardelli 2016), which develops these points in detail, and shows how they carry over to the setting of firstorder logic.
5.6 Previous work on inquisitive semantics
Finally, within the landscape of recent work on inquisitive semantics (among others, Ciardelli et al. 2013a, 2015; Roelofsen 2013; Ciardelli and Roelofsen 2015; Groenendijk and Roelofsen 2013; Punčochář 2015a, b), the contribution of the present paper is threefold. In the first place, we have shown that propositional inquisitive logic may be regarded as a conservative extension of classical propositional logic with a question operator, and we saw that this perspective sheds new light on some logical features of the system. Secondly, we have investigated the role of questions in logical inferences, and we have established a new result, Theorem 1, which brings out the computational content of inquisitive proofs. Thirdly, and most importantly, while work on inquisitive semantics has so far been mainly driven by motivations stemming from linguistics and philosophy of language, we have argued that inquisitive semantics also has solid motivations stemming entirely from within the field of logic. As we saw, taking questions into account broadens the scope of classical logic in an exciting way, bringing within reach an elegant account of the logical relation of dependency.
6 Conclusion and further work
In this paper we have seen that, by moving from a truthbased view of meaning to an informationbased view, we obtain a uniform semantic framework for statements and questions. This allows for a substantial generalization of the fundamental notions of classical logic. In particular, while classical logic is concerned with the relation of logical consequence, which relates specific pieces of information, the presence of question allows us to also capture also the relation of logical dependency, which connects different information types, and which plays an important role in a broad range of different contexts.
Additionally, we saw that questions have a role to play in logical proofs. By using questions, we can manipulate indeterminate information, that is, information which is not fully specified, such as what the symptoms are or whether the treatment is prescribed. This allows us to formally prove that a certain dependency holds within a certain context. Moreover, we saw that, at least in the propositional setting, from such a proof we can extract an algorithm that computes this dependency, i.e., that turns information of the type described by the assumptions into information of the type described by the conclusion.
In this paper, we focused on the fundamental ideas of the inquisitive approach, and on the generalized view of logic to which they give rise. Now that the significance of inquisitive logic and its relevance for applications become clearer, however, many technical questions also become more urgent. One class of questions is prooftheoretical: e.g., does the naturaldeduction system introduced above admit a normalization theorem? If not, can inquisitive logic be regimented in a betterbehaved proof system? The labeled sequent calculus developed by Sano (2009) for a related logic provides a starting point for an alternative approach. Other interesting questions concern the computational properties of the resolution algorithm, as well as the complexity of the problem of deciding if a given entailment holds in InqB.
A further question is whether an interpretation of the kind discussed here is available for the extension of InqB proposed and axiomatized by Punčochář (2015b). In this extension, the system is expanded with operators that yield nonpersistent meanings. The resulting language includes not only formulas like p and ?p, which are supported if certain information is available, but also formulas like \({\sim }p\), which are supported if certain information is lacking. Understanding the role of such formulas in a logic of information and the properties of the resulting system is an interesting task for future work.
An axiomatization of inquisitive predicate logic, or a suitable fragment thereof, would provide the means to reason about dependencies between such questions, thus covering a broad spectrum of interesting informational scenarios.
Finally, an interesting task is to explore the repercussions of the new logical perspective on dependency described in this paper for specific fields in which this relation plays a role, such as database theory. One interesting observation we mentioned is that, given that dependencies can generally be expressed as implications among questions, the famous Armstrong axioms used for reasoning about dependencies in database theory (Armstrong 1974) turn out to be simply particular cases of the standard inference rules for implication; this illustrates how inquisitive logics might provide a general and logically transparent environment for reasoning about database dependencies. In this respect, the fact that proofs of dependencies have a computational interpretation seems of particular interest—especially if this should turn out to be the case also for firstorder inquisitive logic, or interesting fragments thereof. It is also worth noting that while stateoftheart techniques for optimizing query answering in databases, such as the notion of view determinacy (Segoufin and Vianu 2005) focus on partition questions, it seems that mentionsome questions like those in might also be interesting from the perspective of a query language. Thus, an axiomatization of fragments of firstorder inquisitive logic might also provide useful tools to extend the methods currently used to optimize query answering to a broader class of queries.
Footnotes
 1.
This use of the word dependency is quite different from the ordinary sense of the word. If we have a dependency of a question \(\nu \) on another question \(\mu \), then this means that \(\nu \) is completely, and not only partially, determined by \(\mu \). Determinacy would probably be a better term for this notion, but we stick to dependency for the sake of consistency with the existing literature.
 2.
Throughout this section, we use the terms statement and question in their ordinary, pretheoretical sense. Thus, e.g., “the patient has symptom \(S_1\)” is a statement, while “whether the patient has symptom \(S_1\)” and “what symptoms the patient has” are questions. Later on, when we will work with a formal language, a precise definition of statements and questions will be provided, based on a fundamental semantic difference that we will identify between statements and questions in the ordinary sense.
 3.
The exact nature of possible worlds depends on the specific logical framework. Usually, a possible world may be identified with a model for the language at stake. In intensional logics, which aim at representing a whole variety of states of affairs in a single model, possible worlds are internalized as particular entities within the model. We leave this notion unspecified in this section, since we want to abstract away from the details of a specific logical framework.
 4.
Informationoriented semantics have been considered in the literature, especially as a starting point for nonclassical logics (e.g., Beth 1956; Kripke 1965; Veltman 1981), but sometimes also as alternative foundations for classical logics (e.g., Fine 1975; Humberstone 1981; van Benthem 1986; Holliday 2014). As far as the treatment of statements is concerned, our approach will be very similar to the ones in the latter tradition, modulo a basic difference in the modeling of information states. To the best of my knowledge, however, no previous attempt has been made to use such a semantic foundation to bring questions into play in logic. Within the context of inquisitive semantics, the move from worlds to information states as points of evaluation is also discussed in some detail in Groenendijk (2011), which is a source of inspiration for the present paper.
 5.
A reviewer worries that, by characterizing entailment in terms of support, we are effectively redefining this notion. In a sense, this is obviously so: in order to render the relation of entailment more widely applicable, we look for a new characterization of it which is meaningful for a broader class of sentences. However, what we have just established is that this alternative characterization coincides exactly with the standard one as far as the latter reaches—but, as we will see shortly, it extends beyond it. Notice that having multiple semantic characterization of one and the same logical relation is the norm in logic. Think of entailment in intuitionistic logic, which can be characterized by means of prooftheoretic semantics (the formalized BHK interpretation), Kripke semantics, sheaf semantics, topological semantics, algebraic semantics, etc. (see Troelstra and van Dalen 1988a, b). Different semantic characterizations of a logic can of course have different merits. As we will see in the next section, one merit of characterizing classical logic by means of support semantics, rather than by means of truthconditional semantics, is the fact that the former approach, unlike the latter, extends naturally to questions.
 6.
At this stage, this may be taken as a stipulation about what it means for a sentence to be settled: a sentence is settled by virtue of certain information being available in a state; if \(t\subseteq s\), all the information which is available in s is also available in t, and so, t cannot fail to support a sentence if s does. Given a specific logical system based on support semantics, such as the one described in Sect. 3, this property may then be proved as a fact.
 7.
In algebraic jargon, the meaning of a statement is always a principal downset of the space of information states ordered by \(\subseteq \)
 8.
In the formal system to be introduced in the next section, we will in fact use determinacy and indeterminacy as the defining features of statements and questions, respectively.
 9.
Nonnormal sentences are found in systems of firstorder inquisitive logic, as was first observed by Ciardelli (2009). The firstorder systems in Sect. 6 of Ciardelli (2009) and in Ciardelli (2010) can be seen as equipping each formula of firstorder inquisitive logic with a designated generator \(T\varphi \) for the corresponding supportset \([\varphi ]\). A different strategy is explored by Ciardelli et al. (2013b), who aim at making any firstorder sentence normal by refining the notion of meaning. Since logical relations will be defined based on support, and not in terms of alternatives, nonnormal sentences are not problematic for the present purposes.
 10.
This excludes tautological questions like whether John is John, which are trivially settled in all info states. We set these aside here as a manifestation of the familiar difficulties that the possible world framework has in dealing with tautologies and contradictions.
 11.
If \(\varphi \) is normal, as in our examples, the canonical choice will be \(T\varphi =\textsc {Alt}(\varphi )\), but this assumption will not be needed here.
 12.
Being able to view inquisitive logics as conservative extensions of corresponding classical systems is also crucial, e.g., for the enterprise pursued in Ciardelli and Roelofsen (2015). That work introduces an inquisitive version of epistemic logic in which one can interpret, in addition to formulas like \(K_ap\) (agent a knows that p), also formulas like \(K_a{?p}\) (agent a knows whether p) and \(W_a{?p}\) (agent a wonders whether p). The fact that this system is a conservative extension of standard epistemic logic ensures that all the existing work on the latter can be imported immediately into IEL. Thus, nothing is lost when we move from plain epistemic logic to this richer setting.
 13.
It should be noted that the two perspectives mentioned here are not in contrast with each other, but simply bring out different interesting aspects of one and the same logic, InqB. The perspective explored in this paper brings out the continuity with classical logic, showing how InqB can be viewed as adding expressive power to CPL; the alternative perspective, explored in detail in previous work (Ciardelli 2009; Ciardelli and Roelofsen 2011; Roelofsen 2013), brings out the structural relations of this logic to intuitionistic logic and intermediate logics, emphasizing the constructive character of the logic of questions.
 14.
It is quite possible that, in natural language, the alternative question whether \(\varphi \) or \(\psi \) is only settled if we establish which one of \(\varphi \) and \(\psi \) holds, to the exclusion of the other. If this is correct, such a question should be translated in our formal language not as Open image in new window , but rather as Open image in new window . Nothing important in this paper hinges on this empirical issue. What matters is that, however construed, such questions can be represented and reasoned about in the system.
 15.
This differs from the terminology standardly used in inquisitive semantics. In most previous work (e.g., Ciardelli and Roelofsen 2011) determinate sentences are called assertions; indeterminate sentences are called inquisitive, while the term question is reserved for formulas whose supportset covers the whole logical space. We use statement instead of assertion here, since the latter term is often used to refer to a speech act. As for the term question, the reason we go for a more liberal notion is that we want to consider questions that can only be resolved in some worlds. Here, we take sentences with multiple alternatives which do not cover the whole logical space, like Open image in new window , to correspond to questions such as Is Alice coming with or without Bob?, which can only be truthfully resolved in worlds where Alice is coming.
 16.
Notice that this definition partitions the formulas of our language into statements and questions. In this respect, our perspective brings InqB closer to the dichotomous inquisitive semantics \(\textsf {InqD}_\pi \) of Ciardelli et al. (2015), where formulas are partitioned into declaratives and interrogatives. The difference is that, here, the dichotomy is not built into the syntax of the language; rather, formulas are classified as statements or questions according to their semantic properties. The lack of a syntactic dichotomy between the two classes ensures that, in InqB, no restrictions need to be placed on the applicability of propositional connectives, which makes the logic more natural.
 17.
This is not necessarily the case for richer languages. In the inquisitive epistemic logic of Ciardelli and Roelofsen (2015), questions may be embedded under modalities, resulting in new statements expressing, for instance, that an agent wonders whether p. In such a system, the presence of questions also enables the language to express statements that have no equivalent counterpart in a classical modal language.
 18.
The fact that the effect of conjunction and implication on questions does not have to be stipulated, but follows from the same clauses that govern these connectives in statements is a remarkable feature that is characteristic of inquisitive logics [InqB as well as the early inquisitive system of Groenendijk (2009) and Mascarenhas (2009)]. In previous logics of questions, like Belnap and Steel (1976), analogous outcomes were obtained from operations defined adhoc, which bore no systematic relation to their truthconditional counterpart.
 19.
Such conditional questions are not directly expressible as conditionals in English. A reasonable rendering is a sentence like: given a patient’s symptoms and conditions, when is the treatment prescribed? Notice that the existence of the dependency we pointed out in our example amounts precisely to the fact that the hospital protocol settles this question.
 20.
Notice that, in general, resolutions do not correspond exactly to the alternatives for the formula. This is because one resolution may be strictly stronger than another, and thus it may fail to give rise to an alternative: for instance, \(\bot \) is a resolution of Open image in new window , but \(\bot =\emptyset \) is not an alternative for Open image in new window . If we wanted to obtain a perfect correspondence between resolutions and alternatives, we could filter out from \({\mathcal {R}}(\varphi )\) those resolutions that strictly entail another resolution. This is unproblematic, but it is not necessary for our purposes.
 21.
Interestingly, by taking Open image in new window to be the “official” disjunction of the system, InqB may also be regarded as a special kind of intermediate logic. This means that while the logic of statements is classical, the logic of questions has an intuitionistic flavor, as we will observe at several points throughout the paper. The connection between InqB and intermediate logics has been explored in detail in Ciardelli (2009) and Ciardelli and Roelofsen (2011).
 22.
The split rule is the counterpart in our system of the KreiselPutnam axiom adopted in Ciardelli and Roelofsen (2011): Open image in new window . Thus, the KreiselPutnam rule, too, which looked like a fundamental but mysterious ingredient in previous work, takes on a clear intuitive significance from the present perspective.
 23.
In order to simplify the proof, the conjunctive question \({?s_1}\wedge {?s_2}\) has been replaced here by two polar questions, \(?s_1\) and \(?s_2\). This change is merely cosmetic, and dispensable.
 24.
The proof of a dependency does not always have to proceed, as in this case, by “splitting cases”. E.g., from \(\mu \) and \(\mu \rightarrow \nu \), we can immediately infer \(\nu \) by modus ponens. We do not need to look at the resolutions of \(\mu \) and \(\mu \rightarrow \nu \). This is convenient, since the number of resolutions for \(\mu \rightarrow \nu \) is exponential in the number of resolutions for \(\mu \), and typically large.
 25.
This fact is reminiscent of the proofsasprograms correspondence known for intuitionistic logic. As discovered by Curry (1934) and Howard (1980), in intuitionistic logic formulas may be regarded as types of a certain typetheory, extending the simply typed lambdacalculus. A proof \(P:\varphi \vdash \psi \) in intuitionistic logic may be identified with a term \(t_P\) of this type theory which describes a function from objects of type \(\varphi \) to objects of type \(\psi \).
The situation is similar for InqB, except that now, formulas play double duty. On the one hand, formulas may be still be regarded as types. On the other hand, the elements of a type \(\varphi \) may in turn be identified with certain formulas, namely, the resolutions of \(\varphi \). As in intuitionistic logic, a proof \(P:\varphi \vdash \psi \) determines a function \(f_P\) from objects of type \(\varphi \) to objects of type \(\psi \); but since these objects may now be identified with classical formulas, the function \(f_P\) is now defined within the language of classical propositional logic: \(f_P:{\mathcal {L}}_c\rightarrow {\mathcal {L}}_c\).
 26.
Thanks to Justin Bledin for suggesting this analogy.
 27.
 28.
Besides this, there are other difficulties, too. First, it is hard to make sense of the truth conditions for questions. For instance, is the question what is the capital of Spain true at the actual world? The truth conditions of a sentence depend on a given information state, but it is not clear what particular information state we should consider in assessing the truth conditions of the question at a world. Second, while in Nelken and Shan’s system questions can be embedded under logical operations, we do not always get the right results. For instance, the material conditional \(p\rightarrow {?q}\), that is, \(\lnot p\vee (\Box q\vee \lnot \Box q)\), is not a correct rendering of a conditional question, such as (2). Such a question does not ask for a resolution of ?q if p happens to be true, but for a resolution of ?q under the assumption that p.
Notes
Acknowledgments
I am especially grateful to Jeroen Groenendijk and Floris Roelofsen, not only for their precious feedback on the ideas presented here, but also for much joint work in the context of which these ideas arose. In addition, I would like to thank Justin Bledin, Yacin Hamami, Rosalie Iemhoff, Ulrich Kohlenbach, Hannes Leitgeb, Johannes Marti, Martin Otto, Vít Punčochar, Mariusz Urbanski, Andrzej Wiśniewski, and Fan Yang for useful comments and discussions. Thanks to Jouko Väänänen for bringing together researchers working on dependency and on questions in various occasions; these meetings were crucial to the development of the ideas described here. Finally, thanks to two anonymous reviewers for their precious suggestions. Financial support from the Netherlands Organization for Scientific Research (NWO) is gratefully acknowledged.
References
 Abramsky, S., & Väänänen, J. (2009). From IF to BI. Synthese, 167(2), 207–230.CrossRefGoogle Scholar
 Åqvist, L. (1965). A new approach to the logical theory of interrogatives. Uppsala: University of Uppsala.Google Scholar
 Armstrong, W. W. (1974). Dependency structures of data base relationships. In Proceedings of the IFIP congress.Google Scholar
 Belnap, N., & Steel, T. (1976). The logic of questions and answers. New Haven, CT: Yale University Press.Google Scholar
 Beth, E. W. (1956). Semantic construction of intuitionistic logic. Koninklijke Nederlandse Akademie van Wetenschappen, Mededelingen, Nieuwe Reeks, 11(19), 357–388.Google Scholar
 Ciardelli, I. (2008). A generalized inquisitive semantics. Term Paper: University of Amsterdam.Google Scholar
 Ciardelli, I. (2009). Inquisitive semantics and intermediate logics. MSc Thesis, University of AmsterdamGoogle Scholar
 Ciardelli, I. (2010). A firstorder inquisitive semantics. In M. Aloni, H. Bastiaanse, T. de Jager, & K. Schulz (Eds.), Logic, language, and meaning: Selected papers from the seventeenth Amsterdam colloquium (pp. 234–243). Berlin: Springer.CrossRefGoogle Scholar
 Ciardelli, I. (2016). Dependency as question entailment. In S. Abramsky, J. Kontinen, J. Väänänen & H. Vollmer (Eds.), Dependence logic: Theory and applications (pp. 129–181). Switzerland: Springer.Google Scholar
 Ciardelli, I., Groenendijk, J., & Roelofsen, F. (2013a). Inquisitive semantics: A new notion of meaning. Language and Linguistics Compass, 7(9), 459–476.CrossRefGoogle Scholar
 Ciardelli, I., Groenendijk, J., & Roelofsen, F. (2013b). Towards a logic of information exchange: An inquisitive witness semantics. In G. Bezhanishvili, V. Marra, S. Löbner, & F. Richter (Eds.), Logic, language, and computation: Revised selected papers from the ninth international Tbilisi symposium on logic, language, and computation (pp. 51–72). Berlin: Springer.CrossRefGoogle Scholar
 Ciardelli, I., Groenendijk, J., & Roelofsen, F. (2015). On the semantics and logic of declaratives and interrogatives. Synthese, 192(6), 1689–1728.CrossRefGoogle Scholar
 Ciardelli, I., & Roelofsen, F. (2011). Inquisitive logic. Journal of Philosophical Logic, 40(1), 55–94.CrossRefGoogle Scholar
 Ciardelli, I., & Roelofsen, F. (2015). Inquisitive dynamic epistemic logic. Synthese, 192(6), 1643–1687.CrossRefGoogle Scholar
 Curry, H. (1934). Functionality in combinatory logic. Proceedings of the National Academy of Sciences, 20, 584–590.CrossRefGoogle Scholar
 Fine, K. (1975). Vagueness, truth and logic. Synthese, 30(3), 265–300.CrossRefGoogle Scholar
 Gamut, L. T. F. (1991). Language, logic and meaning. Chicago: Chicago University Press.Google Scholar
 Groenendijk, J. (1999). The logic of interrogation. In T. Matthews & D. Strolovitch (Eds.), Semantics and linguistic theory (pp. 109–126). Ithaca, NY: Cornell University Press.Google Scholar
 Groenendijk, J. (2009). Inquisitive semantics: Two possibilities for disjunction. In P. Bosch, D. Gabelaia, & J. Lang (Eds.), Seventh international Tbilisi symposium on language, logic, and computation. Berlin: Springer.Google Scholar
 Groenendijk, J. (2011). Erotetic languages and the inquisitive hierarchy. In a Festschrift for Martin Stokhof. http://dare.uva.nl/document/487828.
 Groenendijk, J., & Roelofsen, F. (2009). Inquisitive semantics and pragmatics. In Presented at the workshop on language, communication, and rational agency at Stanford. www.illc.uva.nl/inquisitivesemantics.
 Groenendijk, J., & Roelofsen, F. (2013). Towards a suppositional inquisitive semantics. In M. Aher, D. Hole, E. Jeřábek, & C. Kupke (Eds.), Logic, language, and computation: 10th international Tbilisi symposium on logic, language, and computation, TbiLLC 2013, Gudauri, Georgia, September 23–27, 2013. Revised Selected Papers (pp. 137–156). Berlin: Springer.Google Scholar
 Groenendijk, J., & Stokhof, M. (1984). Studies on the semantics of questions and the pragmatics of answers. PhD Thesis, University of Amsterdam.Google Scholar
 Harrah, D. (1961). A logic of questions and answers. Philosophy of Science, 28, 40–46.CrossRefGoogle Scholar
 Harrah, D. (1963). Communication: A logical model. Cambridge: MIT Press.Google Scholar
 Hintikka, J. (1962). Knowledge and belief: An introduction to the logic of the two notions. Cornell: Cornell University Press.Google Scholar
 Hintikka, J. (1999). Inquiry as inquiry: A logic of scientific discovery. Dordrecht: Kluwer Academic Publishers.CrossRefGoogle Scholar
 Holliday, W. (2014). Partiality and adjointness in modal logic. In R. Goré, B. Kooi, & A. Kurucz (Eds.), Advances in modal logic (AiML) (pp. 313–332). London: College Publications.Google Scholar
 Howard, W. (1980). The formulaeastypes notion of construction. In J. P. Seldin & J. R. Hindley (Eds.), To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism (pp. 479–490). New York: Academic Press.Google Scholar
 Humberstone, L. (1981). From worlds to possibilities. Journal of Philosophical Logic, 10(3), 313–339.CrossRefGoogle Scholar
 Kripke, S. (1965). Semantical analysis of intuitionistic logic I. In J. N. Crossley & M. A. Dummett (Eds.), Formal systems and recursive functions (pp. 92–130). Amsterdam: NorthHolland.CrossRefGoogle Scholar
 Mascarenhas, S. (2009). Inquisitive semantics and logic. Master Thesis, University of Amsterdam.Google Scholar
 Nelken, R., & Shan, C.C. (2006). A modal interpretation of the logic of interrogation. Journal of Logic, Language, and Information, 15, 251–271.CrossRefGoogle Scholar
 Punčochář, V. (2015a). A generalization of inquisitive semantics. Journal of Philosophical Logic. doi: 10.1007/s1099201593791.
 Punčochář, V. (2015b). Weak negation in inquisitive semantics. Journal of Logic, Language, and Information, 24(3), 323–355.CrossRefGoogle Scholar
 Roelofsen, F. (2013). Algebraic foundations for the semantic treatment of inquisitive content. Synthese, 190(1), 79–102.CrossRefGoogle Scholar
 Sano, K. (2009). Sound and complete treesequent calculus for inquisitive logic. In Proceedings of the sixteenth workshop on logic, language, information, and computation.Google Scholar
 Segoufin, L., & Vianu, V. (2005). Views and queries: Determinacy and rewriting. In Principles of database systems, (pp 49–60). New York: ACM.Google Scholar
 ten Cate, B., & Shan, C.C. (2007). Axiomatizing Groenendijk’s logic of interrogation. In M. Aloni, A. Butler, & P. Dekker (Eds.), Questions in dynamic semantics (pp. 63–82). Amsterdam: Elsevier.Google Scholar
 Tichy, P. (1978). Questions, answers, and logic. American Philosophical Quarterly, 15, 275–284.Google Scholar
 Troelstra, A., & van Dalen, D. (1988a). Constructivism in mathematics, an introduction, volume 1. In Studies in logic and the foundations of mathematics (Vol. 121). Amsterdam: NorthHolland.Google Scholar
 Troelstra, A., & van Dalen, D. (1988b) Constructivism in mathematics, an introduction, volume 2. In Studies in logic and the foundations of mathematics (Vol. 123). Amsterdam: NorthHolland.Google Scholar
 Väänänen, J. (2007). Dependence logic: A new approach to independence friendly logic. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
 Väänänen, J. (2008). Modal dependence logic. In K. R. Apt & R. van Rooij (Eds.), New perspectives on games and interaction. Amsterdam: Amsterdam University Press.Google Scholar
 van Benthem, J. (1986). Partiality and nonmonotonicity in classical logic. Logique et Analyse, 29(114), 225–247.Google Scholar
 Velissaratou, S. (2000). Conditional questions and whichinterrogatives. MSc Thesis, University of Amsterdam.Google Scholar
 Veltman, F. (1981). Data semantics. In J. Groenendijk, T. Janssen, & M. Stokhof (Eds.), Formal methods in the study of language. Amsterdam: Mathematical Centre.Google Scholar
 Wiśniewski, A. (1995). The posing of questions: Logical foundations of erotetic inferences (Vol. 252). Dordrecht: Kluwer Academic Publishers.CrossRefGoogle Scholar
 Wiśniewski, A., & LeszczyńskaJasion, D. (2015). Inferential erotetic logic meets inquisitive semantics. Synthese, 192(6), 1585–1608.CrossRefGoogle Scholar
 Yang, F. (2014). On extensions and variants of dependence logic: A study of intuitionistic connectives in the team semantics setting. PhD Thesis, University of Helsinki.Google Scholar
Copyright information
Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.