As a simple exercise in modal logic, I'd like to show that $\not\vdash\Diamond(p\lor\neg p)$. However, when using the tableaux method, I can't get very far. After replacing $\neg\Diamond$ with $\Box\neg$, there are no previously introduced worlds in which to apply $\Box$. If I try to introduce "all" possible worlds, it seems like the branch is closed (so probably this is illicit?).

$$\neg\Diamond(p\lor\neg p),0\\ \Box\neg(p\lor\neg p),0\\ p,1\\ \neg p,1\\p,2\\ \neg p,2\\p,3\\ \neg p,3\\ \vdots\\ \times$$

I need to show that this tree has (at least) one open branch in order to prove $\not\vdash \Diamond(p\lor\neg p)$.

  • $\begingroup$ What is your axiom system? Plenty of modal logics do have $\vdash p\vee\neg p$ (e.g. $p\vee\neg p$ is valid in all Kripke frames). $\endgroup$ Aug 20, 2019 at 14:56
  • $\begingroup$ What exactly are you trying to do here? You say that you want to show $\not \vdash p \lor \neg p$ -- but then where do your $\neg \Diamond (p \lor \neg p)$ and $\Box \neg(p \lor \neg p)$ come from? Are you trying to model derivability ($\vdash$) via modal operators ($\Box, \Diamond$)? These are not the same thing! While it is possible to use the language of modal logic to formalize arguments about derivability in logic -- if that's what you were having in mind -- you can not simply identify $\vdash \phi$ with $\vdash \Box \phi$ or $\vdash \Diamond \psi$! $\endgroup$ Aug 20, 2019 at 15:33
  • $\begingroup$ Also, to show that a derivation with all branches closed does not exist, it does not suffice to present just one tableau with an open branch -- you have to argue that any attempt at completing the tableau will have open branches, that is, you have to provide an explanation along with your tableau showing why no other rule applications will lead to success. $\endgroup$ Aug 20, 2019 at 15:33
  • $\begingroup$ Also, as pointed out in the other comment, whether we have $\vdash p \lor \neg p$ or $\not \vdash p \lor \neg p$ will depend on which rule system you are talking about. Since your formula doesn't have any modal operators in it, we don't need the clutter of modal logic with its different systems, as its (non-)derivability will coincide with that in non-modal standard logic. If you're talking about modal classical logic, then we have $\vdash p \lor \neg p$. If you are talking about e.g. (modal) intuitionistic logic, where we indeed have $\not\vdash p \lor \neg p$, you need to make this explicit. $\endgroup$ Aug 20, 2019 at 15:42
  • 1
    $\begingroup$ @Doubt I updated my answer with a simple countermodel we can construct from the open branch. $\endgroup$ Aug 21, 2019 at 15:04

1 Answer 1


As you correctly say, you start your tableau with

$\neg \Diamond(p \lor \neg p), 0\\ \Box \neg (p \lor \neg p), 0$

And that's where it already ends: In order to continue by disassembling $\Box$, you'd need to have a $0$-accessible world $1$ in your branch, $0r1$. This is what the rule in Priest's book states:

$\Box A, i\\ irj\\ \downarrow\\ A, j$

Here, $A$ is the formula $\neg(p \lor \neg q)$, $i$ is $0$, and $j$ is $1$.

But we do not have such a statement $0r1$: The world $1$ has nowhere been introduced. You can't just make the label $1$ up, it must have been introduced into the branch beforehand as $0r1$ by an application of the $\Diamond$ rule -- but you don't have a formula starting with $\Diamond$ in your branch, and hence no world $1$ to continue with.

The semantic motivation for this restriction is the following:
If we have a formula of the form $\Diamond A, i$, then we know by the semantics of $\Diamond$ that there exists a possible world $j$ accessible from $i$ such that $A$ holds at $j$, so the rule for $\Diamond$ requires us to introduce this world into the branch by writing $irj$ (where $r$ stands for "reaches" or "accessibility relation").
However, if by $\Box$ we make a claim about all the possible worlds $j$ that are accessible from $i$, then we need to make sure that these worlds $j$ actually exist: $\Box A, i$ states that "For all worlds $j$, if $j$ is accessible from $i$, then $A$ holds at $j$". This statement tells us nothing about the existence of $i$-accessible worlds: The formula $\Box A, i$ can become vacuously true if there are no $i$-accessible worlds at all; and even if there are worlds that $i$ can access, then according to the "if"-clause we need to restrict ourselves to those worlds of which we know that $i$ can access them, and are not allowed to just make up claims about new worlds that we have never seen on the branch before. So we need to make use of those worlds that we know exist and are accessible from $i$, namely those that have already been introduced in the branch as $irj$.
Hence, according to the definition of the $\Box$ rule, in order to go from $\Box \neg(p \lor \neg q), 0$ to a world $1$, we need to have $0r1$ already present in the branch.

But this is not the case here. Also, since the only thing we did so far is the conversion from $\neg \Diamond$ to $\Box \neg$ (which was the only option available at that time), it is obvious that at no point we could have chosen a different rule application that would enable us to continue the tableau. (This part is important: In order to show $\not \vdash$, i.e. to prove that no syntactic derivation (e.g. no tableau) exists, it does not suffice to present just one unsuccessful (in the case of tableaus: open) derivation -- instead, we need to argue why any attempt of setting up a proof will eventually fail.) Since there is no other way to construct the tableau such that will eventually be closed, we proved that there is no tableau refutation for the formula $\Diamond(p \lor \neg p)$: We successfully proved $\not\vdash \Diamond(p \lor \neg p)$.

From this open branch it is straightforward to construct a countermodel that refutes the validity ($\not \vDash$) of the formula. Since our problem was that we know of no $0$-accessible world that could serve to refute $\neg(p \lor \neg p)$, setting up our countermodel is very simple: We just create a structure with only one world, which can reach nothing and in which nothing holds:

enter image description here

Let $\mathfrak{A} = \langle W, R, v \rangle$ with
$W = \{w_0\}$,
$R = \emptyset$,
$v: \langle P,w \rangle \mapsto 0$ for any propositional letter $P$ and world $w \in W$

Since $w_0$ can't reach any worlds at all, trivially there is no reachable world in which $p \lor \neg p$ holds,

  • hence $w_0 \not \vDash \Diamond(p \lor \neg p)$
    ($\Diamond(p \lor \neg p)$ is not true in the world $w_0$, since $p \lor \neg p$ is not true in any $w_0$-accessible world),
  • hence $\mathfrak{A} \not \vDash \Diamond(p \lor \neg p)$
    ($\Diamond(p \lor \neg p)$ is not true in the structure $\mathfrak{A}$, since it is not true in all $w \in W$),
  • hence $\not \vDash \Diamond(p \lor \neg p)$
    ($\Diamond(p \lor \neg p)$ is not valid, since it is not true in all structures).

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .