QUESTIONS IN TWO-DIMENSIONAL LOGIC

Abstract

Since Kripke, philosophers have distinguished a priori true statements from necessarily true ones. A statement is a priori true if its truth can be established before experience, and necessarily true if it could not have been false according to logical or metaphysical laws. This distinction can be captured formally using two-dimensional semantics.

There is a natural way to extend the notions of apriority and necessity so they can also apply to questions. Questions either can or cannot be resolved before experience, and either are or are not about necessary facts. Classical two-dimensionalism has no account of question meanings, so it has to be combined with a framework for question semantics in order to capture these observations. It is shown in [14] how two-dimensional semantics can be combined with inquisitive semantics, in which questions are analyzed in terms of information. The present paper investigates the logic of two-dimensional inquisitive semantics, and provides a complete proof system.

1 Introduction

1.1 A priori and necessary truth

An adequate analysis of the meaning of sentences has to make a distinction between a priori and necessary truths [11]. A statement is called a priori true if its truth can be established before experience, which means it is true irrespective of the situation in which it is used. An example is (1):

1. (1) I am here now.

Although every context may provide different referents for ‘I’, ‘here’ and ‘now’, whatever the statement expresses in a context will always be true in that context. This is why we don’t need to have information about what the world is like to know that it is true.

In contrast, a statement is necessarily true if what it expresses could not have been false, according to logical or metaphysical laws. An example is (2):

1. (2) Hesperus is Phosphorus.

Given that ‘Hesperus’ and ‘Phosphorus’ both refer to Venus, this identity statement expresses that Venus is identical to itself, which Kripke considers to be a necessary fact. ¹

A statement can be a priori true but fail to be necessarily true, for instance, because of the indexicals it contains, as is the case in (1). We can tell, purely based on the meaning of the words, that this sentence can only be truthfully stated. On the other hand, the fact that is expressed here might have been false, as the speaker could have been somewhere else at this time.

Conversely, a necessary truth like (2) can fail to be true a priori: without knowledge of what the world is like, we can fail to know that these names refer to the same object, and thus we cannot be certain it is true.

Several authors (Stalnaker [13] and Kaplan [9], among others) have used a two-dimensional semantics in order to formally capture the distinction between necessity and apriority. In a two-dimensional semantics, statements are not evaluated relative to a single index but to a pair of indices. The first index provides the referents for indexicals (and in some cases proper names), while we check whether the sentence is true or false relative to the second index. Although these indices are not always (both) viewed as possible worlds, we will for the sake of simplicity refer to the first index as the actual world and to the second index as the evaluation world.

To check if a statement is necessarily true in a world, we keep the actual world fixed, while varying only the evaluation world. In other words, we check whether the proposition expressed by the statement in the actual world is true in all worlds. To check whether a statement is a priori true, we vary both worlds, but we only look at those pairs in which the actual world and the evaluation world are the same. In this way, we check whether the proposition expressed by the statement in a world is true in that world itself.

We say that a statement is a posteriori if neither the statement itself nor its negation is a priori, and contingent if neither the statement itself nor its negation is necessary.

1.2 A priori and necessary questions

There is a natural way to extend the notions of apriority and necessity so they can also apply to questions. Questions either can or cannot be resolved without knowledge about the world, and either are or are not about necessary facts. For instance, (3) is intuitively a priori:

1. (3) Am I here now?

This question can be resolved without any knowledge of what the world is like, or even who asks the question. But at the same time we would say that, given a context that provides referents for the indexicals, the question whether this person is at that place at that time is contingent, because it can be resolved in more than one way. Now consider (4). Unlike (3), this question cannot be resolved without knowledge of the world:

1. (4) Who am I?

We might fail to have enough information to resolve (4), because we might not know who is speaking. Therefore this question is not a priori. But in this case, given a referent for ‘I’, the question is (on Kripke’s understanding of these notions) about a necessary fact: if identity is necessary, then it is not contingent who I am. ²

Standard two-dimensional semantics cannot capture these facts, because apriority and necessity are defined in terms of truth and questions lack a truth value. In order to overcome this, Van Gessel [14] develops a combination of two-dimensional semantics and inquisitive semantics [3], in which questions are analyzed directly in terms of resolution conditions: the meaning of a question is equated with the set of information states in which it is resolved. In inquisitive semantics, it is natural to generalize the notions of apriority and necessity that already exist in the literature in such a way that they can apply to questions and statements uniformly. While necessary truth and a priori truth are formalized as truth relative to some particular pairs, in two-dimensional inquisitive semantics sentences can be necessarily resolved or a priori resolved, which means being resolved relative to some particular information states.

The present paper is concerned with the logic that this combination gives rise to, which we will call two-dimensional inquisitive logic ( $\textsf {Inq2D}$ ). For simplicity, we will work with the propositional variant here. The main ingredients of this system are an operator with which questions can be formed, as well as three modal operators: apart from apriority and necessity, it has a modal operator for actuality, which plays the role of an indexical. ³

The ‘classical’ (that is, non-inquisitive) variant of this logic is the one described in [6, 7]. I will generalize this system to the inquisitive setting in order to be able to express statements about the necessity and apriority of questions, such as (5), as well as questions about the necessity and apriority of statements and questions, as in (6). ⁴

1. (5) It is a priori whether $\varphi $ .

1. (6)

   1. a. Is it a priori that $\varphi $ ?

   2. b. Is it a priori whether $\varphi $ ?

The rest of this paper is set up as follows. In Section 2 I will introduce the semantics of $\textsf {Inq2D}$ . I will then give an alternative completeness proof for the classical fragment of $\textsf {Inq2D}$ in Section 3. The details of the completeness proof for the full language will be given in Section 4.

2 Two-dimensional inquisitive logic

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 [1]) 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 [6]). 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 [6, 7]. ⁵

Definition 2.2 (Matrix frame)

A matrix frame is a structure $\langle W,R_\square ,R_A,R_\blacksquare \rangle $ , where:

• • $W = W'\times W'$ for some set of worlds $W'$ ;

• • $\langle w,v \rangle R_\square \langle w',v' \rangle \iff w=w'$ ;

• • $\langle w,v \rangle R_A \langle w',v' \rangle \iff w=w'=v'$ ;

• • $\langle w,v \rangle R_\blacksquare \langle w',v' \rangle \iff w'=v'$ .

We define: $D = \{\langle w,v\rangle \in W~|~ w = v \}.$

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 [1]. ⁶

Definition 2.3 (Support conditions)

For $\boxtimes \in \{\square ,A,\blacksquare \}:$ let $\sigma _{\boxtimes }(x) = \{ y~|~ xR_{\boxtimes } y \}$ .

• • $s \models p \iff s \subseteq V(p);$

• • $s \models \bot \iff s = \emptyset ;$

• • $s \models \varphi \wedge \psi \iff s\models \varphi \text { and } s\models \psi ;$

• •

• • $s \models \varphi \rightarrow \psi \iff \text { for all } t\subseteq s: t\models \varphi \text { implies } t\models \psi ;$

• • $s \models \square \varphi \iff \text {for all } \langle w,v \rangle \in s: \sigma _\square ( w,v ) \models \varphi ; $

• • $s \models A\varphi \iff \text {for all } \langle w,v \rangle \in s: \sigma _A( w,v ) \models \varphi ; $

• • $s \models \blacksquare \varphi \iff \text {for all } \langle w,v \rangle \in s: \sigma _\blacksquare ( w,v ) \models \varphi . $

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:

Fact 2.1 (Derived support conditions for $\neg $ , $\vee $ and $\mathord {?}$ )

• • $s \models \neg \varphi \iff \text {for all } \langle w,v\rangle \in s: \langle w,v\rangle \not \models \varphi ;$

• • $s \models \varphi \vee \psi \iff \text {for all } \langle w,v\rangle \in s: \langle w,v\rangle \models \varphi \text { or } \langle w,v\rangle \models \psi ;$

• • $s \models \mathord {?}\varphi \iff s\models \varphi \text { or for all } \langle w,v\rangle \in s: \langle w,v\rangle \not \models \varphi .$

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 $ . ⁷ Thus, what $A\varphi $ expresses can be phrased as ‘in the actual world, the information conveyed by $\varphi $ is true’. ⁸

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

, which is sensitive to issues: ⁹

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: ¹⁰

• • 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 [4], 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.

Definition 2.6 (General consequence)

$\Phi \models _{\textsf {g}}\psi $ iff for all models M and information states s: if $M, s\models \varphi $ for all $\varphi \in \Phi $ then $M,s\models \psi $ .

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):

Definition 2.7 (Real-world consequence)

$\Phi \models _{\textsf {r}}\psi $ iff for all models M and diagonal information states s: if $M, s \models \varphi $ for all $\varphi \in \Phi $ then $M,s \models \psi $ .

This restriction can be motivated by viewing real-world consequence as a specific case of contextual entailment [1]: 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. ¹¹

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:

Fact 2.2.

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 [8].

An interesting observation we can make here is that this property does not hold for $\textsf {Inq2D}$ . ¹² 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 $ . ¹³

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. ¹⁴

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 Completeness proof for the classical fragment

We start by giving a completeness proof for the non-inquisitive fragment of the language. This language $\mathcal {L}_!$ will simply be the -free fragment, generated by the following grammar: ¹⁵

Definition 3.1 (Classical fragment)

$$ \begin{align*}\alpha ::= p ~|~ \bot ~|~ \alpha \wedge \alpha ~|~ \alpha \rightarrow \alpha ~|~ \square\alpha ~|~ A\alpha ~|~ \blacksquare\alpha.\end{align*} $$

The classical fragment of the system consists only of truth-conditional formulas. That is, the support relation between states and formulas can be reduced to the relation of truth between worlds and formulas.

Fact 3.1 (Truth conditions of classical fragment)

The truth conditions of the classical fragment are as follows:

• • $\langle w,v\rangle \models p \iff \langle w,v\rangle \in V(p);$

• • $\langle w,v\rangle \not \models \bot ;$

• • $\langle w,v\rangle \models \alpha \wedge \beta \iff \langle w,v\rangle \models \alpha \text { and } \langle w,v\rangle \models \beta ;$

• • $\langle w,v\rangle \models \alpha \rightarrow \beta \iff \langle w,v\rangle \not \models \alpha \text { or } \langle w,v\rangle \models \beta ;$

• • $\langle w,v\rangle \models \square \alpha \iff \langle w,v\rangle R_\square \langle w',v'\rangle \text { implies } \langle w',v'\rangle \models \alpha ; $

• • $\langle w,v\rangle \models A\alpha \iff \langle w,v\rangle R_A \langle w',v'\rangle \text { implies } \langle w',v'\rangle \models \alpha ; $

• • $\langle w,v\rangle \models \blacksquare \alpha \iff \langle w,v\rangle R_\blacksquare \langle w',v'\rangle \text { implies } \langle w',v'\rangle \models \alpha . $

The truth conditions are indeed the same as the ones given in [7]. ¹⁶ The completeness proof for the classical fragment in the present paper is also similar to the one given there. I will first explain in which steps the proof in the present paper proceeds.

Although we are ultimately interested in the logic of real-world consequence, we start by proving completeness for the logic of general consequence. We will do this by constructing a canonical model for two-dimensional logic. However, this canonical model is itself not a matrix model. We will therefore first introduce a more general class of models, which we will call sliced matrix models.

We will then show that the canonical model of two-dimensional logic is a sliced matrix model, and use this canonical model to prove completeness with respect to sliced matrix frames.

Completeness with respect to regular matrix frames then follows from the fact that sliced matrix models and regular matrix models share the same general consequence relation.

We then have a complete proof system for the general consequence relation, but not yet for the real-world consequence relation. We define the latter in terms of the former and prove completeness.

The strategy in this section is similar to the one in [7], but slightly more direct: a canonical model is given which is not itself a matrix model, but from which a matrix model can be constructed. In [7], this construction takes place in two steps: first, from a point-generated subframe of the canonical model a Restall frame is constructed [12]. Second, it is shown that every Restall frame is a bounded morphic image of a matrix frame. In the present paper, the canonical model is a sliced matrix model, and only one step is needed to construct a matrix model.

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) [7]. 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 [1]. ¹⁷ 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.

Definition 3.2 (Sliced matrix model)

A sliced matrix model M is a structure $\langle W,R_\square ,R_A,R_\blacksquare ,V\rangle $ where:

• • $R_\blacksquare $ connects pairs to some subset of D rather than to all of D:

  $$ \begin{align*}\langle w,v \rangle R_\blacksquare \langle w',v' \rangle \Rightarrow \langle w',v' \rangle\in D.\end{align*} $$

• • Pairs are at least related to the actual pair on their own row:

  $$ \begin{align*}\text{For any}\ w,v:\ \langle w,v \rangle R_\blacksquare \langle w,w \rangle.\end{align*} $$

• • $R_\blacksquare $ is transitive and euclidean (positive and negative introspection).

• • All other elements of the structure are defined as in regular matrix models.

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.

Definition 3.3 (Sliced consequence)

$\Phi \models _{\textsf {s}}\psi $ iff for all sliced models M and states s: if $M, s\models \varphi $ for all $\varphi \in \Phi $ , then $M,s\models \psi $ .

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*} $$

Proof. The following are theorems of $\vdash _{\textsf {g}}$ and therefore members of any maximally consistent set:

1. T1 $A\alpha \rightarrow AA\alpha ;$ (by A15 and A14)

2. T2 $AA\alpha \rightarrow A\alpha .$ (by A19, A18 and R3)

From (T1) and (T2) it follows that $AA\alpha \in \Gamma $ just in case $A\alpha \in \Gamma $ , so $(\Gamma _A)_A = \Gamma _A$ . By Definition 3.4, $\textsf {t}(\Gamma _A,\Gamma )$ is either $\Gamma $ or $\Gamma _A$ , but the latter can only be the case if $\Gamma _A = \Gamma $ .□

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*} $$

Proof. By Definition 3.4, $\textsf {t}(\Gamma ,\Delta )$ is either $\Gamma _A$ or $\Delta $ . In the former case, $A\alpha \in \Gamma _A$ iff $AA\alpha \in \Gamma $ iff (by T1 and T2) $A\alpha \in \Gamma $ iff $\alpha \in \Gamma _A$ . In the latter case, $\Gamma _A=\Delta _A$ . $A\alpha \in \Delta $ iff $\alpha \in \Delta _A$ iff $\alpha \in \Gamma _A$ .□

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

Definition 3.5 (Canonical sliced matrix model)

Let $M^c = \langle W^c,R^c_\square ,R^c_A,R^c_\blacksquare ,V^c\rangle $ , where:

• • $W^c = T^c \times T^c$ ;

• • $R^c_\square $ and $R^c_A$ are defined as in any sliced matrix model;

• • $\langle \Gamma ,\Delta \rangle R^c_\blacksquare \langle \Gamma ',\Delta '\rangle \iff \Gamma '=\Delta '\text { and } {\{\alpha ~|~\blacksquare \alpha \in \textsf {t}(\Gamma ,\Delta )\} \subseteq \textsf {t}(\Gamma ',\Delta ')}$ ;

• • $\langle \Gamma ,\Delta \rangle \in V(p) \iff p \in \textsf {t}(\Gamma ,\Delta )$ .

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*} $$

Proof. By induction on the complexity of $\alpha $ . I give only the case for $\boxtimes \alpha $ (for $\boxtimes \in \{\square ,A,\blacksquare \}$ ). The following theorems of $\vdash _{\textsf {g}}$ will be used:

1. T3 $\square \alpha \rightarrow A\square \alpha $ ; (by A11, A12, R2 and R3)

2. T4 $A\square \alpha \rightarrow \alpha $ . (by A13, A14 and A12)

1. (⇐) Assume $\boxtimes \alpha \in \textsf {t}(\Gamma ,\Delta )$ . Then take an arbitrary pair $\langle \Gamma ',\Delta '\rangle $ such that $\langle \Gamma ,\Delta \rangle R^c_{\boxtimes } \langle \Gamma ',\Delta '\rangle $ . We need to show that $M^c,\langle \Gamma ',\Delta '\rangle \models \alpha $ .

   1. (□) If $\square \alpha \in \textsf {t}(\Gamma ,\Delta )$ , by (T3) we have $A\square \alpha \in \textsf {t}(\Gamma ,\Delta )$ . Then by Lemma 3.2, $\square \alpha \in \Gamma _A$ . Since $\Gamma ' = \Gamma $ , $\square \alpha \in \Gamma ^{\prime }_A$ , so by Lemma 3.2, $A\square \alpha \in \textsf {t}(\Gamma ',\Delta ')$ . It follows by (T4) that $\alpha \in \textsf {t}(\Gamma ',\Delta ')$ .

   2. (A) In this case, $\Gamma '=\Delta '=\Gamma $ . By Definition 3.4, $\textsf {t}(\Gamma ',\Delta ') = \Gamma _A$ . It follows from Lemma 3.2 that if $A\alpha \in \textsf {t}(\Gamma ,\Delta )$ then $\alpha \in \Gamma _A$ .

   3. (■) It follows from the definition of $R^c_\blacksquare $ that $\alpha \in \textsf {t}(\Gamma ',\Delta ')$ .

      By the induction hypothesis, $M^c,\langle \Gamma ',\Delta '\rangle \models \alpha $ .

2. (⇒) For the left to right case, assume $\boxtimes \alpha \not \in \textsf {t}(\Gamma ,\Delta )$ . Then $\neg \boxtimes \alpha \in \textsf {t}(\Gamma ,\Delta )$ . So we need to find some $\langle \Gamma ',\Delta '\rangle $ such that $\langle \Gamma ,\Delta \rangle R^c_{\boxtimes } \langle \Gamma ',\Delta '\rangle $ and $M^c,\langle \Gamma ',\Delta '\rangle \not \models \alpha $ .

   Let $\Delta ^- = \{\neg \alpha \} \cup \{\beta ~|~\boxtimes \beta \in \textsf {t}(\Gamma ,\Delta )\}$ . Then $\Delta ^-$ is consistent. If not, then $\{\beta ~|~\boxtimes \beta \in \textsf {t}(\Gamma ,\Delta )\}\vdash _{\textsf {g}}\alpha $ . But then $\{\boxtimes \beta ~|~\boxtimes \beta \in \textsf {t}(\Gamma ,\Delta )\}\vdash _{\textsf {g}}\boxtimes \alpha $ , and this contradicts the assumption that $\neg \boxtimes \alpha \in \textsf {t}(\Gamma ,\Delta )$ . Let $\Delta '$ be any maximally consistent set extending $\Delta ^-$ .

   The next step is to show that there exists a pair $\langle \Gamma ',\Delta ' \rangle $ such that $\Delta ' = \textsf {t}(\Gamma ',\Delta ')$ and $\langle \Gamma ,\Delta \rangle R^c_{\boxtimes } \langle \Gamma ',\Delta '\rangle $ .

   1. (□) We show that $\Delta ' = \textsf {t}(\Gamma ,\Delta ')$ . This follows from the definition of $\textsf {t}$ and the fact that $\Gamma _A = \Delta ^{\prime }_A$ : if $\alpha \in \Gamma _A$ , then by Lemma 3.2, $A\alpha \in \textsf {t}(\Gamma ,\Delta )$ . By axiom (A15), it follows that $\square A\alpha \in \textsf {t}(\Gamma ,\Delta )$ . Then by construction of $\Delta '$ , $\square A\alpha \in \Delta '$ . It follows from axiom (A14) that $A\alpha \in \Delta '$ and thus $\alpha \in \Delta ^{\prime }_A$ . Conversely, if $\alpha \not \in \Gamma _A$ , then $\neg \alpha \in \Gamma _A$ , and from the previous part of the proof it follows that $\neg \alpha \in \Delta ^{\prime }_A$ , so $\alpha \not \in \Delta ^{\prime }_A$ .

   2. (A) In this case, $\Delta ^-$ is already a maximally consistent set by definition. Furthermore, it is defined in such a way that $\Delta ^- = \Gamma _A$ . Thus $\Delta '=\Gamma _A = \textsf {t}(\Gamma ,\Gamma )$ .

   3. (■) By construction, $\Delta '$ contains $A\alpha \rightarrow \alpha $ for any $\alpha $ , due to (A19), so it is easy to show that $\Delta '=\Delta ^{\prime }_A$ . This means that $\Delta ' = \textsf {t}(\Delta ',\Delta ')$ , and since $\{\alpha ~|~\blacksquare \alpha \in \textsf {t}(\Gamma ,\Delta )\} \subseteq \textsf {t}(\Delta ',\Delta ')$ , we have by definition of $R^c_\blacksquare $ that $\langle \Gamma ,\Delta \rangle R^c_\blacksquare \langle \Delta ',\Delta '\rangle $ .

   Thus we have found a $\langle \Gamma ',\Delta ' \rangle $ such that $\langle \Gamma ,\Delta \rangle R^c_{\boxtimes } \langle \Gamma ',\Delta '\rangle $ and $\alpha \not \in \textsf {t}(\Gamma ',\Delta ')$ . By induction hypothesis it follows that $M^c,\langle \Gamma ',\Delta ' \rangle \not \models \alpha $ . Therefore $M^c,\langle \Gamma ,\Delta \rangle \not \models \boxtimes \alpha $ .□

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*} $$

Proof. Suppose $\Gamma \not \vdash _{\textsf {g}}\alpha $ . Then $\Gamma \cup \{\neg \alpha \}$ is consistent, so there exists a maximally consistent set $\Delta $ such that $\Gamma \subseteq \Delta $ but $\alpha \not \in \Delta $ . By Lemma 3.1, $\Delta = \textsf {t}(\Delta _A,\Delta )$ , thus we have a pair in the canonical model such that, by the truth lemma, $M^c,\langle \Delta _A,\Delta \rangle \models \Gamma $ but $M^c,\langle \Delta _A,\Delta \rangle \not \models \alpha $ .

By finding a pair which makes $\Gamma $ true and $\alpha $ false we also found an information state that supports $\Gamma $ but not $\alpha $ , namely the singleton state consisting only of that pair. Therefore, $\Gamma \not \models _{\textsf {s}}\alpha $ .□

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 $ . ¹⁸ □

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*} $$

Proof. Immediate by Definition 3.6, Fact 2.2 and the fact that and $A\alpha $ are equivalent for classical formulas $\alpha $ .□

4 Extending completeness to the full language

Having obtained a completeness proof for the classical fragment of $\textsf {Inq2D}$ , it remains to be shown that this result can be extended to the inquisitive setting.

It is shown in [1] how this can be done for any normal modal logic. Although the logic of real-world consequence is not a normal modal logic (there are validities $\varphi $ for which $\square \varphi $ is not valid), the logic of general consequence is, which means we should again take the logic of general consequence as a starting point.

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 [1], we can define resolutions for the whole language of $\textsf {Inq2D}$ as follows:

Definition 4.1 (Resolutions)

• • $\mathcal {R}(\alpha ) = \{\alpha \}$ if $\alpha $ is -free;

• • $\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$ is a function from $\mathcal {R}(\varphi )\text { to } \mathcal {R}(\psi )\};$

• •

• • $\mathcal {R}(\square \varphi ) = \{\bigvee _{\alpha \in \mathcal {R}(\varphi )}\square \alpha \};$

• • $\mathcal {R}(A\varphi ) = \{\bigvee _{\alpha \in \mathcal {R}(\varphi )}A\alpha \};$

• • $\mathcal {R}(\blacksquare \varphi ) = \{\bigvee _{\alpha \in \mathcal {R}(\varphi )}\blacksquare \alpha \}.$

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: ¹⁹

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*} $$

Proof sketch. The crucial direction is from left to right. Suppose $\Phi \models _{\textsf {s}}\psi $ and take any $\Gamma \in \mathcal {R}(\Phi )$ . Then $\Gamma $ entails any formula in $\Phi $ , so $\Gamma \models _{\textsf {s}}\psi $ . This means that .

Now suppose toward a contradiction that there is no $\alpha \in \mathcal {R}(\psi )$ such that $\Gamma \models _{\textsf {s}}\alpha $ . Then for each $\alpha \in \mathcal {R}(\psi )$ there exists a sliced model $M_\alpha $ and state $s_\alpha $ such that $M_\alpha ,s_\alpha \models \gamma $ for all $\gamma \in \Gamma $ but $M_\alpha ,s_\alpha \not \models \alpha $ .

Then from these sliced models we can construct a new sliced model M, the domain of which is $W'\times W'$ , where $W'$ is the disjoint union of the worlds of all original models $M_\alpha $ for $\alpha \in \mathcal {R}(\psi )$ . We define $V( w,v)$ as $V_\alpha ( w,v)$ if $\langle w,v\rangle $ is a pair in $M_\alpha $ , and as $V_\alpha ( w,w)$ otherwise. As $R_\blacksquare $ we take the union of all $R^\alpha _\blacksquare $ , and the other relations are defined as normal. Let s be the union of the states $s^\alpha $ .

Then a simple proof by induction on the structure of formulas shows that the formulas which s of M supports are the formulas that all individual states $s_\alpha $ out of which it was built support. Thus we have $M,s\models \gamma $ for all $\gamma \in \Gamma $ and $M,s\not \models \alpha $ for all $\alpha \in \mathcal {R}(\psi )$ . So $M,s\not \models \psi $ . As this contradicts the assumption that $\Gamma \models _{\textsf {s}}\psi $ , we are done.□

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}}$ . ²⁰ 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*} $$

Proof. The left to right direction is Lemma 6.4.12 of [1]. The other direction follows immediately from his Lemmas 6.4.14 and 6.4.19.□

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): ²¹

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*} $$

Proof. Suppose $\Phi \models _{\textsf {g}}\psi $ . By Lemma 4.3, we obtain $\Phi ,\Delta _{A20}\models _{\textsf {s}}\psi $ . By Theorem 4.1 we have that $\Phi ,\Delta _{A20}\vdash _{\textsf {g}}\psi $ . Since all formulas in $\Delta _{A20}$ are axioms in $\vdash _{\textsf {g}'}$ , it follows that $\Phi \vdash _{\textsf {g}'}\psi $ .□

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*} $$

Proof. Immediate by Fact 2.2.□

5 Conclusion

Apart from giving an alternative completeness proof for the classical two-dimensional logic in [7], we have shown that the logic can be extended in a natural way to a setting in which questions play a role: this allows us to express questions and statements about the apriority, necessity and actuality of questions as well as statements. We have observed that $\textsf {Inq2D}$ does not have the disjunction property. This is caused by the fact that the question whether a formula is a priori is valid on any model, even though models can differ in whether they make this formula a priori or not. We have given a sound and complete proof system for $\textsf {Inq2D}$ .

This system can be extended in many ways: an obvious next step would be to add a knowledge operator K and investigate the interaction between apriority, necessity and knowledge, but it would also be interesting to add its inquisitive counterpart, the ‘entertain’ operator E/ $\boxplus $ (see [1]), which is sensitive to issues of agents.