An Axiomatic System and a Tableau Calculus for STIT Imagination Logic

Abstract

We formulate a Hilbert-style axiomatic system and a tableau calculus for the STIT-based logic of imagination recently proposed in Wansing (2015). Completeness of the axiom system is shown by the method of canonical models; completeness of the tableau system is also shown by using standard methods.

1 Introduction

There exists an important difference between imagination and the propositional attitudes of belief and knowledge. Whilst it is widely assumed that, as a matter of psychological fact, it is impossible for agents to form beliefs at will, it seems to be clear that imagination may operate in voluntary mode. However, until recently the agentiveness of imagination has not been accounted for in the sparse literature on the logic of imagination ascriptions. Both I. Niiniluoto [10] and A. Costa Leite [8] treat expressions of the form ‘agent j imagines that’ as normal modal operators. Also, there is disagreement concerning the extent to which imagination is regulated by logical principles. Modelling imagination as a normal modality comes with the commitment to a number of properties that in analogy to the well-known problem of logical omniscience in epistemic logic may be said to give rise to a problem of logical omni-imagination. Imagination then is closed under valid implication and imagined implication. Moreover, all valid propositions of the underlying non-modal logic are imagined. This may be seen as a rather strong idealization and as being descriptively inadequate. According to some authors, such as G. Priest [11], imagination even fails to be governed by any logical principles.

A position intermediate between these two extremes is adopted in [18], where the semantics of a propositional logic of imagination ascriptions for single agents has been motivated and introduced. The main feature of this approach is that ‘to imagine’ is seen as an action verb. It is assumed that subjects often and typically have direct control over their imaginations. This idea suggests to model imagination ascriptions by using the modal logic of agency, more concretely the seeing-to-it-that (STIT) theory developed by N.D. Belnap, M. Perloff, M. Xu, F. von Kutschera, and J. Horty, cf. [2, 6] and the references given there. In [18] it is argued that imagination is closed under valid equivalence, and the suggested STIT imagination logic is compared with Niiniluoto’s [10] semantics of imagination ascriptions. The semantics of the agentive imagination operator merges the semantics of the dstit-operator from STIT theory and the interpretation of the necessity operator in the smallest classical modal logic E, see [4]. As a result, imagination is closed under valid equivalence. In this framework, propositional content is represented by sets of moment/history-pairs. The point is not that propositions are necessarily to be identified with sets of moment/history-pairs, but that for imagination we have closure under some criterion of propositional identity. This conception agrees with understanding imagination in terms of mental pictures that are assumed to comprise propositional content. If an agent a imagines that B, and B is logically equivalent with C, then the mental picture that a creates in her or his act of imagining that B does not differ from the picture created by imagining that C, cf. [18].¹

In the present paper, we provide two different kinds of proof systems for the semantically introduced logic of imagination: a Hilbert-style axiomatization and a tableau calculus. Both systems offer algorithmic insight into the STIT imagination logic. We shall not repeat the motivating considerations from [18] but otherwise keep the paper self-contained. Whereas in [18] the focus is on introducing the semantics of the modal imagination operators, in the present paper we include other modal operators as well.

2 Semantics

We first present the language of propositional STIT imagination logic and assume a countably infinite set V a r of propositional variables, the connectives ¬ (negation), ∧ (conjunction),² and the following set of modalities:

• 1. S A understood as ‘ A is settled true’; the dual modality is P A understood as ‘A is possible’.

• 2. [c] _a A understood as ‘agent a c s t i t-realizes A’; another action modality, namely, [d] _a A to be read as ‘agent a d s t i t-realizes A’, is in this setting a defined one with the following definition: [c] _a A ∧ ¬S A.

• 3. I _a A understood as ‘agent a imagines that A’.

All the agent indices are assumed to stand for pairwise different agents. For these modalities we assume the following ‘stit-plus-neighbourhood’ semantics defined in [18].

An imagination model is a tuple $\mathcal {M} = \langle Tree, \leq , Ag, Choice, \{ N_{a}\mid a \in Ag \}, V\rangle$, where:

• T r e e is a non-empty set of moments, and ≤ is a partial order on T r e e such that

  $$\forall m_{1},m_{2}\exists m(m \leq m_{1} \wedge m \leq m_{2}),$$

  and

  $$\forall m_{1},m_{2},m((m_{1} \leq m \wedge m_{2} \leq m) \to (m_{1} \leq m_{2} \vee m_{2} \leq m_{1})).$$

• The set H i s t o r y of all histories of $\mathcal {M}$ is then just the set of all maximal ≤-chains in T r e e. A history h is said to pass through a moment m iff m ∈ h. The set of all histories passing through m ∈ T r e e is denoted by H _m .

• A g is a finite set of all agents acting in T r e e and is assumed to be disjoint from all the other items in $\mathcal {M}$. The set A g is fixed for the language of STIT imagination logic and does not vary from model to model.

• C h o i c e is a function defined on the set T r e e×A g, such that for an arbitrary (m, a) ∈ T r e e×A g, the value of this function, that is to say C h o i c e(m, a) (more commonly denoted $Choic{e^{m}_{a}}$) is a partition of H _m . If h ∈ H _m , then $Choic{e^{m}_{a}}(h)$ denotes the element of $Choic{e^{m}_{a}}$ to which h belongs. In the special case when we have $Choic{e^{m}_{a}} = \{ H_{m} \}$, it is said that the agent a has a vacuous choice at the moment m. In our models, C h o i c e is assumed to satisfy the following two restrictions:

  • “No choice between undivided histories”: for arbitrary m ∈ T r e e, a ∈ A g, e∈$Choic{e^{m}_{a}}$, and h, h ^′ ∈ H _m :

    $$(h \in e \wedge \exists m^{\prime}(m < m^{\prime} \wedge m^{\prime} \in h \cap h^{\prime})) \to h^{\prime} \in e.$$

  • “Independence of agents”. If f is a function defined on A g such that ∀a ∈ A g $(f(a) \in Choic{e_{a}^{m}})$, then $\bigcap _{a \in Ag}f(a) \neq \varnothing$.

• The set of moment/history-pairs in $\mathcal {M}$, that is to say, the set

  $$MH(\mathcal{M}) = \{ (m, h) \mid m \in Tree, h \in H_{m} \}$$

  is then to be used as a set of points, where formulas are evaluated.

• For every a ∈ A g, we have N _a : $MH(\mathcal {M}) \to 2^{(2^{MH(\mathcal {M})})}$. N _a is thus a neighbourhood function, defining, for every moment history pair (m, h) the set of propositions imagined by the agent a at the moment m in history h.

• V is an evaluation function for atomic sentences, i.e., $V{\hspace {0.25mm}:\hspace {0.25mm}} Var \to 2^{MH(\mathcal {M})}$.

Definition 1

The relation of satisfaction of sentences in the above defined language at moment/history-pairs in an imagination model $\mathcal {M}$ is then defined inductively as follows:

$$\begin{array}{@{}rcl@{}} \mathcal{M}, (m,h) &\vDash& p \Leftrightarrow (m,h) \in V(p), \text{ for atomic \(p\);} \\ \mathcal{M}, (m,h) &\vDash& (A \wedge B) \Leftrightarrow \mathcal{M}, (m,h) \vDash A \text{ and } \mathcal{M}, (m,h) \vDash B;\\ \mathcal{M}, (m,h) &\vDash& \neg A \Leftrightarrow \mathcal{M}, (m,h) \not\vDash A;\\ \mathcal{M}, (m,h) &\vDash& SA \Leftrightarrow \forall h^{\prime} \in H_{m}(\mathcal{M}, (m,h^{\prime}) \vDash A);\\ \mathcal{M}, (m,h) &\vDash& [c]_{a}A \Leftrightarrow \forall h^{\prime} \in Choic{e^{m}_{a}}(h)(\mathcal{M}, (m,h^{\prime}) \vDash A);\\ \mathcal{M}, (m,h) &\vDash& I_{a}A \Leftrightarrow \forall h^{\prime} \in Choic{e^{m}_{a}}(h)\\ &&(\{ (m^{\prime},h^{\prime\prime\prime}) \in MH(\mathcal{M}) \mid \mathcal{M}, (m^{\prime},h^{\prime\prime\prime}) \vDash A \} \in N_{a}((m,h^{\prime}))) \text{ and } \\ &&\exists h^{\prime\prime} \!\in\! H_{m} (\{ (m^{\prime},h^{\prime\prime\prime}) \in MH(\mathcal{M}) \mid \mathcal{M}, (m^{\prime},h^{\prime\prime\prime}) \!\vDash\! A \} \notin N_{a}((m,h^{\prime\prime}))). \end{array} $$

If by $\Vert A \Vert _{{\mathcal M}}$ we denote the set $\{ (m,h) \in MH(\mathcal {M}) \mid \mathcal {M}, (m,h) \vDash A \}$, i.e., the truth set of A in model ${\mathcal M}$, then the above satisfaction clause for formulas I _a A can more compactly be rewritten as:

$$\mathcal{M}, (m,h) \vDash I_{a}A \; \Leftrightarrow \; $$

$$\forall h^{\prime} \in Choic{e^{m}_{a}}(h) \, (\Vert A \Vert_{{\mathcal M}} \in N_{a}((m,h^{\prime}))) \text{ and } \exists h^{\prime\prime} \in H_{m} \, (\Vert A \Vert_{{\mathcal M}} \notin N_{a}((m,h^{\prime\prime}))). $$

A picture may help to familiarize oneself with the semantics, see Fig. 1.

Definition 2

A formula is said to be valid in an imagination model ${\mathcal M}$ iff A is satisfied by every moment/history-pair in $\mathcal {M}$, and A is said to be valid (simpliciter) iff A is valid in every imagination model.

The language of STIT imagination logic, as presented here, does not contain temporal operators. Therefore, it may seem natural to use the alternative, atemporal Kripke STIT semantics developed in [1] for single agents (and in [9] for collective agents) and to extend it by neighbourhood functions. This is a legitimate move, but we refrain from making it because we view the branching-time structures augmented by agent choice functions as the intended semantics of STIT theory.

Fig. 1

Two choice-cells of the single agent a at moment m; {h ₁, h ₂, h ₃, h ₄} = H _m ; $(m,h_{1}) \vDash I_{a}A$ and $(m,h_{2}) \vDash I_{a}A$; ∥A∥ ∉ N _a ((m, h ₃)); $(m,h_{4}) \not \vDash I_{a}A$

Note that in [18] it has been pointed out that I _a A can be defined as [d] _a □ _a A (notation adjusted), where □ _a A is true in a model $\mathcal M$ at moment/history-pair (m, h) iff $\Vert A \Vert _{{\mathcal M}} \in N_{a} (m,h)$. The latter can be understood as saying that the proposition expressed by A belongs to the set of propositions contained in s’s mental image at (m, h) in model $\mathcal M$. There are, however, reasons to take the operators I _a as primitive connectives. T. Williamson [13] considers imagination as working in voluntary and involuntary mode. Treating I _a as primitive guards against misinterpreting [d] _a □ _a A as saying that agent a sees to it that a imagines in involuntary mode that A, which could be made true by performing some indirect actions, such as taking drugs, so as to make sure that □ _a A is the case. If imagining is seen as a homogeneous activity, it seems natural to consider the non-normal modal operator □ _a as incorporated in the primitive agentive operator I _a .³

3 Axiomatization

For the semantically presented logic we propose the following axiomatization:

• (A0) Propositional tautologies.

• (A1) S is an S5 modality.

• (A2) For every a ∈ A g, [c] _a is an S5 modality.

• (A3) S A → [c] _a A for every a ∈ A g.

• (A4) $(P[c]_{a_{1}}A_{1} \wedge {\ldots } \wedge P[c]_{a_{n}}A_{n}) \to P([c]_{a_{1}}A_{1} \wedge \ldots \wedge [c]_{a_{n}}A_{n})$, provided that all the a ₁…a _n are pairwise different.

• (A5) I _a A → ([c] _a I _a A ∧ ¬S I _a A) for every a ∈ A g.

Rules are as follows:

• (R1) Modus ponens.

• (R2) From A infer S A.

• (R3) From A⇔B infer I _a A⇔I _a B for every a ∈ A g.

Note

Observe that (A4) actually is a family of schemas parametrized by n. The above axiomatization is just the axiomatization of d s t i t logic proposed by Ming Xu plus the axiomatization of the logic of I _a as a minimal neighbourhood modal system for the smallest classical (or congruential) modal logic E plus the special axiom (A5) stating the agentive character of the imagination operator. Note also that the converse of (A5) easily follows from (A2), so that we actually have a biconditional here.

The above axiomatization can easily be show to be sound with respect to the class of all imagination models. Our aim now is to get a strong completeness theorem for this system L with respect to the above semantics, in the following form: if Θ is an L-consistent set of sentences, then Θ has a model.

In what follows we will always use ‘consistency’ to mean ‘ L-consistency’ and we let ⊩ stand for the relation of L-derivability.

In order to get the main theorem, we use the technique of canonical models, which is an adaptation of the corresponding techniques for the two respective parts of our system as mentioned in the Note above. In particular, we draw on [2](@var1@ch. 17@var1@) in many matters relevant to the pure STIT part of the following construction.

More precisely, we let W to be the set of all L-maxiconsistent sets of sentences and we denote the members of W as w, w ^′, w ₁ etc. We set w R w ^′ iff {A∣S A ∈ w} ⊆ w ^′, and we set w≃ _a w ^′ iff {A∣[c] _a A ∈ w} ⊆ w ^′. By standard modal logic, (A1) and (A2) ensure that all these relations are relations of equivalence; moreover, (A3) ensures that ≃ _a ⊆ R for every a ∈ A g.

Indeed, let w≃ _a w ^′ and let S A ∈ w. By (A3) and maxiconsistency of w, we get [c] _a A ∈ w, whence by w≃ _a w ^′ we get that A ∈ w ^′. Since A was arbitrary, this means that w R w ^′.

In the sequel, we will be denoting equivalence classes of W with respect to R by X, X ^′, X ₁, etc. The set of all such equivalence classes will be denoted by Ξ. When restricted to an arbitrary X∈Ξ, the relation R turns into the universal relation, but relations of the form ≃ _a can remain non-trivial equivalences breaking X up into several equivalence classes. We will denote the family of equivalence classes corresponding to $\simeq _{a}\upharpoonright X$ by E(X, a).

For the construction of the canonical model below, we will need to pick among the elements of W a maxiconsistent set which is the only element of the respective R- and ∼ _a -equivalence classes. In order to do this, we consider maxiconsistent sets extending the following set of formulas:

$${\Sigma} \,=\, \{ \neg p \mid p \in Var \} \cup \{ SA \leftrightarrow A \mid \text{ for arbitrary }A \} \cup \{ [c]_{a}A \leftrightarrow A \mid \text{ for arbitrary }A \}. $$

The following facts are worth noting:

• (F1) There exists exactly one element in W, which extends Σ. We will denote this element by w. Indeed, one easily sees that Σ pre-determines every non-modal formula by fixing the literals. The modalities S and [c] _a are then just vacuous in virtue of the definition of Σ. Finally, every maxiconsistent set extending Σ will have to contain ¬I _a A for every formula A and every a ∈ A g. For suppose otherwise. Then for some w ∈ W such that Σ ⊆ w, for some formula A and for some a ∈ A g we will have I _a A ∈ w. Then, by (A5) and maxiconsistency of w we will get ¬S I _a A ∈ w. Therefore, by definition of Σ and maxiconsistency of w, we will get ¬I _a A ∈ w, which contradicts the assumption that w ∈ W. Therefore, the statements beginning with I _a -modalities are also fixed for every w ∈ W, for which Σ ⊆ w. It is also easy to see that such a maxiconsistent w extending Σ must exist, since Σ itself is obviously consistent⁴

• (F2) It follows from the definitions of Σ and R that the R-equivalence set containing w contains w only. We will denote this equivalence set by X.

We now proceed to the definition of our canonical model, which will be based on a tree of depth 2. First, we choose⁵ an element 0 ∉ Ξ ∪ W and define our set of moments:

$$Tree = \{ 0 \} \cup {\Xi} \cup W.$$

We then set the following partial order on T r e e. For arbitrary x, y ∈ T r e e we have x≤y iff x = y, or y ∈ x or x = 0. This allows for a simple description of the set of histories in our frame. Every history turns out to have the form h _w =〈0,X, w〉, where X∈Ξ and w ∈ X. Thus, our set of histories is in one-to-one correspondence with W.

Thirdly, we define the choice function. It assigns a vacuous choice to every agent at every moment m, if m ∉ Ξ. That is to say, the only choice of every agent at every such moment will be just the set of all histories passing through this moment. Otherwise, i.e. for the case when m = X∈Ξ, we define the choice function as follows:

$$Choic{e_{a}^{X}} = \{ H \mid \exists e \in E(X,a)(H = \{ h_{w} \mid w \in e \}) \}. $$

Next, we need to define the imagination neighbourhoods. We do this in the following way. $N_{a}((m,h)) = \varnothing$ for every a ∈ A g and every m ∉ Ξ. For the case when m = X∈Ξ, we need one further auxiliary notion. For every sentence A we set E x t(A) (read: ‘the extension of A) to be {(X, h _w )∣A ∈ w ∈ X} if A ∉ w; otherwise we set

$$Ext(A) = \{ (X, h_{w})\mid A\in w\in X \} \cup \{ (m,h_{w}) \mid m \notin {\Xi} \text{ and } m \in h_{w} \}. $$

Having defined the extensions, we set

$$N_{a}((X, h_{w})) = \{ Ext(A) \mid I_{a}A \in w \} $$

for arbitrary w ∈ X∈Ξ.

Finally, we define the evaluation function for variables in the following way:

$$V(p) = \{ (X, h_{w})\mid p \in w\in X \in {\Xi} \}. $$

We need to show that the canonical model $\mathcal {M}$ defined above is a model of our logic. The semantic restrictions are mostly seen to hold immediately; in particular, the no-choice-between-undivided-histories restriction holds because we only have undivided histories at the moment 0, where only vacuous choices are allowed. The only exception is the independence-of-agents restriction, which we treat below.

Lemma 1 (On Independence)

Let m∈Tree and let f be a function on Ag such that ∀a∈Ag $(f(a) \in Choic{e_{a}^{m}})$ . Then $\bigcap _{a \in Ag}f(a) \neq \varnothing$.

Proof

If m ∉ Ξ, then the statement of the lemma is obvious, since every agent will have a vacuous choice. We treat the case when m = X∈Ξ. Consider a function f as described in the lemma. For every f(a) we fix e _f(a) ∈ E(X, a) such that f(a)={h _w ∣w ∈ e _f(a)} and we fix, further, an arbitrary w _f(a) ∈ e _f(a). Since e _f(a) is an ≃ _a -equivalence class, there is a set Γ _f(a) of sentences of the form [c] _a A shared by all the members of e _f(a) and only those members. Also, since X is an R-equivalence class, there is a set Δ of sentences of the form S A shared by all (and only) members of X. Consider, then, the following set of sentences:

$${\Lambda} = (\bigcup\limits_{a \in Ag}{\Gamma}_{f(a)}) \cup {\Delta}. $$

We claim that Λ is consistent. Assume otherwise. In this case Λ contains a finite inconsistent subset. Given that S and [c] _a are S5-modalities, we can assume that this inconsistent subset has the following elements:

$$SB, [c]_{a_{1}}A_{1},\ldots, [c]_{a_{n}}A_{n},$$

where all the a ₁…a _n are pairwise different (and moreover, A g = {a ₁…a _n }). We know, further, that for all 1≤i≤n we have $SB, [c]_{a_{i}}A_{i} \in w_{f(a_{i})}$. So, choose an arbitrary w ∈ X. For every 1≤i≤n we have $w_{f(a_{i})}Rw$, therefore, we must also have $P[c]_{a_{i}}A_{i} \in w$ for every 1≤i≤n. Indeed, if it were otherwise, we would have $S\neg [c]_{a_{i}}A_{i} \in w$ since w is maxiconsistent. But then, given that $wRw_{f(a_{i})}$, we would have $\neg [c]_{a_{i}}A_{i} \in w_{f(a_{i})}$, a contradiction.

Thus, we have in fact that

$$P[c]_{a_{1}}A_{1}\wedge{\ldots} \wedge P[c]_{a_{n}}A_{n} \in w, $$

therefore, by (A4), we also have

$$P([c]_{a_{1}}A_{1}\wedge{\ldots} \wedge [c]_{a_{n}}A_{n}) \in w. $$

This, in turn, means that the set

$$\{ A \mid SA \in {\Delta} \} \cup \{ [c]_{a_{1}}A_{1}\wedge{\ldots} \wedge [c]_{a_{n}}A_{n} \} $$

is consistent: otherwise, we would have that

$$\{ A \mid SA \in {\Delta} \} \vdash \neg([c]_{a_{1}}A_{1}\wedge{\ldots} \wedge [c]_{a_{n}}A_{n}), $$

and, by standard modal S5-reasoning, that

$${\Delta} \vdash S\neg([c]_{a_{1}}A_{1}\wedge{\ldots} \wedge [c]_{a_{n}}A_{n}), $$

which, given that w ∈ X and hence Δ ⊆ w, would mean inconsistency of w, a contradiction.

Therefore, we may choose an arbitrary maxiconsistent w ^′ extending {A∣S A∈Δ} ∪$\{ [c]_{a_{1}}A_{1}\wedge {\ldots } \wedge [c]_{a_{n}}A_{n} \}$, and by the fact that this set contains {A∣S A∈Δ} we know that w R w ^′ and thus w ^′ ∈ X and further S B ∈ w ^′. This means that our finite subset in fact has a model and is not inconsistent. Therefore, since the finite set was arbitrary, Λ is consistent as well. Consider, then, an arbitrary maxiconsistent w ^″ extending Λ. Since Δ ⊆ w ^″, we have w ^″ ∈ X, and since Γ _f(a) ⊆ w ^″ for arbitrary a ∈ A g, we have w ^″≃ _a w _f(a) for every such a. This means, in turn, that w ^″ ∈ e _f(a) for every a ∈ A g, and so $h_{w^{\prime \prime }} \in \bigcap _{a \in Ag}f(a) \neq \varnothing$. □

By now, the only ingredient to be added is the Truth Lemma; we divide it into two parts as follows.

Lemma 2 (Truth Lemma 1)

Let m ∉ Ξ and m ∈ h. Then, for any sentence A, the following holds:

$$\mathcal{M}, (m,h) \vDash A \Leftrightarrow A \in \mathbf{w}.$$

Proof

We use induction on the construction of A. If A = p ∈ V a r, then A ∉ w, and also (m, h) ∉ V(A), since m ∉ Ξ. Therefore, $\mathcal {M}, (m,h) \not \vDash A$.

The Boolean cases are then trivial.

If A = S B, then $\mathcal {M}, (m,h) \vDash A$ iff $\mathcal {M}, (m,h^{\prime }) \vDash B$ for every h ^′ such that m ∈ h ^′ iff A ∈ w by induction hypothesis (since we have proved IH for arbitrary h going through m).

If A = [c] _a B, then $\mathcal {M}, (m,h) \vDash A$ iff $\mathcal {M}, (m,h^{\prime }) \vDash B$ for every h ^′ such that m ∈ h ^′ and $h^{\prime } \in Choic{e_{a}^{m}}(h)$ iff A ∈ w by induction hypothesis (cf. the commentary on the previous case).

If A = I _a B, then A ∉ w by (F1). We also have $\mathcal {M}, (m,h) \not \vDash A$, since, given that m ∉ Ξ, all the choices at m are vacuous. □

Lemma 3 (Truth Lemma 2)

Let X ∈ Ξ and w ∈ X. Then, for any sentence A, the following holds:

$$\mathcal{M}, (X, h_{w} ) \vDash A \Leftrightarrow A \in w.$$

Proof

Again, we use induction on the construction of A. The atomic case we have by definition of V, and the Boolean cases are obvious. We consider the modal cases.

Let A = S B, and assume that S B ∈ w. Then take any $h_{w^{\prime }}$ passing through X. In the context of $\mathcal {M}$ this means that w ^′ ∈ X, which in turn means that w R w ^′. Therefore, we have B ∈ w ^′ and, by induction hypothesis, $\mathcal {M}, (X, h_{w^{\prime }}) \vDash B$. Since $h_{w^{\prime }}$ was arbitrary, this means that $\mathcal {M}, (X, h_{w} ) \vDash SB$.

On the other hand, assume that S B ∉ w. This means that the set

$$\alpha = \{ C \mid SC \in w \} \cup \{ \neg B \}$$

is consistent. Indeed, otherwise we would have

$$\{ C \mid SC \in w \} \vdash B,$$

and further, by standard S5 reasoning

$$\{ SC \mid SC \in w \} \vdash SB,$$

and so, given, maxiconsistency of w, we would have S B ∈ w, contrary to our assumption. Therefore, consider an arbitrary w ^′ ∈ W extending α. By definition, w ^′ ∈ X, therefore $h_{w^{\prime }}$ goes through X and we have, by induction hypothesis, that $\mathcal {M}, (X, h_{w^{\prime }} ) \not \vDash B$.

Let A = [c] _a B, and let [c] _a B ∈ w. Then take any $h_{w^{\prime }}$ such that $h_{w^{\prime }} \in Choic{e_{a}^{X}}(h_{w})$. In the context of $\mathcal {M}$ this means that w≃ _a w ^′. Therefore, we have B ∈ w ^′ and, by induction hypothesis, $\mathcal {M}, (X, h_{w^{\prime }}) \vDash B$. Since $h_{w^{\prime }}$ was arbitrary, this means that $\mathcal {M}, (X, h_{w} ) \vDash [c]_{a}B$.

On the other hand, assume that [c] _a B ∉ w. This means that the set

$$\beta = \{ C \mid [c]_{a}C \in w \} \cup \{ \neg B \}$$

is consistent. Indeed, otherwise we would have

$$\{ C \mid [c]_{a}C \in w \} \vdash B,$$

and further, by standard S5 reasoning

$$\{ [c]_{a}C \mid [c]_{a}C \in w \} \vdash [c]_{a}B,$$

and so, given, maxiconsistency of w, we would have [c] _a B ∈ w, contrary to our assumption. Therefore, consider an arbitrary w ^′ ∈ W extending β. By definition, w ^′≃ _a w, and also w ^′ ∈ X given that ≃ _a ⊆ R. Therefore $h_{w^{\prime }}$ goes through X and moreover $h_{w^{\prime }} \in Choic{e_{a}^{X}}(h_{w})$. By induction hypothesis, we have that $\mathcal {M}, (X, h_{w^{\prime }} ) \not \vDash B$, and so, putting all together, that $\mathcal {M}, (X, h_{w} ) \not \vDash [c]_{a}B$.

Let A = I _a B. First of all, note that by induction hypothesis and Lemma 2 we have the following identity:

$$ Ext(B) = \{ (m,h) \mid \mathcal{M}, (m,h) \vDash B \}. $$

(1)

Now, assume that I _a B ∈ w. Then, by (A5), we also have [c] _a I _a B ∈ w and ¬S I _a B ∈ w. Take any $h_{w^{\prime }}$ such that $h_{w^{\prime }} \in Choic{e_{a}^{X}}(h_{w})$. In the context of $\mathcal {M}$ this means that w≃ _a w ^′. Therefore, we have I _a B ∈ w ^′. By definition of N _a , this means that $Ext(B) \in N_{a}((X, h_{w^{\prime }}))$. On the other hand, the fact that ¬S I _a B ∈ w means that the set

$$\gamma = \{ C \mid SC \in w \} \cup \{ \neg I_{a}B \}$$

is consistent. Indeed, otherwise we would have

$$\{ C \mid SC \in w \} \vdash I_{a}B,$$

and further, by standard S5 reasoning

$$\{ SC \mid SC \in w \} \vdash SI_{a}B,$$

and so, given maxiconsistency of w, we would have S I _a B ∈ w, contrary to our assumption. Therefore, consider an arbitrary w ^″ ∈ W extending γ. By definition, w ^″ ∈ X so that $h_{w^{\prime \prime }}$ goes through X, and we have $Ext(B) \notin N_{a}((X, h_{w^{\prime \prime }}))$ by definition of N _a .

Putting all this together, we get that, by Eq. 1, $\{(m,h) \mid \mathcal {M}, (m,h) \vDash B \} \in N_{a}((X. h_{w^{\prime }}))$ for every $h_{w^{\prime }} \in Choic{e_{a}^{X}}(h_{w})$ and $\{ (m,h) \mid \mathcal {M}, (m,h) \vDash B \} \notin N_{a}((X, h_{w^{\prime \prime }}))$ for some $h_{w^{\prime }}$ going through X. That is to say, we get that $\mathcal {M}, (X, h_{w} ) \vDash I_{a}B$.

On the other hand, if I _a B ∉ w, then, of course, E x t(B) ∉ N _a (X, h _w ), and given the fact that $h_{w} \in Choic{e_{a}^{X}}(h_{w})$ and the identity (1), we get that $\mathcal {M}, (X, h_{w} ) \not \vDash I_{a}B$ immediately. □

Now we are ready for the main result of this section.

Theorem 1 (Completeness)

Let Θ be a consistent set of sentences. Then Θ has a model.

Proof

Consider the model $\mathcal {M}$ defined above. By Lemma 1 and the reasoning given immediately before it, $\mathcal {M}$ is an imagination model. Take any maxiconsistent set w extending Θ and its corresponding R-equivalence class X. Then, by Lemma 3, we have $\mathcal {M}, (X, h_{w} ) \vDash {\Theta }$. □

We also get compactness of the STIT imagination logic axiomatized by L as a standard consequence of strong completeness.

4 Tableaux

We now devise a tableau proof system to implement the systematic search for countermodels to inferences. The tableau calculus we shall present is based on the tableau calculus for dstit logic in [17] (see also [15]) and the labelled tableau calculus for E in [7].

The tableau rules are utilized to process semantic information about imagination models, and we will use (i) expressions $h_{i} {\lhd _{a}^{m}} h_{l}$ to indicate that the histories h _i and h _l are choice-equivalent for agent a at moment m, (ii) statements m _k ∈ h _k to express that moment m _k belongs to history h _k , (iii) expressions m ≺ m _k to state that moment m is earlier than moment m _k , and (iv) statements ∥A∥∈N _a ((m, h)) (∥A∥∉N _a ((m, h))) to express that the truth set of A belongs (does not belong) to N _a ((m, h)). Moreover, it must be ensured that a model induced by a complete tableau satisfies the independence of agents condition and that ${\lhd _{a}^{m}}$ indeed designates an equivalence relation. To guarantee the latter properties, the structural tableau rules of Table 1 are assumed.

Table 1 Structural tableau rules

We annotate formulas by names of moment/history-pairs. If Δ is a set of formulas, then Δ⁰ := {A,(m, h ₀)∣A∈Δ}. A tableau is a rooted tree; its nodes are sets of certain expressions. In this section we shall use ‘⊩’ not to denote L-derivability, but to form derivability statements (i.e., sequents) in the tableau calculus we are about to define. If Δ ⊩ A is a sequent, then the root of the tableau for Δ ⊩ A is Δ⁰ ∪ {m ∈ h ₀, m ≺ m ₀, m ₀ ∈ h ₀} ∪ {¬A,(m, h ₀)}. To expressions from this root, decomposition rules and structural tableau rules can be applied to complete the tableau. A tableau is said to be complete iff each of its branches is complete. A branch is complete if there is no possibility to apply one more rule to expand this branch. A tableau branch is said to be closed iff there are expressions of the form A,(m, h) and ¬A,(m, h) on the branch or expressions of the form ∥A∥∈N _a ((m, h)) and ∥A∥∉N _a ((m, h)). A closed branch is considered complete. A tableau is called closed iff all of its branches are closed, and it is called open if it is not closed.

The indices i, k, l,… used in the tableau rules are natural numbers, and a new index is the smallest natural number not already used in the tableau. In models constructed from open tableau branches, we shall interpret an agent index a by a itself. Note that it may happen that a rule is applied to an expression from a tableau node more than once if the rule requires additional input and suitable additional input is introduced at later nodes. If, for instance, the decomposition rule for formulas S A is applied to the expressions S A,(m, h _i ), m ∈ h _k , and later on the branch a new expression m ∈ h _l is introduced, then the rule has to be applied also to S A,(m, h _i ), m ∈ h _l .

The tableau calculus for STIT imagination logic consists of the tableau rules presented in the Tables 1 and 2. Syntactic consequence is then defined as follows.

Table 2 Decomposition rules for STIT imagination logic

Definition 3

Let Δ∪{A} be a set of formulas. Δ ⊩ A (‘A is derivable from Δ’) iff there exists a closed and complete tableau for Δ⁰ ∪ {m ∈ h ₀, m ≺ m ₀, m ₀ ∈ h ₀}∪{¬A,(m, h ₀)}.

If there is a complete and open branch on a tableau with root Δ⁰ ∪ {m ∈ h ₀, m ≺ m ₀, m ₀ ∈ h ₀} ∪ {¬A,(m, h ₀)}, then there exists a countermodel to the sequent Δ ⊩ A. The construction of a countermodel is guided by the open branch, but there are limits to directly reading off a countermodel. An open branch may contain an expression ∥A∥∈N _a ((m, h) and thereby provide the information that in the countermodel the truth set of A is a neighbourhood of agent a at moment/history-pair (m, h), but that does not fully specify the countermodel.

Examples of tableaux

The examples in Table 3 show open and complete tableaux from which a countermodel can be read off to some extent. Then in Table 4 we present two examples of closed tableaux. In the first example from Table 4 the branching two-premises tableau rule for the imagination operator is applied. In the second example from Table 4 we prove an instance of axiom (A5) and apply the other decomposition rules for the imagination operator.

Table 3 Examples of open tableaux

Table 4 Examples of closed tableaux

Note that the open branches in the first two examples do not provide full information concerning the construction of a countermodel. The countermodel consists of three distinct moments of time m, m ₀, and m ₁. The moments m ₀ and m ₁ are later than moment m and are assumed to be incomparable with respect to the temporal order. There are two histories; history h ₀ passes through m and m ₀, and history h ₁ passes through m and m ₁. In the first example the induced model is such that the truth set of p → p, i.e., the set of all moment/history-pairs, belongs to N _a ((m, h ₀)) but not to N _a ((m, h ₁)). The remaining features of the countermodel are left unspecified. In both examples the open tableau does not give any information concerning the evaluation of p and thus the evaluation of p is arbitrary. In the second example the induced model is such that the truth set of I _a p belongs to N _a ((m, h ₀)) but not to N _a ((m, h ₁)). ∥I _a p∥ = $\{ (m^{*}, h^{*}) \mid \forall h^{\prime } \in Choice^{m^{*}}_{a}(h^{*} ) (\Vert p \Vert \in N_{a} ((m^{*}, h^{\prime }))) \text { and } \exists h^{\prime \prime } \in H_{m^{*}} (\Vert p \Vert \not \in N_{a} ((m^{*} , h^{\prime \prime })))\}$. Since no information about ∥p∥ is provided on the open branch, we may set ∥I _a p∥ =$\varnothing$. Thus, in the induced countermodel $\varnothing \in N_{a}((m, h_{0}))$ and $\varnothing \not \in N_{a}((m, h_{1}))$.

Note that in the second example from Table 4 the final node of the leftmost branch is obtained by applying the rule for negated imagination operators to ¬I _a p,(m, h ₁) and that the final nodes of the other two branches are obtained by applying the rule for non-negated imagination operators to I _a p,(m, h ₀). Note also that the rule TRAN gives rise to infinite tableaux, cf. Example 3.4.7 in [12].

Definition 4

Let $\mathcal {M} = \langle Tree, \leq , Ag, Choice, \{ \overline N_{a}\mid a \in Ag \}, V\rangle$ be an imagination model and let b be a tableau branch. The model ${\mathcal M}$ is said to be faithful to b iff there exists a function, $f:S\rightarrow MH({\mathcal M})$, where S = { (m _k , h _i ) | m _k ∈ h _i occurs on b } ⊆ M×H with M = { m _k | m _k occurs on b }, H = { h _k | h _k occurs on b }, such that the following conditions hold:

• 1. For every expression A,(m, h) on b, it holds that ${\mathcal M}, f((m,h)) \vDash A$.

• 2. (∀h, h ^′ ∈ H) (∀m ∈ M) left(f((m, h))) = left(f((m, h ^′))) and (∀m, m ^′ ∈ M) (∀h ∈ H) right(f((m, h))) = right(f((m ^′, h))), where left and right are the left and right projection functions. Thus, it is possible to define two auxiliary functions related to f, π ₁:M → T r e e and π ₂:H → H i s t o r y by requiring that for m ∈ M, $\pi _{1}(m)=\overline m$, if $f((m,\ldots ))=(\overline m,\ldots )$, and for h ∈ H, $\pi _{2}(h)=\bar h$, if $f((\ldots ,h))=(\ldots ,\bar h)$.

• 3. If m _i ∈ h _k occurs on b, then $\pi _{2}(h_{k}) \in H_{\pi _{1}(m_{i})}$.

• 4. If $h_{i} {\lhd _{a}^{m}} h_{k}$ occurs on b, then $\pi _{2}(h_{k} )\in Choice_{a}^{\pi _{1}(m)}(\pi _{2}(h_{i}))$.

• 5. If ∥A∥∈N _a ((m, h)) occurs on b, then $\Vert A \Vert _{\mathcal M} \in \overline N_{a}({f((m,h))})$.

The function f is said to show that ${\mathcal M}$ is faithful to branch b.

Lemma 4

Let $\mathcal {M} = \langle Tree, \leq , Ag, Choice, \{ \overline N_{a}\mid a \in Ag \}, V\rangle$ be an imagination model, and let b be a tableau branch. If ${\mathcal M}$ is faithful to b and a tableau rule is applied to b, then the application produces at least one extension b ^′ of b, such that ${\mathcal M}$ is faithful to b ^′.

Proof

Assume that f is a function that shows ${\mathcal M}$ to be faithful to b. We have to consider every tableau rule. If extended branches are obtained by applying one of the rules for ¬¬A, (A∧B) or ¬(A∧B), then obviously f shows ${\mathcal M}$ to be faithful to at least one extension b ^′ of b. Suppose the rule for formulas S A is applied to S A,(m, h _i ). Then branch b ^′ extends branch b by A,(m, h _k ) for all m ∈ h _k on b. Since f is faithful to b, we have ${\mathcal M} ,f((m,h_{i})) \vDash SA$. By the definition of satisfaction, it holds that ${\mathcal M} , (\pi _{1}(m), \bar h) \vDash A$ for all $\bar h \in H_{\pi _{1}(m)}$. Since $\pi _{2}(h_{k})\in H_{\pi _{1}(m)}$, we have ${\mathcal M} , f((m,h_{k}))\vDash A$ for all h _k with m ∈ h _k on b and f shows ${\mathcal M}$ to be faithful to b ^′.

Suppose now that the rule for ¬S A is applied to ¬S A,(m, h _i ), so that b is extended by m ≺ m _k , m ∈ h _k , m _k ∈ h _k , and ¬A,(m, h _k ), for a new index k. Since f shows ${\mathcal M}$ to be faithful to b, we have ${\mathcal M} , f((m,h_{i})) \vDash \neg S A$. Thus, there is $\bar h\in H_{\pi _{1}(m)}$ with ${\mathcal M} , (\pi _{1}(m), \bar h) \vDash \neg A$. We define f ^′ to be the same function as f, except that $f^{\prime }((m,h_{k} )) = (\pi _{1}(m),\bar h)$ and $f^{\prime }((m_{k},h_{k}))=(\overline m,\bar h)$ for some $\overline m \in \bar h$ with $\pi _{1}(m)\leq \overline m$. Clearly, the function f ^′ satisfies Condition 2 of Definition 4, and the functions π ₁, π ₂ of f ^′ are appropriately expanded, i.e., $\pi _{2} (h_{k}) = \bar h$ and $\pi _{1} (m_{k}) = \overline m$. Then ${\mathcal M} , f^{\prime }((m,h_{k} ))$ $\vDash$ ¬A, $\pi _{2}(h_{k} ) \in H_{\pi _{1}(m)}$, and $\pi _{2}(h_{k} ) \in H_{\pi _{1}(m_{k})}$ . The function f ^′ shows ${\mathcal M}$ to be faithful to the extended branch b ^′.

Next, suppose the rule for [c _a ]A is applied to [c _a ]A,(m, h _i ). Then we obtain b ^′ as an extension of b by A,(m, h _k ) for all $h_{i} {\lhd _{a}^{m}} h_{k}$ on b. Since f is faithful to b, we have ${\mathcal M} ,f((m,h_{i})) \vDash [c_{a}]A$. Then, by the definition of satisfaction, it holds that ${\mathcal M} , (\pi _{1}(m), \bar h) \vDash A$ for all $\bar h \in Choice^{\pi _{1}(m)}_{a}(\pi _{2} (h_{i}))$. Since $\pi _{2}(h_{k})\in Choice^{\pi _{1}(m)}_{a}(\pi _{2} (h_{i}))$, we have ${\mathcal M} , f((m,h_{k}))\vDash A$ for all h _k with $h_{i} {\lhd _{a}^{m}} h_{k}$ on b and f shows ${\mathcal M}$ to be faithful to b ^′.

Assume that the rule for ¬[c _a ]A is applied to ¬[c _a ]A,(m, h _i ), so that b is extended by m ≺ m _k , m ∈ h _k , m _k ∈ h _k , $h_{i} {\lhd _{a}^{m}} h_{k}$, and ¬A,(m, h _k ), for a new index k. Since f shows ${\mathcal M}$ to be faithful to b, we have ${\mathcal M} , f((m,h_{i})) \vDash \neg [c_{a}] A$. Thus, there is $\bar h\in Choice^{\pi _{1}(m)}_{a}(\pi _{2} (h_{i}))$ with ${\mathcal M} , (\pi _{1}(m), \bar h) \vDash \neg A$. We define f ^′ to be the same function as f, except that f ^′((m, h _k )) =$(\pi _{1}(m),\bar h)$ and $f^{\prime }((m_{k},h_{k}))=(\overline m,\bar h)$ for some $\overline m \in \bar h$ with $\pi _{1}(m)\leq \overline m.$ The auxiliary functions π ₁, π ₂ of f ^′ are appropriately expanded. Then ${\mathcal M} , f^{\prime }((m,h_{k} )) \vDash \neg A$, $\pi _{2}(h_{k}) \in H_{\pi _{1}(m_{k})}$, and $\pi _{2}(h_{k} ) \in H_{\pi _{1}(m)}$ (since $\pi _{2}(h_{k} ) = \bar h \in Choice_{a}^{\pi _{1}(m)}(\pi _{2}(h_{i}))\subseteq H_{\pi _{1}(m)}$). The function f ^′ shows ${\mathcal M}$ to be faithful to the extended branch b ^′.

Suppose that the rule for I _a A is applied to I _a A,(m, h _i ). Then the branch b ^′ is obtained as an extension of b by ∥A∥∈N _a ((m, h _k )) for all $h_{i} {\lhd _{a}^{m}} h_{k}$ occurring on b and by m ≺ m _l , m ∈ h _l , m _l ∈ h _l , and ∥A∥∉N _a ((m, h _l )) for a new index l. Since f is faithful to b, we have ${\mathcal M}, f((m, h_{i})) \vDash I_{a} A$. This means that $\forall \bar h \in Choice_{a}^{\pi _{1} (m)}(\pi _{2}(h_{i}))$ $(\Vert A \Vert _{{\mathcal M}} \in \overline N_{a} ((\pi _{1} (m), \bar h)))$ and $\exists \bar h ' \in H_{\pi _{1} (m)}$ $(\Vert A \Vert _{{\mathcal M}} \not \in \overline N_{a} ((\pi _{1} (m), \bar h ')))$. Since $\pi _{2} (h_{k}) \in Choice_{a}^{\pi _{1} (m)}(\pi _{2} (h_{i}))$, we have $\Vert A \Vert \in \overline N_{a} ((\pi _{1}(m), \pi _{2} (h_{k}))$ for all $h_{i} {\lhd _{a}^{m}} h_{k}$ on the branch. We define f ^′ to be exactly as f, except that $f^{\prime }((m, h_{l})) = (\pi _{1} (m), \bar h^{\prime })$ and $f^{\prime }((m_{l}, h_{l})) = (\overline m, \bar h^{\prime })$ for some $\overline m \in \bar h^{\prime }$ with $\tau _{1} (m) \leq \overline m$. The auxiliary functions π ₁, π ₂ of f ^′ are appropriately expanded. Then $\pi _{2} (h_{l}) \in H_{\pi _{1} (m)}$ (since $\pi _{2} (h_{l} ) = \bar h '$ and $\bar h ' \in H_{\pi _{1} (m)}$) and $\pi _{2} (h_{l}) \in H_{\pi _{1} (m_{l})}$ (since $\pi _{1} (h_{l} ) = \overline m$ and $\overline m \in \bar h '$). The function f ^′ shows ${\mathcal M}$ to be faithful to b ^′.

Next, assume that the rule for ¬I _a A is applied to ¬I _a A,(m, h _i ). Then there are two extended branches. The branch b ^′ extends b by ∥A∥∈N _a ((m, h _l )) for every h _l with m ∈ h _l on b. The branch b ^″ extends branch b by ∥A∥∉N _a ((m, h _k )), m ∈ h _k , m _k ∈ h _k , m ≺ m _k , $h_{i} {\lhd ^{m}_{a}} h_{k}$ for some new index k. Since f is faithful to b, we have $\mathcal {M} , f((m,h_{i} )) \vDash \neg I_{a} A$. Thus either (a) $\forall \bar h \in H_{\pi _{1} (m)}$ $(\Vert A \Vert _{{\mathcal M}} \in \overline N_{a} ((\pi _{1} (m), \bar h))$, or (b) $\exists \bar h ' \in Choice_{a}^{\pi _{1} (m)}(\pi _{2} (h_{i}))$ with $\Vert A \Vert _{{\mathcal M}} \not \in \overline N_{a} ((\pi _{1} (m), \bar h '))$. The function f shows ${\mathcal M}$ to be faithful to branch b ^′. In case (b), we define f ^′ to be exactly as f, except that $f^{\prime }((m, h_{k})) = (\pi _{1} (m), \bar h)$ and $f^{\prime }((m_{k}, h_{k})) = (\overline m, \bar h)$ for some $\overline m \in \bar h$ with $\tau _{1} (m) \leq \overline m$. The auxiliary functions π ₁, π ₂ of f ^′ are appropriately expanded. Then $\pi _{2} (h_{k}) \in H_{\pi _{1} (m)}$ (since $\pi _{2} (h_{k} ) = \bar h$ and $\bar h \in H_{\pi _{1} (m)}$) and $\pi _{2} (h_{k}) \in H_{\pi _{1} (m_{k})}$ (since $\pi _{1} (h_{k} ) = \overline m$ and $\overline m \in \bar h$). The function f ^′ shows ${\mathcal M}$ to be faithful to b ^″.

Suppose that the rule for I _a A and ¬I _a B is applied to I _a A,(m, h _i ) and ¬I _a B,(m, h _i ). Again there are two extended branches. The branch b ^′ extends branch b by m ≺ m _k , m _k ∈ h _k , m ∈ h _k , A,(m _k , h _k ), ¬B,(m _k , h _k ) for a new index k. The branch b ^″ extends b by m ≺ m _l , m _l ∈ h _l , m ∈ h _l , ¬A,(m _l , h _l ), B,(m _l , h _l ) for a new index l. Since f is faithful to b, we have ${\mathcal M} , f((m,h_{i} )) \vDash I_{a} A$ and ${\mathcal M} , f((m,h_{i} )) \vDash \neg I_{a} B$. It is easily seen that therefore $\Vert A \Vert _{{\mathcal M}}$ ≠$\vert B \Vert _{{\mathcal M}}$. Hence, either (a) there is a moment/history-pair $(\overline m , \bar h )$ $\in MH({\mathcal M} )$ with ${\mathcal M} , (\overline m , \bar h ) \vDash A$ and ${\mathcal M} , (\overline m , \bar h ) \vDash \neg B$ or (b) there is a moment/history-pair $(\overline m , \bar h )$ $\in MH({\mathcal M} )$ with ${\mathcal M} , (\overline m , \bar h )\vDash \neg A$ and ${\mathcal M} , (\overline m , \bar h )\vDash B$. Case (a): We define f ^′ to be the same function as f, except that f ^′((m, h _k )) =$(\pi _{1}(m),\bar h )$ and f ^′((m _k , h _k )) =$(\overline m ,\bar h )$ for some $\overline m \in \bar h$ with $\pi _{1}(m)\leq \overline m.$ The auxiliary functions π ₁, π ₂ of f ^′ are appropriately expanded. Then ${\mathcal M} , f^{\prime }((m,h_{k} )) \vDash A$, ${\mathcal M} , f^{\prime }((m,h_{k} )) \vDash \neg B$, and $\pi _{2}(h_{k} ) \in H_{\pi _{1}(m)}$. The function f ^′ shows ${\mathcal M}$ to be faithful to the extended branch b ^′. Case (b): analogous to the previous case.

Finally, we consider the structural tableau rules. If f shows $\mathcal M$ to be faithful to b, and one of the rules REF, SYM, or TRAN is applied to obtain a branch b ^′, then f shows $\mathcal M$ to be faithful to b ^′ and Condition 4 from Definition 4 is satisfied, because for every agent a ∈ A g and every m ∈ T r e e, the relation $\{(h,h^{\prime })\mid h^{\prime } \in Choic{e_{a}^{m}}(h)\}$ is an equivalence relation.

For IND, we have $\pi _{2}(h_{n})\in Choice_{a_{1}}^{\pi _{1}(m)} (\pi _{2}(h_{l_{1}}))$, … , $\pi _{2}(h_{n})\in Choice_{a_{k}}^{\pi _{1}(m)} (\pi _{2}(h_{l_{k}}))$, because ${\mathcal M}$ satisfies the independence of agents condition. Moreover, since $\pi _{2}(h_{n})\in Choice_{a_{1}}^{\pi _{1}(m)} (\pi _{2}(h_{l_{1}}))$ ⊆$H_{\pi _{1}(m)}$, it follows that $\pi _{2}(h_{n}) \in H_{\pi _{1}(m)}$. Thus, the function f shows ${\mathcal M}$ to be faithful to a branch b, if the IND-rule is applied to b. □

Theorem 2 (Soundness)

If ${\Delta } \not \vDash A$ , then Δ⊯A.

Proof

If ${\Delta } \not \vDash A$, then there is a model ${\mathcal M}$ and a moment/history-pair (m ^′, h ^′)$\in MH({\mathcal M} )$, such that for all B∈Δ, ${\mathcal M},(m^{\prime },h^{\prime }) \vDash B$ and ${\mathcal M}, (m^{\prime },h^{\prime }) \not \vDash A$. We consider a complete tableau for Δ⁰ ∪ { ¬A,(m, h ₀)} ∪ {m ∈ h ₀, m ≺ m ₀, m ₀ ∈ h ₀}, such that every branch starts with the single-node branch b consisting of Δ⁰ ∪ { ¬A,(m, h ₀)} ∪ {m ∈ h ₀, m ≺ m ₀, m ₀ ∈ h ₀}. Let f((m, h ₀))=(m ^′, h ^′). Then f shows ${\mathcal M}$ to be faithful to b. (Without loss of generality, we may assume that in ${\mathcal M}$’s set of moments there is a moment m ^″ later than m ^′, so that we can put f(m ₀, h ₀) = (m ^″, π ₂(h ₀)). If necessary, we can add such a moment and assume that agents have vacuous choices at (m ^″, π ₂(h ₀)) and that (m ^″, π ₂(h ₀)) ∉V(p) for every atom p.) By the previous lemma, after applying a tableau rule to branch b, the model ${\mathcal M}$ is faithful to at least one branch which is an extension of b. Therefore, in the tableau there is a complete branch b ^′ to which ${\mathcal M}$ is faithful. If every branch of such a tableau is closed, then (i) there are formulas C, ¬C, and a pair (m ^″, h ^″) such that C,(m ^″, h ^″) and ¬C,(m ^″, h ^″) occur on b ^′, or (ii) there is a formula D, an agent index a, and a pair (m ^″′, h ^″′) such that ∥D∥∈N _a ((m ^″′, h ^″′)) and ∥D∥∉N _a ((m ^″′, h ^″′)) occur on b ^′. Since ${\mathcal M}$ is faithful to b ^′, there is a function f ^′ such that we have the contradiction ${\mathcal M},f^{\prime }((m^{\prime \prime },h^{\prime \prime }))\vDash C$ and ${\mathcal M},f^{\prime }((m^{\prime \prime },h^{\prime \prime }))\vDash \neg C$ or the contradiction $\Vert D\Vert _{{\mathcal M}} \in \overline N_{a}((m^{\prime \prime \prime },h^{\prime \prime \prime }))$ and $\Vert D\Vert _{{\mathcal M}} \not \in \overline N_{a}((m^{\prime \prime \prime },h^{\prime \prime \prime }))$. Hence, there is no complete closed tableau for Δ⁰ ∪ { ¬A,(m, h ₀)}∪{m ∈ h ₀, m ≺ m ₀, m ₀ ∈ h ₀} and thus Δ⊯A. □

In order to show completeness, we define for a given open branch of a complete tableau a model. Then we show that the defined model satisfies the formulas occurring on the open branch.

Definition 5

Let b be an open branch of a complete tableau. Then the model ${\mathcal M}_{b}$ =$(Tree,\leq , Ag,Choice, \{ \overline N_{a} \mid a \in Ag\}, V)$ induced by b is defined as follows:

• 1. T r e e := { m∣(m, h) occurs on b }.

• 2. ≤ := the reflexive, transitive closure of { (m _i , m _j )∣m _i ≺m _j occurs on b, m _i , m _j ∈ T r e e }.

• 3. A g := { a∣a is an agent index occurring on b }.

• 4. $Choic{e_{a}^{m}}(h)$ :=$\{\, h_{l} \mid h {\lhd ^{m}_{a}} h_{l} \text { occurs on } b\,\}$ for all a ∈ A g, m ∈ T r e e, m ∈ h occurring on b.

• 5. $\overline N_{a}((m,h))$ :=$\{\Vert A \Vert _{{\mathcal M}_{b}} \mid \Vert A \Vert \in N_{a} ((m,h)) \text { occurs on } b\}$.

• 6. V(p) := { (m, h)∣p,(m, h) occurs on b }; $V(p) = \varnothing$ for every other atomic formula p.

Since b is a complete and open branch, (m, h) ∉ V(p) if ¬p,(m, h) occurs on b. Because of the reflexive and transitive closure and since every moment m _k introduced by a tableau rule is a ≺-successor of the root moment m from the first node in a tableau, the ordered set (T r e e, ≤) is a tree and thus a branching time structure. Given this branching time structure, we have induced sets of histories and moment/history-pairs. Since b is an open branch of a complete tableau, by the structural rules REF, SYM, and TRAN, ${\lhd _{a}^{m}}$ is an equivalence relation defined on H _m . Therefore, $Choic{e_{a}^{m}}(h)$ is the corresponding equivalence class of h. By rule IND, the independence of agents condition is satisfied, cf. [17].

Note

Contrary to first appearance, the neighbourhood functions $\overline N_{a}$ are well-defined. We can define the depth of I-nesting of a formula A, d I(A). If A contains no imagination operator I _a , then d I(A) = 0. If A has the form ¬B or [c _a ]B, then d I(A) = d I(B). If A is a conjunction (B∧C), then d I(A) is m a x(d I(B),d I(C)). If A has the shape I _a B, then d I(A) = d I(B)+1. We can show that $\overline N_{a}((m,h))$ is well-defined by a double induction first on the depth of I-nesting and then on the construction of A. If d I(A) = 0, then the truth set $\Vert A \Vert _{{\mathcal M}_{b}}$ is well-defined because it is defined independently of neighbourhood functions, and thus $\overline N_{a}((m,h))$ is well-defined. Suppose that d I(A) = n+1, and $\overline N_{a}((m,h))$ is well-defined for formulas B with d I(B) ≤ n, i.e., $\Vert B \Vert _{{\mathcal M}_{b}}$ is well-defined. Then (i) A has the shape I _a B or (ii) A has the form (B∧C) with d I(B) ≤ n+1 and d I(C) ≤ n+1. In case (i), we may use the induction hypothesis to conclude that $\Vert A \Vert _{{\mathcal M}_{b}}$ is well-defined. In case (ii), we may note that $\Vert (B \wedge C) \Vert _{{\mathcal M}_{b}}$ =$\Vert B \Vert _{{\mathcal M}_{b}}$ ∩$\Vert C \Vert _{{\mathcal M}_{b}}$. By induction on the construction of A, $\Vert B \Vert _{{\mathcal M}_{b}}$ and $\Vert C \Vert _{{\mathcal M}_{b}}$ are well-defined, and thus their intersection is well-defined. But then $\overline N_{a}((m,h))$ is well-defined. Hence, $\overline N_{a}((m,h))$ is well-defined for every formula A.

Lemma 5

If b is an open branch of a complete tableau and ${\mathcal M}_{b}$ = (Tree,≤,Ag, Choice, $\{ \overline N_{a} \mid a \in Ag\}$ , V) is the model induced by b, then (if A,(m,h) occurs on b, then ${\mathcal M}_{b} , (m,h) \vDash A$ ).

Proof

The proof is by induction on the number of connectives in A. Suppose that A is atomic and hence contains no connectives and A,(m, h) occurs on b. By definition of the valuation function V, (m, h)∈V(A), so that $\mathcal {M}_{b} , (m,h) \vDash A.$

If A is a negated atom ¬p and the expression ¬p,(h, m) occurs on b, then, as noted above, $\mathcal {M}_{b} , (m,h) \not \vDash p,$ and thus $\mathcal {M}_{b} , (m,h) \vDash A$.

If A has the shape ¬¬B, B∧C, or ¬(B∧C) we may use the induction hypothesis and the fact that the tableau is complete.

Suppose that A has the form S B. If A,(m, h) occurs on b, then for every h _k with m ∈ h _k on b we have B, (m, h _k ) on b (since the tableau is complete) and, by the induction hypothesis, $\mathcal {M}_{b},(m,h_{k})\vDash B.$ By the definition of H _m , it follows that $\mathcal {M}_{b},(m,h)\vDash SB.$

Let A have the form ¬S B. If A,(m, h) occurs on b, then, by completeness of the tableau, there is a pair (m, h _k ) on b with ¬B,(m, h _k ) on b. By the induction hypothesis and definition of M _b , $\mathcal {M}_{b},(m,h_{k}) \vDash \neg B$. Therefore, $\mathcal {M}_{b},(m,h)\vDash \neg SB.$

If A has the form [c] _a B and A,(m, h) occurs on b, then B,(m, h _k ) occurs on b for every h _k with $h {\lhd _{a}^{m}} h_{k}$ on b. By the induction hypothesis and the definition of ${\mathcal M}_{b}$ it follows that ${\mathcal M}_{b} , (m, h ) \vDash [c]_{a} B$.

If A has the shape ¬[c] _a B and A,(m, h) occurs on b, then there exists an h _k with $h {\lhd _{a}^{m}} h_{k}$ and ¬B,(m, h _k ) occurring on b. By definition of ${\mathcal M}_{b}$, it follows that $h_{k}\in Choic{e_{a}^{m}}(h)$ and, by the induction hypothesis, it follows that ${\mathcal M}_{b},(m,h_{k})\vDash \neg B$. Therefore ${\mathcal M}_{b},(m,h)\vDash \neg [c]_{a} B$.

If A has the form I _a B and A,(m, h) occurs on b, then ∥B∥∈N _a ((m, h)) occurs on b for every h _k with $h {\lhd _{a}^{m}} h_{k}$ on b. Moreover, there exists an h _l with $h {\lhd _{a}^{m}} h_{l}$ and ∥B∥∉N _a ((m, h _l )) occurring on b. By definition of ${\mathcal M}_{b}$, $\Vert B \Vert _{{\mathcal M}_{b}}\in \overline N_{a}((m,h))$ for every h _k with $h_{k} \in Choic{e_{a}^{m}}(h)$ and $\Vert B \Vert _{{\mathcal M}_{b}}\not \in \overline N_{a}((m,h_{l}))$ with $h_{l} \in Choic{e_{a}^{m}}(h)$. Hence ${\mathcal M}_{b},(m,h)\vDash I_{a} B$.

Suppose that A has the form ¬I _a B and that A,(m, h) occurs on b. Then there are two cases, according to the branching of the decomposition rule for negated imagination ascriptions. In the first case ∥B∥∈N _a ((m, h _l )) occurs on b for every h _l with m ∈ h _l on b. By definition of ${\mathcal M}_{b}$, $\Vert B \Vert _{{\mathcal M}_{b}}\in \overline N_{a}((m,h_{l}))$ for every h _l ∈H _m . But then ${\mathcal M}_{b},(m,h) \not \vDash I_{a} B$, i.e., ${\mathcal M}_{b},(m,h) \vDash A$. In the second case there exists an h _k with $h {\lhd _{a}^{m}} h_{k}$ and ∥B∥∉N _a ((m, h _k )) occurring on b. By the definition of ${\mathcal M}_{b}$, $h_{k} \in Choic{e_{a}^{m}}(h)$. Since b is open, $\Vert B \Vert _{{\mathcal M}_{b}}\not \in \overline N_{a}((m,h_{k}))$. But then ${\mathcal M}_{b},(m,h) \not \vDash I_{a} B$, i.e., ${\mathcal M}_{b},(m,h) \vDash A$. □

Theorem 3 (Completeness)

If Δ⊯A, then ${\Delta } \not \vDash A.$

Proof

Suppose that Δ⊯A. Then there is no complete and closed tableau for Δ⁰ ∪ {¬A,(m, h ₀)} ∪ {m ∈ h ₀, m ≺ m ₀, m ₀ ∈ h ₀}. Let b be an open branch of a complete tableau for this set and let $\mathcal {M}_{b}$ be the model induced by b. By the previous lemma, it follows that $\mathcal {M}_{b} , (m, h_{0}) \vDash A$ for every formula A∈Δ and ${\mathcal M}_{b} , (m, h_{0}) \vDash \neg A$, thus ${\mathcal M}_{b} , (m, h_{0}) \not \vDash A$. Therefore, ${\Delta } \not \vDash A$. □

As a corollary to tableau soundness and completeness we may note that if one complete tableau for Δ⁰ ∪ {¬A,(m, h ₀)}∪{m ∈ h ₀, m ≺ m ₀, m ₀ ∈ h ₀} corresponding to the sequent Δ ⊩ A is open, then every complete tableau is open, and if one complete tableau for Δ⁰ ∪ {¬A,(m, h ₀)} ∪ {m ∈ h ₀, m ≺ m ₀, m ₀ ∈ h ₀} is closed, then so is every tableau corresponding to Δ ⊩ A.

5 Conclusion

The present paper addresses and solves one of the open problems listed in [18], namely to give proof-theoretic characterizations of the semantically presented STIT imagination logic. The other items are still on the agenda: addressing the programme of reducing non-propositional imagination ascriptions to propositional ones as suggested by Niiniluoto [10], the development of a first-order extension of STIT imagination logic with identity, the addition of conception operators as in [8], and the development of the idea of “strategic imagination”. In [5] is has been shown that dstit-logic for groups of agents is undecidable. We conjecture that single-agent STIT imagination logic is decidable.