Actuality, Tableaux, and Two-Dimensional Modal Logics

Abstract

In this paper we present tableau methods for two-dimensional modal logics. Although models for such logics are well known, proof systems remain rather unexplored as most of their developments have been purely axiomatic. The logics herein considered contain first-order quantifiers with identity, and all the formulas in the language are doubly-indexed in the proof systems, with the upper indices intuitively representing the actual or reference worlds, and the lower indices representing worlds of evaluation—first and second dimensions, respectively. The tableaux modulate over different notions of validity such as local, general, and diagonal, besides being general enough for several two-dimensional logics proposed in the literature. We also motivate the introduction of a new operator into two-dimensional languages and explore some of the philosophical questions raised by it concerning the relations there are between actuality, necessity, and the a priori, that seem to undermine traditional intuitive interpretations of two-dimensional operators.

Appendices

Appendix 1 Soundness and Completeness for S5$_{2D}$

The soundness theorem for $\mathbf S5 _{2D}$ is an extension of corresponding proofs for modal logic presented, for instance, in Fitting and Mendelsohn (1998) and Priest (2008).

Definition 8.1

(Satisfiability) Let S be a set of doubly-indexed formulas. We say S is satisfiable in ${\mathcal {M}}=\langle W ,\langle w*,w*\rangle ,{\mathcal {R}}_{\Box },{\mathcal {R}}_{\mathcal {F}},\mathscr {D},V\rangle$ just in case there is a function, f, assigning to each (single) index n occurring in S a possible world $f(n)\in Z$, where $f(0)=w*$, $W= Z\times Z$, such that,

• If $[\varphi ]^i_n\in S$, then $\varphi$ is true at f(n) relative to f(i), i.e. ${\mathcal {M}}^{f(i)}_{f(n)}\vDash \varphi$.

• If the pairs of indices $\langle i,n\rangle$ and $\langle i,m\rangle$ are in S, then $\langle f(i),f(n)\rangle {\mathcal {R}}_{\Box }\langle f(i),f(m)\rangle$.

• If the pairs of indices $\langle i,n\rangle$ and $\langle j,n\rangle$ are in S, then $\langle f(i),f(n)\rangle {\mathcal {R}}_{\mathcal {F}}\langle f(j),f(n)\rangle$.

Definition 8.2

A tableau branch $\mathfrak {b}$ is satisfiable just in case the set of doubly-indexed formulas on it is satisfiable in some model, and a tableau is satisfiable just in case some branch of it is satisfiable.

Lemma 8.1

A closed tableau is not satisfiable.

Proof

Suppose that $\mathcal {T}$ is a closed tableau that is also satisfiable. By Definition 8.2, some branch $\mathfrak {b}$ of $\mathcal {T}$ is satisfiable, whence there is a model, ${\mathcal {M}}=\langle W ,\langle w*,w*\rangle ,{\mathcal {R}}_{\Box },{\mathcal {R}}_{\mathcal {F}},\mathscr {D},V\rangle$, satisfying the set S of doubly-indexed formulas on $\mathfrak {b}$ by way of the function f, by Definition 8.1. But since, by assumption, $\mathcal {T}$ is also closed, for some formula $\varphi$ and pair of indices $\langle i,n\rangle$, $[\varphi ]^i_n\in S$ and $[\lnot \varphi ]^i_n\in S$. Hence, by Definition 8.1, ${\mathcal {M}}^{f(i)}_{f(n)}\vDash \varphi$ and ${\mathcal {M}}^{f(i)}_{f(n)}\nvDash \varphi$, which is impossible. $\square$

Lemma 8.2

If one of the rules in $\mathbf S5 _{2D}$ is applied to a satisfiable 2D-tableau, it results in another satisfiable 2D-tableau.

Proof

Suppose $\mathfrak {b}$ is a branch of a satisfiable 2D-tableau $\mathcal {T}$ and that we apply one of the rules in $\mathbf S5 _{2D}$ to a doubly-indexed formula occurring on $\mathfrak {b}$. It is easily seen that the result is another satisfiable tableau. Since, by assumption, $\mathcal {T}$ is satisfiable, by Definition 8.2 at least one of its branches, say, $\mathfrak {b}*$, is satisfiable. Now, if $\mathfrak {b}*\ne \mathfrak {b}$, then $\mathfrak {b}*$ remains satisfiable after we apply a rule on $\mathfrak {b}$, whence we have a satisfiable 2D-tableau by Definition 8.2. On the other hand, if $\mathfrak {b}*=\mathfrak {b}$, we need to consider several cases. We omit the arguments for the Booleans, modal operators, quantifiers, and identity, since these are routine.⁵⁴ In order to carry on such arguments in the 2D framework one just needs to add a pair of indices where the first coordinate does not do any work.

Suppose $[\mathcal {A}\varphi ]^i_n$ occurs on $\mathfrak {b}$, and we apply the rule for $\mathcal {A}$. Since $\mathfrak {b}$ is satisfiable, ${\mathcal {M}}^{f(i)}_{f(n)}\vDash \mathcal {A}\varphi$, by Definition 8.1. Thus, ${\mathcal {M}}^{f(i)}_{f(i)}\vDash \varphi$, by the truth clause for $\mathcal {A}$. Therefore, applying the rules for $\mathcal {A}$ to a satisfiable 2D-tableau results in another satisfiable 2D-tableau. The argument for $\lnot \mathcal {A}$ is analogous.

Suppose $[\odot \varphi ]^i_n$ occurs on $\mathfrak {b}$, and we apply the rule for $\odot$. Since $\mathfrak {b}$ is satisfiable, ${\mathcal {M}}^{f(i)}_{f(n)}\vDash \odot \varphi$, by Definition 8.1. Thus, ${\mathcal {M}}^{w*}_{f(n)}\vDash \varphi$, by the truth clause for $\odot$, in which case ${\mathcal {M}}^{f(0)}_{f(n)}\vDash \varphi$, since ‘0’ is fixed to $w*$. Therefore, applying the rules for $\odot$ to a satisfiable 2D-tableau results in another satisfiable 2D-tableau. The argument for $\lnot \odot$ is analogous.

Suppose $[\otimes \varphi ]^i_n$ occurs on $\mathfrak {b}$, and we apply the rule for $\otimes$. Since $\mathfrak {b}$ is satisfiable, ${\mathcal {M}}^{f(i)}_{f(n)}\vDash \otimes \varphi$, by Definition 8.1. Thus, ${\mathcal {M}}^{f(n)}_{f(n)}\vDash \varphi$, by the truth clause for $\otimes$. Therefore, applying the rules for $\otimes$ to a satisfiable 2D-tableau results in another satisfiable 2D-tableau. The argument for $\lnot \otimes$ is analogous.

Suppose [$\mathcal {F}\varphi$]$^i_n$ occurs on $\mathfrak {b}$, and we apply the rule for $\mathcal {F}$. Since $\mathfrak {b}$ is satisfiable, ${\mathcal {M}}^{f(i)}_{f(n)}\vDash \mathcal {F}\varphi$, by Definition 8.1. Also, for every pair of indices $\langle i,n\rangle$ and $\langle j,n\rangle$ occurring on $\mathfrak {b}$, $\langle f(i),f(n)\rangle {\mathcal {R}}_{\mathcal {F}}\langle f(j),f(n)\rangle$. Thus, ${\mathcal {M}}^{f(j)}_{f(n)}\vDash \varphi$, by the truth clause for $\mathcal {F}$. On the other hand, suppose [$\lnot \mathcal {S}\varphi$]$^i_n$ occurs on $\mathfrak {b}$. Since $\mathfrak {b}$ is satisfiable, ${\mathcal {M}}^{f(i)}_{f(n)}\vDash \lnot \mathcal {S}\varphi$, by Definition 8.1, and so ${\mathcal {M}}^{f(i)}_{f(n)}\nvDash \mathcal {S}\varphi$. Hence, for every $\langle f(i),f(n)\rangle {\mathcal {R}}_{\mathcal {F}}\langle f(j),f(n)\rangle$, ${\mathcal {M}}^{f(j)}_{f(n)}\nvDash \varphi$, by the truth clause for $\mathcal {S}$, and so ${\mathcal {M}}^{f(j)}_{f(n)}\vDash \lnot \varphi$. Therefore, applying the rules for $\mathcal {F}$ to a satisfiable 2D-tableau results in another satisfiable 2D-tableau.

Suppose [$\mathcal {S}\varphi$]$^i_n$ occurs on $\mathfrak {b}$, and we apply the rule for $\mathcal {S}$. Since $\mathfrak {b}$ is satisfiable, ${\mathcal {M}}^{f(i)}_{f(n)}\vDash \mathcal {S}\varphi$, by Definition 8.1. Thus, for some $z\in Z$, $\langle f(i),f(n)\rangle {\mathcal {R}}_{\mathcal {F}}\langle z,f(n)\rangle$ and ${\mathcal {M}}^{z}_{f(n)}\vDash \varphi$, by the truth clause for $\mathcal {S}$. Let g be like f except that $g(j)=z$, where j is a new index occurring on $\mathfrak {b}$. Since g and f agree except for j, the tableau extended by g is satisfiable. Moreover, by definition of g, $\langle g(i),g(n)\rangle {\mathcal {R}}_{\mathcal {F}}\langle g(j),g(n)\rangle$ and ${\mathcal {M}}^{g(j)}_{g(n)}\vDash \varphi$. By choice of g, it follows that ${\mathcal {M}}^{f(j)}_{f(n)}\vDash \varphi$. The argument for $\lnot \mathcal {F}$ is analogous. Therefore, applying the rules for $\mathcal {S}$ to a satisfiable 2D-tableau results in another satisfiable 2D-tableau.

Finally, let $\varphi$ be a basic formula and suppose [$\varphi$]$^i_n$ occurs on $\mathfrak {b}$, and that we apply the upper exchange rule. Since $\mathfrak {b}$ is satisfiable, ${\mathcal {M}}^{f(i)}_{f(n)}\vDash \varphi$, by Definition 8.1. Moreover, since $\varphi$ is a basic formula, ${\mathcal {M}}^{f(j)}_{f(n)}\vDash \varphi$, for any first coordinate f(j) of any pair of worlds, given that the models are constrained by (Neutrality). Therefore, applying the upper exchange rule to a satisfiable 2D-tableau results in another satisfiable 2D-tableau. $\square$

Theorem 8.1

(Soundness) If $\varphi$ has a 2D-tableau proof, then $\varphi$ is valid.

Proof

Suppose $\varphi$ has a 2D-tableau proof, in which case there is a closed 2D-tableau, $\mathcal {T}$, beginning with $[\lnot \varphi ]^0_0$. For a contradiction, assume that $\varphi$ is not valid. Thus, there is a 2D-centered model, ${\mathcal {M}}=\langle W ,\langle w*,w*\rangle ,{\mathcal {R}}_{\Box },{\mathcal {R}}_{\mathcal {F}},\mathscr {D},V\rangle$, such that ${\mathcal {M}}^{w*}_{w*}\nvDash \varphi$. Let f be a function such that $f(0)=w*$. By Definition 8.1, $\{[\lnot \varphi ]^0_0\}$ is satisfiable. Moreover, since its only branch is satisfiable, $\mathcal {T}$ is also satisfiable, and so is any 2D-tableau extending it by way of the rules in $\mathbf S5 _{2D}$, by Lemma 8.2. Therefore, $\mathcal {T}$ is both closed and satisfiable, contradicting Lemma 8.1, whence ${\mathcal {M}}^{w*}_{w*}\vDash \varphi$. $\square$

Infinite Tableaux and Systematic Procedure. Some 2D-tableaux may run infinitely, and by König’s Lemma these will have at least one infinite branch. In what follows we give an example of a failed proof attempt in $\mathbf S5 _{2D}$ generating an infinite 2D-tableau:

A 2D-matrix for the above looks like this:

$$\begin{aligned} \begin{pmatrix} &{}\quad 0 &{}\quad 1 &{}\quad 2 &{}\quad 3 &{}\quad \dots \\ 0 &{}\quad p &{}\quad \lnot p &{}\quad \times &{}\quad \times &{}\quad \\ 1 &{}\quad p &{}\quad \times &{}\quad \lnot p &{}\quad \times &{}\quad \\ 2 &{}\quad p &{}\quad \times &{}\quad \times &{}\quad \lnot p &{}\quad \\ \vdots &{}\quad \vdots &{}\quad &{}\quad &{}\quad &{}\quad \ddots \\ \end{pmatrix} \end{aligned}$$

Using the same procedure as before to devise a countermodel we have the following:

• Since ${\mathcal {M}}^0_0\vDash p$ and ${\mathcal {M}}^0_1\nvDash p$, it follows that ${\mathcal {M}}^0_0\nvDash \Box p$. Hence, .

• Since and ${\mathcal {M}}^1_2\nvDash p$, it follows that ${\mathcal {M}}^1_1\nvDash \Box p$. Hence, .

• Since ${\mathcal {M}}^2_0\vDash p$ and ${\mathcal {M}}^2_3\nvDash p$, it follows that ${\mathcal {M}}^2_2\nvDash \Box p$. Hence, ${\mathcal {M}}^2_0\nvDash p\supset \Box p$.

• $\dots$ Hence, ${\mathcal {M}}^0_0\nvDash \mathcal {S}(p\supset \Box p$).

Even though a finite countermodel can be easily constructed to invalidate $\mathcal {S}(p\supset \Box p$),⁵⁵ we need a systematic procedure for constructing 2D-tableaux in order to prove that any tableau so constructed is such that, if it has an open branch, finite or not, there is a countermodel for it.

Now, several systematic procedures of this kind can be found in the literature, even for the modal cases. In particular, we direct the reader again to Fitting and Mendelsohn (1998, pp. 126–127,)⁵⁶ since our strategy will be based on it. Thus, let [$\varphi ]^i_n$ be any doubly-indexed formula of which we want to know whether or not it is satisfiable. For stage $n=1$, introduce [$\lnot \varphi$]$^i_n$ to the 2D-tableau as line 1. Next, suppose n stages have been completed. If the 2D-tableau is already closed, then we have produced a proof of [$\varphi$]$^i_n$. On the other hand, if the 2D-tableau remains open, then we proceed to stage $n+1$ in which we take an open branch $\mathfrak {b}$ of the 2D-tableau such that $\mathfrak {b}$ is the leftmost highest point on it, and for each doubly-indexed formula $[\psi ]^j_m$ ⁵⁷ such that it occurs on $\mathfrak {b}$ we extend the 2D-tableau as follows:

• I If $[\psi ]^j_m$ is a basic formula, say, $[\chi ]^k_p$, add $[\chi ]^l_p$ to the end of $\mathfrak {b}$, where l is an upper index added by either $\mathcal {S}$ or $\mathcal {F}$ (if it does not already contain it).

• II If a constant, say, c, is on $\mathfrak {b}$, add $[(c=c)]^k_p$ to the end of $\mathfrak {b}$ for all pairs of indices $\langle k,p\rangle$ occurring on $\mathfrak {b}$.

• III If the pair of indices $\langle k,p\rangle$ is on $\mathfrak {b}$, add $[(c= c)]^k_p$ to the end of $\mathfrak {b}$ for all constants c on $\mathfrak {b}$.

• IV If $[\psi ]^j_m$ is $[(c= d)]^k_q$, for any constants c and d, and $[\varphi (c)]^k_p$ occurs on $\mathfrak {b}$, add $[\varphi (d)]^k_p$ to the end of $\mathfrak {b}$ (if it does not already contain it).

• V If $[\psi ]^j_m$ is $[\lnot \lnot \chi ]^k_p$, add $[\chi ]^k_p$ to the end of $\mathfrak {b}$ (if it does not already contain it).

• VI If $[\psi ]^j_m$ is $[(\zeta \wedge \chi )]^k_p$, add both $[\zeta ]^k_p$ and $[\chi ]^k_p$ to the end of $\mathfrak {b}$ (if it does not already contain them—analogously for the other conjunctive cases).

• VII If $[\psi ]^j_m$ is $[(\zeta \vee \chi )]^k_p$, split the end of $\mathfrak {b}$ into $\mathfrak {b}_1$ and $\mathfrak {b}_2$, adding [$\zeta$]$^k_p$ and $[\chi ]^k_p$ to the end of $\mathfrak {b}_1$ and $\mathfrak {b}_2$, respectively (if it does not already contain them—analogously for the other disjunctive cases).

• VIII If $[\psi ]^j_m$ is $[\Diamond \chi ]^k_p$, take the first lower numeric index, q, which is new to $\mathfrak {b}$, and add $[\chi ]^k_q$ to the end of $\mathfrak {b}$ (if it does not already contain it—analogously for $\lnot \Box$).

• IX If $[\psi ]^j_m$ is $[\Box \chi ]^k_p$, add every doubly-indexed formula $[\chi ]^k_q$ to the end of $\mathfrak {b}$ for every index q occurring on the branch (if it does not already contain it—analogously for $\lnot \Diamond$).

• X If $[\psi ]^j_m$ is $[\odot \chi ]^k_p$, add $[\chi ]^0_p$ to the end of $\mathfrak {b}$ (if it does not already contain it—analogously for $\lnot \odot$).

• XI If $[\psi ]^j_m$ is $[\otimes \chi ]^k_p$, add $[\chi ]^p_p$ to the end of $\mathfrak {b}$ (if it does not already contain it—analogously for $\lnot \otimes$).

• XII If $[\psi ]^j_m$ is $[\mathcal {A} \chi ]^k_p$, add $[\chi ]^k_k$ to the end of $\mathfrak {b}$ (if it does not already contain it—analogously for $\lnot \mathcal {A}$).

• XIII If $[\psi ]^j_m$ is $[\mathcal {S} \chi ]^k_p$, take the first upper numeral index, l, which is new to $\mathfrak {b}$, and add $[\chi ]^l_p$ to the end of $\mathfrak {b}$ (if it does not already contain it—analogously for $\lnot \mathcal {F}$).

• XIV If $[\psi ]^j_m$ is $[\mathcal {F} \chi ]^k_p$, add every doubly-indexed formula $[\chi ]^l_p$ to the end of $\mathfrak {b}$ for every index l occurring on the branch (if it does not already contain it—analogously for $\lnot \mathcal {S}$).

• XV If $[\psi ]^j_m$ is $[(\exists x)\chi ]^k_p$, take the first constant, c, not appearing on $\mathfrak {b}$, and add $[\chi [c/x]]^k_p$ to the end of $\mathfrak {b}$ (if it does not already contain it—analogously for $(\lnot \forall x)$).

• XVI If $[\psi ]^j_m$ is $[(\forall x)\chi ]^k_p$, add every doubly-indexed formula $[\chi [c/x]]^k_p$ to the end of $\mathfrak {b}$ such that c is among the first countably many individual constants available (if it does not already contain it—analogously for $(\lnot \exists x)$).

Once this procedure is completed for the leftmost highest point on the 2D-tableau, repeat it for the next highest point closest from it until the rightmost highest point. This is where stage $n+1$ is concluded. Now there are three possible cases to consider. Either the systematic procedure resulted in a closed 2D-tableau, thereby producing a proof of [$\varphi$]$^i_n$; the procedure terminated, producing an open branch; the procedure does not terminate, producing a possibly infinite open branch.

Completeness for $\mathbf S5 _{2D}$. We show how to construct a countermodel such that, if $\mathfrak {b}$ is any complete open branch of a 2D-tableau, finite or not, then $\mathfrak {b}$ is satisfiable, where $\mathfrak {b}$ is a complete open branch of a 2D-tableau $\mathcal {T}$ just in case every rule that can possibly be applied to it has been applied. In order to construct a countermodel we use the same procedure as in the counterexamples above.

Definition 8.3

(Equivalence class) Let $\approx$ be an equivalence relation over the set of constants in $\mathcal {L}_2{}_D$ such that $c_0\approx c_1$ iff ‘[$c_0= c_1$]$^i_n$’ occurs on $\mathfrak {b}$ for any pair of indices $\langle i,n\rangle$. Moreover, for any c, let [c] denote the equivalence class of c relative to $\approx$.

Definition 8.4

(Model) For the countermodel, if k is any single index occurring on $\mathfrak {b}$, let $Z=\{k\mid k\in \mathfrak {b}\}$, and $W=Z\times Z$. Let $\langle 0,0\rangle$ be a distinguished element of W. For every $\langle i,n\rangle ,\langle i,m\rangle \in W$, set $\langle i,n\rangle {\mathcal {R}}_{\Box }\langle i,m\rangle$, and for every $\langle i,n\rangle ,\langle j,n\rangle \in W$, set $\langle i,n\rangle {\mathcal {R}}_{\mathcal {F}}\langle j,n\rangle$. Next we define C as the set of all constants occurring on $\mathfrak {b}$, and $\mathscr {D}=\{[c]\mid c\in C\}$. Furthermore, set $V(c,\langle i,n\rangle )=[c]$ to each $c\in C$, and to each n-place predicate symbol, R, on $\mathfrak {b}$, let $V(R,\langle i,n\rangle )=\{\langle [c_0],\ldots ,[c_n]\rangle :R(c_0,\ldots ,c_n)^i_n$ occurs on $\mathfrak {b}$}. Given both rigidity conditions, for every constant symbol c and $\langle i,n\rangle ,\langle j,m\rangle \in W$ we have $V(c,\langle i,n\rangle )=V(c,\langle j,m\rangle )$. In case $\varphi$ is atomic, if [$\varphi$]$^i_n$ occurs on $\mathfrak {b}$ then ${\mathcal {M}}^i_n\vDash \varphi$, otherwise set ${\mathcal {M}}^i_n\nvDash \varphi$.⁵⁸ This is enough to define a constant domain 2D-centered model ${\mathcal {M}}=\langle W ,\langle 0,0\rangle ,{\mathcal {R}}_{\Box },{\mathcal {R}}_{\mathcal {F}},\mathscr {D},V\rangle$.

Lemma 8.3

(Truth lemma) Let $\mathfrak {b}$ be a complete open branch of a 2D-tableau, and ${\mathcal {M}}$ be a constant domain 2D-centered model, ${\mathcal {M}}=\langle W ,\langle 0,0\rangle ,{\mathcal {R}}_{\Box },{\mathcal {R}}_{\mathcal {F}},\mathscr {D},V\rangle$. For every doubly-indexed formula, [$\varphi$]$^i_n$,

$$\begin{aligned}{}[\varphi ]^i_n\text { occurs on }\mathfrak {b}\Leftrightarrow {\mathcal {M}}^i_n\vDash \varphi \end{aligned}$$

Proof

By induction on $\varphi$. We only consider the relevant two-dimensional operators.

Let $\varphi$ be $\mathcal {A}\psi$. If [$\mathcal {A}\psi$]$^i_n$ occurs on $\mathfrak {b}$, then $[\psi ]^i_i$ is also on $\mathfrak {b}$. By I.H., ${\mathcal {M}}^i_i\vDash \psi$, whence ${\mathcal {M}}^i_n\vDash \mathcal {A}\psi$, by the truth clause for $\mathcal {A}$ (the argument for $\lnot \mathcal {A}\psi$ is analogous).

Let $\varphi$ be $\odot \psi$. If [$\odot \psi$]$^i_n$ occurs on $\mathfrak {b}$, then $[\psi ]^0_n$ is also on $\mathfrak {b}$. By I.H., ${\mathcal {M}}^0_n\vDash \psi$, whence ${\mathcal {M}}^i_n\vDash \odot \psi$, by the truth clause for $\odot$ (analogously for $\lnot \odot \psi$).

Let $\varphi$ be $\otimes \psi$. If [$\otimes \psi$]$^i_n$ occurs on $\mathfrak {b}$, then $[\psi ]^n_n$ is also on $\mathfrak {b}$. By I.H., ${\mathcal {M}}^n_n\vDash \psi$, whence ${\mathcal {M}}^i_n\vDash \otimes \psi$, by the truth clause for $\otimes$ (analogously for $\lnot \otimes \psi$).

Let $\varphi$ be $\mathcal {F}\psi$. If [$\mathcal {F}\psi$]$^i_n$ occurs on $\mathfrak {b}$, then for every j on $\mathfrak {b}$, $[\psi ]^j_n$ is also on $\mathfrak {b}$. By I.H. and construction, ${\mathcal {M}}^j_n\vDash \psi$ for every $\langle i,n\rangle {\mathcal {R}}_{\mathcal {F}}\langle j,n\rangle$, whence ${\mathcal {M}}^i_n\vDash \mathcal {F}\psi$, by the truth clause for $\mathcal {F}$. On the other hand, let $\varphi$ be $\lnot \mathcal {S}\psi$. If [$\lnot \mathcal {S}\psi$]$^i_n$ occurs on $\mathfrak {b}$, then for every j on $\mathfrak {b}$, [$\lnot \psi$]$^j_n$ also occurs on $\mathfrak {b}$. By I.H. and construction, ${\mathcal {M}}^j_n\nvDash \psi$ for every $\langle i,n\rangle {\mathcal {R}}_{\mathcal {F}}\langle j,n\rangle$, whence ${\mathcal {M}}^i_n\nvDash \mathcal {S}\psi$, by the truth clause for $\mathcal {S}$.

Let $\varphi$ be $\mathcal {S}\psi$. If [$\mathcal {S}\psi$]$^i_n$ occurs on $\mathfrak {b}$, then for some j on $\mathfrak {b}$, $[\psi ]^j_n$ is also on $\mathfrak {b}$. By I.H. and construction, ${\mathcal {M}}^j_n\vDash \psi$ for some $\langle i,n\rangle {\mathcal {R}}_{\mathcal {F}}\langle j,n\rangle$, whence ${\mathcal {M}}^i_n\vDash \mathcal {S}\psi$, by the truth clause for $\mathcal {S}$. On the other hand, let $\varphi$ be $\lnot \mathcal {F}\psi$. If [$\lnot \mathcal {F}\psi$]$^i_n$ occurs on $\mathfrak {b}$, then for some j on $\mathfrak {b}$, [$\lnot \psi$]$^j_n$ is also on $\mathfrak {b}$. By I.H., ${\mathcal {M}}^j_n\nvDash \psi$ for some $\langle i,n\rangle {\mathcal {R}}_{\mathcal {F}}\langle j,n\rangle$, whence ${\mathcal {M}}^i_n\nvDash \mathcal {F}\psi$, by the truth clause for $\mathcal {F}$. $\square$

Theorem 8.2

(Completeness) If $\varphi$ is valid, then $\varphi$ has a 2D-tableau proof.

Proof

We prove the contrapositive. Suppose $\varphi$ does not have a 2D-tableau proof, in which case any 2D-tableau $\mathcal {T}$ beginning with $[\lnot \varphi ]^0_0$ remains open. Let $\mathfrak {b}$ be a complete open branch of $\mathcal {T}$ such that $[\lnot \varphi ]^0_0$ occurs on $\mathfrak {b}$. By Lemma 8.3, there is a constant domain 2D-centered model, ${\mathcal {M}}=\langle W ,\langle 0,0\rangle ,{\mathcal {R}}_{\Box },{\mathcal {R}}_{\mathcal {F}},\mathscr {D},V\rangle$, such that ${\mathcal {M}}^0_0\nvDash \varphi$. Consequently, $\varphi$ is not valid. $\square$

Appendix 2: Soundness and Completeness Theorems for General and Diagonal Tableaux

It might be useful to indicate how the soundness and completeness theorems for local 2D-tableaux can be modified for general and diagonal 2D-tableaux. The only differences concern the main theorems for soundness and completeness, namely, Theorems 8.1 and 8.2. In what follows we show how they are adjusted for general 2D-tableaux.

Theorem 9.1

(Soundness for general 2D-tableaux) If $\varphi$ has a general 2D-tableau proof, then $\varphi$ is valid.

Proof

Suppose $\varphi$ has a general 2D-tableau proof, in which case there is a closed general 2D-tableau, $\mathcal {T}$, which begins with $[\lnot \varphi ]^n_m$, where $n\ne m$, and both n and m are different from ‘0’. For a contradiction, assume that $\varphi$ is not generally valid. Thus, there is a 2D-centered model, ${\mathcal {M}}=\langle W ,\langle w*,w*\rangle ,{\mathcal {R}}_{\Box },{\mathcal {R}}_{\mathcal {F}},\mathscr {D},V\rangle$, and a pair $\langle v,w\rangle \in W$, such that ${\mathcal {M}}^{v}_{w}\nvDash \varphi$. Let f be a function such that $f(n)=v$ and $f(m)=w$, in which case ${\mathcal {M}}^{f(n)}_{f(m)}\nvDash \varphi$. By Definition 8.1, $\{[\lnot \varphi ]^n_m\}$ is satisfiable. Moreover, since its only branch is satisfiable, $\mathcal {T}$ is also satisfiable, and so is any general 2D-tableau extending it by way of the $\mathbf S5 _{2D}$ rules, by Lemma 8.2. Therefore, $\mathcal {T}$ is both closed and satisfiable, contradicting Lemma 8.1, whence ${\mathcal {M}}^{v}_{w}\vDash \varphi$. $\square$

Theorem 9.2

(Completeness for general 2D-tableaux) If $\varphi$ is valid, then $\varphi$ has a general 2D-tableau proof.

Proof

We prove the contrapositive. Suppose $\varphi$ does not have a general 2D-tableau proof, in which case any general 2D-tableau $\mathcal {T}$ beginning with $[\lnot \varphi ]^n_m$, where $n\ne m$, both n and m are different from ‘0’, and that remains open. Let $\mathfrak {b}$ be a complete open branch of $\mathcal {T}$ such that $[\lnot \varphi ]^n_m$ occurs on $\mathfrak {b}$. By Lemma 8.3, there is a constant domain 2D-centered model, ${\mathcal {M}}=\langle W ,\langle 0,0\rangle ,{\mathcal {R}}_{\Box },{\mathcal {R}}_{\mathcal {F}},\mathscr {D},V\rangle$, such that ${\mathcal {M}}^n_m\nvDash \varphi$. Consequently, $\varphi$ is not generally valid. $\square$

The arguments for diagonal 2D-tableaux are very similar, we just have to consider a sentence, $\varphi$, indexed by any pair, $\langle n,n\rangle$, where $n\ne 0$. Besides this, the arguments are essentially the same.

Appendix 3: Different Systems

We show that sound and complete general 2D-tableau can be obtained for different systems extended by $\mathbf S5 _{2D}$.

1.1 S5 $\mathcal {A}$

Crossley and Humberstone offer the following axioms for S5 $\mathcal {A}$ with general validity, besides the usual S5 axioms:⁵⁹

• (A1) $\mathcal {A}(\varphi \supset \psi )\supset (\mathcal {A}\varphi \supset \mathcal {A}\psi )$

• (A2) $\mathcal {A}\equiv \lnot \mathcal {A}\lnot \varphi$

• (A3) $\Box \varphi \supset \mathcal {A}\varphi$

• (A4) $\mathcal {A}\varphi \supset \Box \mathcal {A}\varphi$.

Lemma 10.1

$\mathbf S5 _{2D}$ with general validity extends S5 $\mathcal {A}$ with general validity.

Proof

General 2D-tableau proof schemata can be given to prove axioms (A1)-(A4). We show (A3) and (A4), and leave (A1) and (A2) for the reader. $\square$

Corollary 10.1

Soundness and Completeness for S5 $\mathcal {A}$ with general validity.

Proof

By Lemma 10.1 and soundness and completeness for $\mathbf S5 _{2D}$ general 2D-tableaux.$\square$

Moreover, it can be shown that $\mathbf S5 _{2D}$ extends S5 $\mathcal {A}$ with local validity as well by proving the axiom schema $\mathcal {A}\varphi \supset \varphi$, which is straightforwardly done by local 2D-tableaux.

1.2 S5 $\mathcal {AF}$

In what follows we exhibit Davies and Humberstone’s axiomatization of S5 $\mathcal {AF}$. Besides the basis provided by S5 $\mathcal {A}$, we have:

($\mathcal {F}$1):

$\mathcal {F}(\varphi \supset \psi )\supset (\mathcal {F}\varphi \supset \mathcal {F}\psi )$

($\mathcal {F}$2):

$\mathcal {F}\varphi \supset \varphi$

($\mathcal {F}$3):

$\mathcal {F}\varphi \supset \mathcal {FF}\varphi$

($\mathcal {F}$4):

$\varphi \supset \mathcal {F}\lnot \mathcal {F}\lnot \varphi$

($\mathcal {F}$5):

$\varphi \supset \mathcal {F}\varphi$, for any $\mathcal {A}$-free formula $\varphi$.

($\mathcal {F}$6):

$\mathcal {FA}\varphi \equiv \Box \varphi$, for any $\mathcal {A}$-free formula $\varphi$.

Lemma 10.2

$\mathbf S5 _{2D}$ with general validity extends S5 $\mathcal {AF}$ with general validity.

Proof

Again, general 2D-tableau proof schemata can be given for axioms ($\mathcal {F}$1)-($\mathcal {F}$6).

$\square$

Corollary 10.2

Soundness and Completeness for S5 $\mathcal {AF}$ with general validity.

Proof

By Lemma 10.2 and soundness and completeness for $\mathbf S5 _{2D}$ general 2D-tableaux. $\square$

Theorem 10.1

Soundness for $\mathbf{S5E }_{2D}$.

Proof

The arguments are very similar to the corresponding proofs for $\mathbf S5 _{2D}$. We only need the following adjustments. The definition of satisfiability needs to be modified by taking into account ${\mathcal {R}}_{\mathcal {D}}$ rather than ${\mathcal {R}}_{\mathcal {F}}$, in which case for a constant domain 2D-centered model, ${\mathcal {M}}=\langle W ,\langle w*,w*\rangle ,{\mathcal {R}}_{\Box },{\mathcal {R}}_{\mathcal {D}},\mathscr {D},V\rangle$, a set S of doubly-indexed formulas, and a function f from each individual index n in S to a possible world in Z, if the pairs of indices $\langle i,n\rangle$ and $\langle z,z\rangle$ are in S, then $\langle f(i),f(n)\rangle {\mathcal {R}}_{\mathcal {D}}\langle f(z),f(z)\rangle$. The rest of the definition remains the same. The soundness lemma corresponding to Lemma 8.2 varies with respect to the latter in minor details: it does not need arguments for $\otimes$ and $\odot$, it contains clauses for $\mathcal {D}$ and $\mathcal {C}$ rather than $\mathcal {F}$ and $\mathcal {S}$, which will be very similar, besides not containing arguments for upper exchange. We leave the details for the reader. $\square$

Theorem 10.2

Completeness for $\mathbf{S5E }_{2D}$.

Proof

The arguments are, again, very similar to the ones for $\mathbf S5 _{2D}$. However, for the countermodel corresponding to Definition 8.4, since we are not assuming rigidity with respect to the upper index, there needs to be some adjustments in our definitions. First, we need to modify Definition 8.3 of equivalent classes. Let $\approx _{i,n}$ be an equivalence relation over the set of constants in $\mathcal {L}_{E2D}$ such that $c_0\approx _{i,n} c_1$ iff ‘$[c_0= c_1]^i_n$’ occurs on $\mathfrak {b}$ for any constants $c_0$, $c_1$, and pair of indices $\langle i,n\rangle$. Moreover, for any c, let [c]$_{i,n}$ denote the equivalence class of c relative to $\approx _{i,n}$. Now, if k is any index occurring on $\mathfrak {b}$, let $Z=\{k\mid k\in \mathfrak {b}\}$, and $W=Z\times Z$. Let $\langle 0,0\rangle$ be a distinguished element of W. For every $\langle i,n\rangle ,\langle i,m\rangle \in W$, set $\langle i,n\rangle {\mathcal {R}}_{\Box }\langle i,m\rangle$, and for every $\langle i,n\rangle ,\langle z,z\rangle \in W$, set $\langle i,n\rangle {\mathcal {R}}_{\mathcal {D}}\langle z,z\rangle$. Let $\mathscr {D}=\{[c]_{i,n}\mid c,\langle i, n \rangle \text { on } \mathfrak {b}\}$. Concerning rigidity, this time we only assume that for any constant symbol c and $\langle i,n\rangle ,\langle i,m\rangle \in W$, $V(c,\langle i,n\rangle )=V(c,\langle i,m\rangle )$, where $V(c,\langle i,n\rangle )=[c]_{i,n}$ and to each n-place predicate symbol, R, on $\mathfrak {b}$, let $V(R,\langle i,n\rangle )=\{\langle [c_0]_{i,n},\ldots ,[c_n]_{i,n}\rangle :R(c_0,\ldots ,c_n)^i_n$ occurs on $\mathfrak {b}$}. We do not assume (Neutrality) anymore. The rest of the definition remains the same as in Definition 8.4. Furthermore, the truth lemma is basically the same except for, again, having clauses for $\mathcal {D}$ and $\mathcal {C}$ rather than $\mathcal {F}$ and $\mathcal {S}$, which are straightforward. $\square$