2.1 Language

The language of $\textsf {Inq2D}$ is defined as follows:

Definition 2.1 (Logical language)

We define the usual abbreviations:

In short, we extend the basic inquisitive logic $\textsf {InqB}$ (following the notation conventions of [Reference Ciardelli1]) with operators to express necessity ( $\square $ ), actuality (A) and apriority ( $\blacksquare $ ).

Necessity and apriority operate on different levels: the former is a property of propositions, while the latter is a property of propositional concepts (or, in Kaplanian terms, of content and of character, respectively). However, there are reasons for considering apriority as part of the logical language rather than as a meta-logical notion, and therefore operating on the same level in the formalization as necessity. First, it is interesting to study the interactions between apriority and necessity (see, for instance, the analysis of the nesting problem in [Reference Fritz6]). Second, it makes sense to embed claims about apriority of sentences under logical operators, like negation and question-forming operators.

2.2 Semantics

Our semantics will operate on the same models as the ones used in [Reference Fritz6, Reference Fritz7].Footnote ⁵

We can think of matrix frames as diagrams in which the elements of $W'$ are both on the vertical and the horizontal axis, and the pairs in W are coordinates. A pair $\langle w, v \rangle $ is an evaluation point that takes w to be the world considered as actual and v to be the world of evaluation.

If w and v are the same, then the actual world is the evaluation world, which can be considered the normal situation. However, we also need pairs in which w and v are different, namely to evaluate expressions in a different world than the one in which they are uttered. As we will see, this is the case only if we are evaluating expressions embedded under $\square $ . For example, it is true in w that John could have been somewhere else than where he actually is, if there is a pair $\langle w,v\rangle $ such that John is in a different place in v than where he is in w.

The relation $R_\square $ connects a pair to all the pairs on the same row. This means that it considers other worlds of evaluation, while keeping the actual world constant. The relation $R_A$ looks at the unique ‘actual pair’ within the row. That is, it connects any $\langle w,v\rangle $ to $\langle w,w\rangle $ .

D is the set of all these ‘actual pairs’: pairs in which the same world is contained twice. It is also called the diagonal because of the position these pairs are in when we draw a matrix. D will be the set of distinguished elements on which consequence and validity will be defined. $R_\blacksquare $ connects each pair simply to all pairs on the diagonal. See Figure 1 for an illustration of the relations in a matrix frame.

Fig. 1 Relations in matrix frames (transitive arrows omitted).

As usual in inquisitive semantics, we will evaluate sentences not relative to single points in the model but relative to sets of them—in this case, not sets of worlds but sets of pairs of worlds. We will call any subset of W an information state and use the term diagonal information state for subsets of D.

We can think of an information state s as something that gives us incomplete information about what the actual world is (namely, it is one of the worlds w such that $\langle w,v\rangle \in s$ for some v). In a similar way, it gives us information about what the world of evaluation is (namely, one of the worlds v such that $\langle w,v\rangle \in s$ for some w). On top of this, it also gives us information about how the two relate: for instance, the information state $\{\langle w,w\rangle , \langle v,v\rangle \}$ also tells us that the actual world and the evaluation world are the same.

Not all information states in the model represent natural states of information for a person to be in. In fact, a person can be assumed to always be in a diagonal information state: we might not know what the actual world is or what the evaluation world is, but we can always know that these two are the same. Like non-diagonal pairs, non-diagonal information states are only present in the model to evaluate expressions embedded under $\square $ .

A matrix model is any matrix frame extended with a valuation function V, which will be defined as follows: instead of assigning a set of worlds to each propositional atom, it assigns a set of pairs of worlds, so a set of elements of W.

Whenever p represents a sentence with an indexical, like ‘I am hungry’, its truth will depend not only on the world of evaluation (which determines whether the person denoted by ‘I’ is indeed hungry), but also on what the actual world is (which determines how the indexical is resolved). Therefore, the valuation may make it true in $\langle w,v\rangle $ but false in $\langle w',v\rangle $ . Atoms whose truth does not at all depend on the left element of pairs can be considered to represent sentences without indexicals or proper names.

We are now ready to give the semantics for $\textsf {Inq2D}$ , which is a special case of inquisitive Kripke modal logic (InqBK) as presented in [Reference Ciardelli1].Footnote ⁶

We write $s\models \varphi $ for ‘s supports $\varphi $ ’, which means that the information in s already contains the information conveyed by $\varphi $ and settles the issue raised by $\varphi $ . The issue that a formula raises is trivial if there is only one maximal supporting state, while the information a formula conveys is trivial if the supporting states together cover the entire logical space.

We can define the notion of truth with respect to an evaluation pair as support in the corresponding singleton state:

Definition 2.4 (Truth)

$$ \begin{align*}\langle w,v\rangle\models\varphi \iff \{\langle w,v\rangle\}\models\varphi.\end{align*} $$

This notion of truth relative to a pair allows us to give the derived support conditions for the abbreviations in the following way:

For some formulas, being supported in s simply amounts to being true relative to all pairs in s. These formulas are called truth-conditional.

Definition 2.5 (Truth-conditionality)

A formula $\varphi $ is truth-conditional iff

$$ \begin{align*}s\models\varphi\iff\text{for all } \langle w,v\rangle\in s: \langle w,v\rangle\models\varphi.\end{align*} $$

The operator (inquisitive disjunction) can be used to construct formulas that are not truth-conditional, such as . For this formula to be supported in s, it is not enough if all pairs in s make it true—it is required that they either all make p true or all make q true. Formulas that are not truth-conditional will be called questions.

2.3 State-based actuality

Two facts about the modalities should be highlighted. First, any formula of the form $\square \varphi $ , $\blacksquare \varphi $ or $A\varphi $ is by definition a truth-conditional formula (this can be seen from the support conditions, which operate on individual pairs). For necessity and apriority this is as it should be, since ‘it is necessary whether $\varphi $ ’ and ‘it is a priori whether $\varphi $ ’ are indeed statements, not questions. Second, since $R_A$ connects every pair only to one single pair, the truth conditions of $A\varphi $ are not sensitive to the issue raised by $\varphi $ .Footnote ⁷ Thus, what $A\varphi $ expresses can be phrased as ‘in the actual world, the information conveyed by $\varphi $ is true’.Footnote ⁸

From a logical perspective it makes sense to consider an alternative actuality operator

, which is sensitive to issues:Footnote ⁹

A formula

is supported by an information state s just in case the information in s about what the actual world is settles the issue expressed by $\varphi $ . Unlike $A\varphi $ ,

is sensitive to the inquisitive content of $\varphi $ and can be a question itself.

However, adding does not make the language more expressive, and since it will be easier for us to work with A in our completeness proof, we will consider A as primitive and define by the following recursive definition:Footnote ¹⁰

• • whenever $\varphi $ is atomic or of the form $\square \psi $ , $A\psi $ or $\blacksquare \psi ;$

• •

• •

• •

With this recursive definition, the support conditions for given above follow as a fact. Whenever $\varphi $ is truth-conditional, $A\varphi $ and are equivalent. For questions $\psi $ , is always equivalent to some formula without ’s.

2.4 Consequence relations

Following the terminology of Crossley & Humberstone [Reference Crossley and Humberstone4], we can distinguish two relations of consequence in two-dimensional logic: the general consequence relation looks at all evaluation pairs of the model, while the real-world consequence relation only looks at diagonal pairs (elements of D). Both of these notions can be generalized to information states.

Intuitively, we want our consequence relation to be such that $\blacksquare \varphi \models \varphi $ . This is not satisfied in the general consequence relation, because it considers all information states. There are information states that support $\blacksquare \varphi $ but not $\varphi $ , namely ones that contain non-diagonal pairs. Therefore it makes more sense to restrict the consequence relation to diagonal information states (subsets of D):

This restriction can be motivated by viewing real-world consequence as a specific case of contextual entailment [Reference Ciardelli1]: we are interested in entailment in a specific context, namely the state in which everything which is a priori is supported, and this state is exactly the diagonal D in our models.Footnote ¹¹

Notice that this does not mean that information states that are not diagonal should be disregarded altogether, as they still come into play whenever a $\square $ -operator is used. They are essential to capture the distinction between necessity and apriority.

For each information state s there is a diagonal information state $s'$ consisting of all the $\langle w,w\rangle $ such that $\langle w,v\rangle \in s$ . As we have seen, is defined in such a way that we have . This can be used to connect the notions of general and real-world consequence by the following fact:

As we will see later, this connection will be exploited by our inference relation.

The notions of general consequence and real-world consequence come with their corresponding notions of validity. The latter is more restricted than the former: the real-world validities include sentences which are valid by virtue of their indexicals, such as ‘Am I here now?’ or $\mathord {?}(A p \rightarrow p)$ , while the general validities are only those sentences that are purely logically resolved (such as $\mathord {?}(p\rightarrow p)$ ).

Notice that apriority is not the same as real-world validity: although all real-world validities are a priori, the converse is not the case. For instance, p can be a priori in some model, but it is not valid.

2.5 Questions and apriority

Classically, what it means for a formula to be valid is that it is true in any possible world in any model. In inquisitive logics, a formula is valid if it is supported in any state in any model.

Normally, this definition makes sure that inquisitive disjunction does not introduce any new validities to the logic. That is, inquisitive logics usually satisfy the disjunction property, which says that the validity of an inquisitive disjunction can be traced back to the validity of one of the disjuncts:

The intuitive idea behind this property is as follows. An inquisitive disjunction puts forward a request to choose between two alternatives. If this disjunction is valid—which means that this choice can be made purely by logic—then one of the suggested alternatives should be valid [Reference Grilletti8].

An interesting observation we can make here is that this property does not hold for $\textsf {Inq2D}$ .Footnote ¹² A counterexample is the following:

It is easy to see why this disjunction is valid: it is supported if either p is true in all pairs on the diagonal or p is false in at least one pair on the diagonal. Clearly, in all models one of the two must be the case. So the failure of the disjunction property is due to the global nature of $R_\blacksquare $ .Footnote ¹³

Intuitively, this result seems to be correct: the only situation in which we can be uncertain as to whether some statement p is a priori is if we do not really grasp what it means—but this is like not knowing in which model we are. Given some model that defines what sentences mean (by means of its valuation function), the question $\mathord {?}\blacksquare p$ should always be resolved.Footnote ¹⁴

While $\mathord {?}\blacksquare p$ is valid, the same does not hold for $\blacksquare \mathord {?} p$ , which expresses something else. The former expresses the question ‘whether it is a priori that p’ while the latter expresses the statement ‘it is a priori whether p’, which is false if the pairs on the diagonal do not agree on the truth value of p.

3.1 Proof system

The proof system for general consequence is displayed in Table 1. It is a Hilbert-style proof system that consists of the standard axioms (A1–A10) and rules (R1–R3) for inquisitive modal logic, extended with the axioms of two-dimensional modal logic (A11–A19) [Reference Fritz7]. The axioms for inquisitive disjunction (A7–A10) are not relevant for the classical fragment, but we will need them when we consider the full language in Section 4. We will denote the proof system of general consequence by $\vdash _{\textsf {g}}$ .

Table 1 Proof system $\vdash _{\textsf {g}}$ of general consequence, where $\alpha $ ranges only over classical formulas. Some modal rules and axioms apply to $\boxtimes \in \{\square ,A,\blacksquare \}$

The soundness of this proof system can be shown by checking that all individual rules and axioms are sound. For (A1–A10, R1–R3), proofs can be found in [Reference Ciardelli1].Footnote ¹⁷ As for (A11–A19), it is easy to see how the properties of the respective relations in the model make them valid (e.g., $\square \alpha \rightarrow \alpha $ and $\Diamond \alpha \rightarrow \square \Diamond \alpha $ are valid because $R_\square $ is an equivalence relation).

3.2 Sliced matrix model

In a regular matrix model, the relation $R_\blacksquare $ connects every pair in the domain with every pair on the diagonal D. In contrast, in a sliced matrix model, $R_\blacksquare $ relates all pairs to some (not necessarily all) pairs on the diagonal.

We can think of such a model as a matrix model which is divided into slices: within a slice, $R_\blacksquare $ can reach all pairs on the diagonal, but it cannot reach any pair outside of the slice. Since $\blacksquare $ is the only modality that can be used to express what is true on other rows, this means that what is true in pairs in one slice is completely independent of what is true in other slices. See Figure 2 for a graphical representation of a sliced matrix model.

Fig. 2 Example of a sliced matrix model. The arrows represent $R_\blacksquare $ (transitive arrows omitted).

We already introduced two consequence relations before, namely general consequence ( $\models _{\textsf {g}}$ ) and real-world consequence ( $\models _{\textsf {r}}$ ). We will now introduce a third notion of consequence, namely the one defined using sliced matrix models.

Note that a regular matrix model is by definition also a sliced matrix model, namely one with exactly one slice.

3.3 Canonical model

We will now construct a canonical model for $\vdash _{\textsf {g}}$ . To make sure that this model has the shape of a matrix, the domain of this model will not be the set of maximally consistent sets of formulas, but the set of all pairs of these. This guarantees that there are just as many rows as there are columns, and that each row has the same amount of elements.

Let us first go through some preliminary definitions. Let $T^c$ be the set of maximally $\vdash _{\textsf {g}}$ -consistent sets of formulas of $\mathcal {L}_!$ . Then we define $W^c = T^c \times T^c$ . For every set of formulas $\Gamma $ , let $\Gamma _A = \{\alpha ~|~A\alpha \in \Gamma \}$ . It is important to note that if $\Gamma $ is maximally consistent, then so is $\Gamma _A$ . This is because by maximal consistency, $\Gamma $ contains either $A\alpha $ or $\neg A\alpha $ . In the latter case, by axiom (A13) it must also contain $A\neg \alpha $ . So $\Gamma _A$ contains exactly one of $\alpha $ and $\neg \alpha $ .

As the points in the canonical model will not themselves be theories but pairs of theories, we need to say which formulas are true at each point. Thus, we need to assign a theory to each pair of theories $\langle \Gamma , \Delta \rangle $ . Clearly it cannot be $\Gamma $ , for then all pairs on a row would make the same formulas true. It can also not be $\Delta $ : in that case, the theory of $\langle \Gamma ,\Gamma \rangle $ would be $\Gamma $ . Since $\langle \Gamma ,\Gamma \rangle $ is on the diagonal, we want the theory of $\langle \Gamma ,\Gamma \rangle $ to be the set of formulas $\alpha $ such that $A\alpha $ is in the theory of $\langle \Gamma ,\Delta \rangle $ . But this is only the case if $\Gamma = \Delta _A$ , so it will not work for arbitrary $\Gamma $ and $\Delta $ . Therefore, the theory of a pair $\langle \Gamma ,\Delta \rangle $ must be a possibly distinct theory, determined by $\Gamma $ and $\Delta $ . We will use the following definition:

Definition 3.4. For each $\langle \Gamma ,\Delta \rangle \in W^c$ , we define:

$$ \begin{align*}\mathsf{t}(\Gamma,\Delta) = \begin{cases}\Delta&\text{if}\ \Gamma_A = \Delta_A\ \text{and}\ \Gamma\neq\Delta,\\\Gamma_A&\text{otherwise.}\end{cases}\end{align*} $$

The idea behind this definition is as follows. Any pair $\langle \Gamma ,\Gamma \rangle $ must be the ‘actual pair’ in its row, but it is not guaranteed that $\Gamma $ is a suitable theory for this: it may be the case that $A\alpha \leftrightarrow \alpha \not \in \Gamma $ . Therefore, $\Gamma _A$ will be the true theory assigned to this pair. Any other element $\langle \Gamma ,\Delta \rangle $ on this row can have $\Delta $ as its true theory, but only if $\Delta $ contains exactly the formulas $A\alpha $ such that $\alpha $ is true in the actual pair. If this is not the case, we reuse $\Gamma _A$ , which makes this element a dummy copy of the actual pair.

In this way, each pair in $W^c$ is associated with a maximally consistent set. The following lemma shows that the converse is also the case: each maximally consistent set $\Gamma $ is associated with at least one pair in the canonical model.

Lemma 3.1. For every maximally consistent set $\Gamma $ :

$$ \begin{align*}\mathsf{t}(\Gamma_A,\Gamma) = \Gamma.\end{align*} $$

The following lemma shows that $\Gamma _A$ consists of all and only the A-formulas of any pair, and will be important in what follows:

Lemma 3.2. For all maximally consistent sets $\Gamma ,\Delta $ :

$$ \begin{align*}A\alpha \in \textsf{t}(\Gamma,\Delta) \iff \alpha\in\Gamma_A.\end{align*} $$

We can now give the definition of the canonical model itself.

To show that the canonical model is indeed a sliced matrix model, we need to show that $R^c_\blacksquare $ relates every pair to the actual pair of its row, and that it is transitive and euclidean. A simple proof using the appropriate axioms suffices to show this.

The completeness proof continues as usual, by establishing a relation between truth at a point in the canonical model and membership of that point, which in this case is mediated by $\textsf {t}$ .

Lemma 3.3 (Truth lemma)

$$ \begin{align*}M^c,\langle\Gamma,\Delta\rangle\models\alpha\iff \alpha\in \textsf{t}(\Gamma,\Delta).\end{align*} $$

3.4 Completeness

Having established the truth lemma, we can prove completeness in the standard way.

Theorem 3.1 (Completeness wrt sliced matrix frames)

$$ \begin{align*}\Gamma\models_{\textsf{s}}\alpha \Rightarrow \Gamma\vdash_{\textsf{g}}\alpha.\end{align*} $$

We have thereby shown that the proof system $\vdash _{\textsf {g}}$ is complete with respect to sliced matrix models. Now we want to show that it is also complete with respect to regular matrix models. This is the case because for every pointed sliced matrix model we can find a pointed regular matrix model that satisfies exactly the same formulas.

Theorem 3.2 (Completeness wrt regular matrix frames)

$$ \begin{align*}\Gamma\models_{\textsf{g}}\alpha \Rightarrow \Gamma\vdash_{\textsf{g}}\alpha.\end{align*} $$

Proof. For this we only need to show that $\Gamma \models _{\textsf {g}}\alpha \Rightarrow \Gamma \models _{\textsf {s}}\alpha $ . Suppose there is a sliced matrix model M and pair $\langle w_0,v_0\rangle $ such that $M,\langle w_0,v_0\rangle \models \gamma $ for all $\gamma \in \Gamma $ but $M,\langle w_0,v_0\rangle \not \models \alpha $ . We define the following regular matrix model $M'$ :

• • $W' = W$ , $R^{\prime }_\square = R_\square $ , $R^{\prime }_A = R_A$ ;

• • Define $R^{\prime }_\blacksquare $ as in a regular matrix model: $\langle w,v \rangle R^{\prime }_\blacksquare \langle w',v' \rangle \iff w'=v'$ ;

• • Let $X = \{ w~|~ \langle w_0,v_0\rangle R_\blacksquare \langle w,v\rangle \text { for some } v \}$ (X is the set of worlds whose row is accessible by $R_\blacksquare $ );

• • We define the following function from pairs to pairs, and define the valuation of $M'$ in terms of this function:

  $f( w,v) = \begin {cases} \langle w,v\rangle & \text {if } w\in X;\\ \langle w_0,w_0\rangle & \text {if }w\not \in X \text { and }w=v;\\ \langle w_0,w\rangle & \text {if }w\not \in X \text { and }v=w_0;\\ \langle w_0,v\rangle & \text {otherwise;}\end {cases}$

  $V'(p)( w,v) = V(p)(f( w,v)).$

In words, if in M a row was accessible by $R_\blacksquare $ from $\langle w_0,v_0\rangle $ , then the valuation of this row in $M'$ is the same. If not, then the valuation of the row is copied from that of the row of $\langle w_0,v_0\rangle $ , but with two pairs swapped: the pair $\langle w,w\rangle $ is valuated like $\langle w_0,w_0 \rangle $ , and the pair $\langle w,w_0 \rangle $ is valuated like $\langle w_0,w\rangle $ . This ensures that the valuation of the actual pair on the new row is the same as the valuation of the actual pair on the original row. See Figure 3 for a graphical representation of this construction.

Fig. 3 A pointed sliced matrix model (a), and a pointed matrix model (c) that satisfies the same formulas. The $\times $ marks the pair on which the model is based. Its slice is copied entirely, and rows from other slices are replaced by its own row, as shown in (b). On these copied rows, the actual pair has to switch positions so it ends up on the diagonal, as is shown in (c).

We can then show that $M',\langle w,v\rangle \models \beta \iff M,f( w,v)\models \beta $ . The proof goes by induction on the structure of formulas, the crucial step is the one for $\blacksquare $ :

1. (⇒) Suppose $M',\langle w,v\rangle \models \blacksquare \beta $ . Then for all $w'$ , we have that $M',\langle w',w'\rangle \models \beta $ and by the induction hypothesis, that $M,f( w',w') \models \beta $ .

   Now take any pair $\langle v',v'\rangle $ such that $f( w,v )R_\blacksquare \langle v',v'\rangle $ . We need to show that $\langle v',v'\rangle = f( w',w')$ for some $w'$ . This follows from the definition of X and f: since $f( w,v )R_\blacksquare \langle v',v'\rangle $ , it must be that $v'\in X$ . Then it follows that $\langle v',v'\rangle = f( v',v')$ .

   By the induction hypothesis, $M,f( v',v') \models \beta $ . Since $\langle v',v'\rangle $ was an arbitrary pair, it follows that $M,f( w,v) \models \blacksquare \beta $ .

2. (⇐) Suppose $M',\langle w,v\rangle \not \models \blacksquare \beta $ . Then there is some $w'$ such that $M',\langle w',w'\rangle \not \models \beta $ . By the induction hypothesis, $M,f( w',w') \not \models \beta $ .

   We need to show that $f( w,v )R_\blacksquare f( w',w')$ . By the definition of f, it must be that $f( w,v )$ and $f( w',w')$ are both pairs whose left element is a world in X, and that $f( w',w')$ is a diagonal pair.

   It follows that $M,f( w,v) \not \models \blacksquare \beta $ .

By definition, $f( w_0,v_0) = \langle w_0,v_0\rangle $ . This means that $M',\langle w_0,v_0\rangle \models \beta \iff M,\langle w_0,v_0\rangle \models \beta $ . We have thus constructed a regular matrix model $M'$ and pair $\langle w_0,v_0\rangle $ that makes all of $\Gamma $ true, but not $\alpha $ .Footnote ¹⁸ □

3.5 Logic of real-world consequence

So far we have shown that $\Gamma \models _{\textsf {g}}\alpha \iff \Gamma \vdash _{\textsf {g}}\alpha $ , but recall that what we were after was an inference relation for real-world consequence. We can define this as follows:

Definition 3.6 (Real-world inference relation)

The inference relation $\vdash _{\textsf {r}}$ for the real-world consequence relation is defined by:

$$ \begin{align*}\Gamma\vdash_{\textsf{r}} \alpha\iff \{A\gamma~|~\gamma\in\Gamma\} \vdash_{\textsf{g}} A\alpha.\end{align*} $$

By the above definition, any proof in the system $\vdash _{\textsf {g}}$ , with $A\gamma $ for all $\gamma \in \Gamma $ as premises and $A\alpha $ as conclusion, counts as a proof of $\alpha $ from $\Gamma $ in $\vdash _{\textsf {r}}$ .

Recall that this mimics exactly the semantic relation between general consequence and real-world consequence. It follows that this inference relation is sound and complete:

Theorem 3.3 (Real-world soundness and completeness)

$$ \begin{align*}\Gamma\vdash_{\textsf{r}} \alpha\iff \Gamma\models_{\textsf{r}} \alpha.\end{align*} $$

4.1 Proof system

The proof system $\vdash _{\textsf {g}}$ , which we introduced in Section 3.1, remains unchanged for now, but unlike before we will also use the axioms for inquisitive disjunction (A7–A10). We will see in Section 4.3 that we need one extra axiom to make the step from sliced matrix models to regular matrix models, but for the moment we will go back to working with sliced matrix models.

4.2 Resolutions

For the completeness proof we make use of the tight relation between inquisitive logic and classical logic, which can be sketched as follows: every formula in $\textsf {Inq2D}$ can be characterized by a set of classical formulas, which are called its resolutions, in such a way that an information state s supports $\varphi $ just in case it supports at least one of its resolutions $\alpha $ .

Extending the definition in [Reference Ciardelli1], we can define resolutions for the whole language of $\textsf {Inq2D}$ as follows:

Because $\varphi $ is supported just in case one of its resolutions is, we can also say that $\varphi $ is supported just in case the inquisitive disjunction of its resolutions is. This shows that any formula can be rewritten as an inquisitive disjunction of classical formulas, which we call its normal form:Footnote ¹⁹

Fact 4.1 (Normal form)

The notion of resolution can be generalized to sets of formulas $\Phi $ in the following way: we call a function $f: \Phi \rightarrow \mathcal {L}_!$ a resolution function of $\Phi $ if for all $\varphi \in \Phi $ , $f(\varphi )\in \mathcal {R}(\varphi )$ . We can then say that $\mathcal {R}(\Phi )$ is the set of sets of formulas $\Gamma $ such that $\Gamma = \{f(\varphi )~|~\varphi \in \Phi \}$ for some resolution function f of $\Phi $ . Simply put, a resolution of $\Phi $ is a set of classical formulas that contains a resolution for each $\varphi \in \Phi $ .

With this generalized notion of resolutions, we can obtain the following lemma:

Lemma 4.1 (Semantic resolution lemma)

$$ \begin{align*}\Phi\models_{\textsf{s}}\psi\iff\text{ for all } \Gamma\in \mathcal{R}(\Phi) \text{ there is } \alpha\in\mathcal{R}(\psi) \text{ such that } \Gamma\models_{\textsf{s}}\alpha.\end{align*} $$

In the proof above, the step in which we construct a new model out of several models, while maintaining the same supported formulas, is not available in regular matrix models. In these models, the truth value of $\blacksquare \alpha $ may change as the model gets bigger, because diagonal pairs become accessible that previously weren’t. Thus, the semantic resolution lemma does not hold for the general consequence relation $\models _{\textsf {g}}$ .Footnote ²⁰ This is why we again need to make a detour through sliced matrix models.

The resolution lemma holds on the syntactic side as well:

Lemma 4.2 (Syntactic resolution lemma)

$$ \begin{align*}\Phi\vdash_{\textsf{g}}\psi\iff\text{ for all } \Gamma\in \mathcal{R}(\Phi) \text{ there is } \alpha\in\mathcal{R}(\psi) \text{ such that } \Gamma\vdash_{\textsf{g}}\alpha.\end{align*} $$

These two lemmas can be connected by the fact that $\vdash _{\textsf {g}}$ is sound and complete for the classical fragment, which we have already shown. Thus we obtain:

Theorem 4.1 (Soundness and completeness wrt sliced frames)

$$ \begin{align*}\Phi\models_{\textsf{s}}\psi \iff \Phi\vdash_{\textsf{g}}\psi.\end{align*} $$

4.3 Regular matrix frames

The next step is to obtain a proof system that is complete with respect to regular matrix frames. Recall that when we proved completeness for the classical fragment, we could use the fact that sliced matrix models and regular matrix models share the same consequence relation. However, this is no longer the case when we consider the full language.

A counterexample is $\mathord {?}\blacksquare p$ . A state s can fail to support this formula in a sliced matrix model: if s contains worlds from more than one slice, p may be a priori in some worlds, but not in others. This is not possible in a regular matrix model, as we have already seen in Section 2.5. There, whether something is a priori cannot differ from world to world: if something is a priori, it is a priori everywhere. Thus, $\mathord {?}\blacksquare p$ is a validity in these models.

In fact, the class of regular matrix frames is exactly the class of sliced frames on which $\mathord {?}\blacksquare p$ is valid. We only need to add the axiom schema $\mathord {?}\blacksquare \alpha $ to obtain completeness with respect to regular matrix frames.

Define $\vdash _{\textsf {g}'}$ as the proof system consisting of the axioms and rules in (A1–A19, R1–R3) and (A20):Footnote ²¹

1. A20 $\mathord {?}\blacksquare \alpha .$

Recall that $\models _{\textsf {g}}$ is the consequence relation in which we consider only models in which $R_\blacksquare $ makes the whole diagonal accessible, while $\models _{\textsf {s}}$ is the consequence relation based on sliced matrix models. To prove completeness, we need to show the following lemma.

Lemma 4.3. Let $\Delta _{A20} = \{\mathord {?}\blacksquare \alpha ~|~\alpha \in \mathcal {L}_!\}$ .

$$ \begin{align*}\Phi\models_{\textsf{g}}\psi \Rightarrow \Phi,\Delta_{A20}\models_{\textsf{s}}\psi.\end{align*} $$

Proof. Suppose we have a sliced model M and a state $s_0$ such that $M,s_0\models \Phi $ , $M,s_0\models \Delta _{A20}$ and $M,s_0\not \models \psi $ . We can then construct a regular model $M'$ which has a state $s_0$ that supports exactly the same formulas as $s_0$ in M. The construction is similar to the one used in the proof for Theorem 3.2. We need to slightly change the definition of X and the valuation:

• • Let $X = \{ w~|~ \langle w',v'\rangle R_\blacksquare \langle w,v\rangle \text { for some } \langle w',v'\rangle \in s_0 \text { and some } v \}$ (we let X be the set of worlds whose row is accessible by $R_\blacksquare $ from any pair in $s_0$ );

• • Since by assumption $M,s_0\not \models \psi $ , it follows that $s_0$ is non-empty. This means we can let $\langle w_0,v_0\rangle $ be one of the pairs in $s_0$ (it does not matter which one). We can then define f and $V'$ as before:

  $f( w,v) = \begin {cases} \langle w,v\rangle & \text {if } w\in X;\\ \langle w_0,w_0\rangle & \text {if }w\not \in X \text { and }w=v;\\ \langle w_0,w\rangle & \text {if }w\not \in X \text { and }v=w_0;\\ \langle w_0,v\rangle & \text {otherwise};\end {cases}$

  $V'(p)( w,v) = V(p)(f( w,v)).$

  We will use $f(s)$ as shorthand for $\{ f( w,v) ~|~ \langle w,v\rangle \in s\}$ .

In this construction, all slices that $s_0$ overlaps with keep the same valuation in $M'$ . For other slices, the valuation of each row is copied from that of the row of $\langle w_0,v_0\rangle $ , but with two pairs swapped as before. See Figure 4 for a graphical representation of this construction.

Fig. 4 An information state in a sliced matrix model (a), and an information state in a regular matrix model (c) that satisfies the same formulas. The slices that overlap with the information state are copied entirely, and rows from other slices are replaced by the row from the pair marked with $\times $ (an arbitrary pair in the information state), as shown in (b). On the copied rows, the actual pair has to switch positions so it ends up on the diagonal, as is shown in (c).

Note that from the assumption that $M,s_0\models \Delta _{A20}$ it follows that $M,X \times W \models \Delta _{A20}$ . Because if not, then there would be some $\alpha $ and some $w,w'\in X$ such that for some $v,v'$ , $M,\langle w,v\rangle \models \blacksquare \alpha $ and $M,\langle w',v'\rangle \models \neg \blacksquare \alpha $ . But by definition of X, both $\langle w,v\rangle $ and $\langle w',v'\rangle $ share their slice with at least one pair in $s_0$ . This would mean $M,s_0\not \models \ \mathord {?}\blacksquare \alpha $ , contradicting our assumption. Since we have $M,X \times W \models \Delta _{A20}$ , it follows by definition of f that $M,f(W \times W) \models \Delta _{A20}$ .

We can then show, by induction on the normal form of formulas, that for all states $s: M',s\models \varphi \iff M,f(s)\models \varphi $ . The crucial step in this induction is the left to right direction for $\blacksquare $ . It suffices to show that the claim holds for an arbitrary $\langle w,v\rangle \in s$ .

1. (⇐) Suppose $M',\langle w,v\rangle \not \models \blacksquare \alpha $ . Then for some $w'$ , we have that $M',\langle w',w'\rangle \not \models \alpha $ and by the induction hypothesis, that $M,f( w',w') \not \models \alpha $ .

   By reflexivity of $R_\blacksquare $ , it follows that $M,f( w',w') \not \models \blacksquare \alpha $ . Therefore, the state $f(W \times W)$ does also not support $\blacksquare \alpha $ . But since $M, f(W \times W) \models \mathord {?}\blacksquare \alpha $ , we must have $M, f(W \times W) \models \neg \blacksquare \alpha $ . This means that no member of $f(W \times W)$ supports $\blacksquare \alpha $ , so $M,f( w,v) \not \models \blacksquare \alpha $ .

Since $f(s_0) = s_0$ , we have shown that $M, s_0\models \varphi \iff M', s_0\models \varphi $ . So we have a regular matrix model $M'$ and a state $s_0$ that supports all of $\Phi $ , but not $\psi $ .□

We then have a complete proof system $\vdash _{\textsf {g}'}$ for the general consequence relation of the class of regular matrix frames:

Corollary 4.1 (Completeness wrt regular matrix frames)

$$ \begin{align*}\Phi\models_{\textsf{g}}\psi \Rightarrow \Phi\vdash_{\textsf{g}'}\psi.\end{align*} $$

4.4 Logic of real-world consequence

We have shown that $\Phi \models _{\textsf {g}}\psi \iff \Phi \vdash _{\textsf {g}'}\psi $ , but we still need an inference relation for real-world consequence. The definition we gave for the classical fragment only needs a minor revision:

Definition 4.2 (Real-world inference relation)

The inference relation $\vdash _{\textsf {r}}$ for the real-world consequence relation is defined by:

This generalizes the previous definition to the full inquisitive language: now, any proof in the system $\vdash _{\textsf {g}'}$ , with for all $\varphi \in \Phi $ as premises and as conclusion, counts as a proof of $\psi $ from $\Phi $ in $\vdash _{\textsf {r}}$ .

Then we can show that the logic of real-world consequence is sound and complete.

Theorem 4.2 (Real-world soundness and completeness)

$$ \begin{align*}\Phi\vdash_{\textsf{r}} \psi\iff \Phi\models_{\textsf{r}} \psi.\end{align*} $$