The law of the excluded-middle in modal logic 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)$.
 A: 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:  

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

