Tableaux for Basic Modal Logic

Shahid Rahman

► To cite this version:

Shahid Rahman. Tableaux for Basic Modal Logic. Licence. France. 2015. cel-01228873

HAL Id: cel-01228873

https://shs.hal.science/cel-01228873

Submitted on 17 Nov 2015

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Tableaux for Basic Modal Logic

Shahid Rahman

shahid.rahman@univ-lille3.fr

Univ. Lille; Philosophie, UMR 8163: STL

## DEFINITION

* A *label* is finite sequence of positive integers. A *labelled formula* is an expression of the form $i\phi$, where *i* is the label of the formula $\phi$.

* If the label *i* is a sequence of length >1 the positive integers of the sequence will be separated by periods. Thus, if *i* is a label and an *n* is positive integer, then *i.n* is a new label, called an *extension of i*. The label *i* is then an *initial segment of i.n*.

<table><thead><tr><th>Restricted Labelling</th><th>Unrestricted Labelling</th></tr></thead><tbody><tr><td>(V)□Ai<br>--------------------</td><td>(F)□Ai<br>--------------------</td></tr><tr><td>(V)Aj<br>--------------------</td><td>(F)Aj<br>--------------------</td></tr><tr><td>(F)◇Ai<br>--------------------</td><td>(T)◇Ai<br>--------------------</td></tr><tr><td>(F)Aj<br>--------------------</td><td>(T)Aj<br>--------------------</td></tr><tr><td>K: j must occur already in the branch<br><br>Reflexivity: j=i<br><br>Seriality: j can be new<br><br>Symmetry: Assume that i = k.n, then j= k (k.n. is an immediate extension of k, and k occurs already in the branch).<br><br>Transitivity: i is an initial segment of j (such as j = i.m or j = i.m.n...).<br><br>Euclideanity: If in the branch occur, i, i.n and it is the case that (V)□Ai.m(or (F) ◇Ai.m), then j = i.n:<br><br>[i]<br>[i.n]<br>(F) ◇Ai.m<br>--------------------<br>(F)Ai.n<br><br>[i]<br>[i.n]<br>(V)□Ai.m</td><td>j: is new</td></tr></tbody></table>
(V)Ai.n

Tableaux and as generated by winning strategies

* If $\Sigma$ is a set of dialogically signed formulae and $X$ is a single dialogically signed formula, we will write $\Sigma, X$ for $\Sigma 4 \{X\}$.

* Observe that the formulae below the line always represent pairs of attack and defence moves. In other words, they represent rounds.

* The vertical bar ‘|’ indicates alternative choices for **O**, **P**'s strategy must have a defence for both possibilities (dialogical games defining two possible plays).

* The rules containing yielding two lines indicate that it is **P** who has the choice – an he thus might need only one of both possible choices.

* Note that the expressions between the symbols "<" and ">", such as `<(P)?` or `<(O)?` are moves – more precisely they are attacks – but not formulae (assertions) which could be attacked. These expressions are not actually part or the tableau. They are formulae which are included in the set of formulae. **These expressions are rather part of the algorithmic device to reconstruct the correspondent dialogues.**

Intuitionistic Tableaux

<table><thead><tr><th>(O)-Cases</th><th>(P)-Cases</th></tr></thead><tbody><tr><td>Σ, (O)A ∨ B<br>------------------<br>Σ, &lt;(P)?- ∨ &gt;(O)A | Σ, &lt;(P)?-<br> ∨ &gt;(O)B</td><td>Σ, (P)A ∨ B<br>------------------<br>Σ[O], &lt;(O)?- ∨ &gt;(P)A<br>Σ[O], &lt;(O)?- ∨ &gt;(P)B</td></tr><tr><td>Σ, (O)A ∩ B<br>------------------<br>Σ, &lt;(P)?-L &gt;(O)A<br>Σ, &lt;(P)?-R &gt;(O)B</td><td>Σ, (P)A ∩ B<br>------------------<br>Σ[O], &lt;(O)?-L &gt;(P)A | Σ[O], &lt;(O)?-<br>R &gt;(P)B</td></tr><tr><td>Σ, (O)A → B<br>------------------<br>Σ[O], (P)A ... | &lt;(P)A &gt;(O)B</td><td>Σ, (P)A → B<br>------------------<br>Σ[O], (O)A; (P)B</td></tr><tr><td>Σ, (O)¬A<br>------------------<br>Σ[O], (P)A; —</td><td>Σ, (P)¬A<br>------------------<br>Σ[O], (O)A; —</td></tr><tr><td>Σ, (O)∀xA<br>------------------<br>Σ, &lt;(P)?- ∀ x/k<sub>i</sub> &gt;(O)A<sub>[x/ki]</sub></td><td>Σ, (P)∀xA<br>------------------<br>Σ[O], &lt;(O)?- ∀ x/k<sub>i</sub> &gt;(P)A<sub>[x/ki]</sub></td></tr></tbody></table>
$$ \begin{array}{c} \Sigma, (\mathbf{O})\exists x A \\ \multicolumn{2}{c}{\text{------------------}} \\ \Sigma, \langle(\mathbf{P})?-\exists>(\mathbf{O})A\text{[x/ki]} \\ \qquad k_i \text{ is new} \end{array} $$

$k_i$ is new

$$ \begin{array}{c} \Sigma, (\mathbf{P})\exists x A \\ \multicolumn{2}{c}{\text{------------------}} \\ \Sigma_{[O]}, \langle(\mathbf{O})?-\exists>(\mathbf{P})A\text{[x/ki]} \end{array} $$

Intuitionistic tableaux are generated with the addition of the set $\Sigma_{[O]}$, which only contains O-signed formulae): the totality of the previous P-formulæ on the same branch of the tree are eliminated.

## DEFINITION

Let us look at two examples, namely one for classical logic and one for intuitionistic logic. We use the tree shape of the tableau made popular by Smullyan ([18]):

If $\Theta$ is a given set of (P-, or O-) signed formulae, we say one of the rules R of above rules of the tableaux-system *applies* to $\Theta$ if by appropriate choice of $\Theta$, the collection of signed formulae above the line in rule R becomes $\Theta$.

By an *application of R to the set Θ*, we mean the replacement of $\Theta$ by $\Theta_1$ (or by $\Theta_1$ and $\Theta_2$, if R is $(\mathbf{P})\wedge, (\mathbf{O})\vee$, or $(\mathbf{O})\rightarrow$) where $\Theta$ is the set of formulae above the line in rule R (after suitable substitution for $\Sigma$, and for the formulae A (and B)) and $\Theta_1$ (or $\Theta_1$ and $\Theta_2$) is the set of formulae below. This assumes R to apply to $\Theta$. Otherwise the result is again $\Theta$. For example, by applying rule $(\mathbf{P})\rightarrow$ to the set $\Theta$: $\{(\mathbf{O})A, (\mathbf{P})B, (\mathbf{P})(\mathbf{C}\rightarrow\mathbf{D})\}$ we may get $\Sigma_{[O]}4\Theta_1$: $\{(\mathbf{O})A, (\mathbf{O})C, (\mathbf{P})D\}$ – notice that $(\mathbf{P})B$ disappeared because we have $\Sigma_{[O]}$ and not $\Sigma$.

By *configuration* we mean a finite collection $\{\Sigma_1, \Sigma_2, ..., \Sigma_n\}$ of sets of signed formulae, where $\Sigma$ might stand for $\Sigma$ and/or $\Sigma_{[O]}$.

By an *application of R to the configuration* $\{\Sigma_1, \Sigma_2, ..., \Sigma_n\}$ we mean the replacement of this configuration with a new one which is like the first except for containing instead of some $\Sigma_i$ the result (or results) of applying rule R to $\Sigma_i$.

By a tableau we mean a finite sequence of configurations $C_1, C_2, ..., C_n$ in which each configuration except the first is the result of applying one of the above rules to the preceding configuration.
A set of signed formulae is closed if it contains both (O)a and (P)a (for a atomic). A configuration {$Σ_1, (Σ_2, ..., Σ_n}$} is closed if each $Σ_i$ is closed. A tableau $C_1, C_2, ..., C_n$ is closed if some $C_i$ is closed.

By a tableau for a set $Σ$ of signed formulae we mean a tableau $C_1, C_2, ..., C_n$ in which $C_1$ is {$Σ$}.

Modal Logic

<table><thead><tr><th>Restricted Labelling</th><th>Unrestricted Labelling</th></tr></thead><tbody><tr><td>(O)□Ai<br>----------------------------------<br>&lt;(P) ?j&gt; (O)Aj</td><td>(P)□Ai<br>----------------------------------<br>&lt;(O) ?j&gt; (P)Aj</td></tr><tr><td>(P)◇Ai<br>----------------------------------<br>&lt;(O) ?◇&gt; (P)Aj</td><td>(O)◇Ai<br>----------------------------------<br>&lt;(P) ?◇&gt; (O)Aj</td></tr><tr><td><b>K:</b> j must occur already in the branch<br><b>Reflexivity:</b> j=i<br><b>Seriality:</b> j can be new<br><b>Symmetry:</b> Assume that i = k.n, then j= k (k.n. is an immediate extension of k, and k occurs already in the branch).<br><b>Transitivity:</b> i is an initial segment of j (such as j = i.m or j = i.m.n...).<br><b>Euclideanity:</b> If in the branch occur, i, i.n and it is the case that (O)□Ai.m(or (P) ◇Ai.m), then j = i.n:<br><br>[i]<br>[i.n]<br>(P)◇Ai.m<br>----------------------------------<br>(P)Ai.n<br><br>[i]<br>[i.n]<br>(O)□Ai.m<br>----------------------------------<br>(O)Ai.n</td><td>j: is new</td></tr></tbody></table>