I have this definition:
Let $\nu$ be any propositional interpretation. Let $b$ be any branch of a tableau. Say that $\nu$ is faithful to b if and only if for every formula, $A$, on the branch, $\nu(A)=1$
For this definition I have the following assignment:
Let $\tau$ and $\rho$ be tableaus such that $\tau \leadsto \rho$. Prove that $\tau$ is satisfiable/valid if and only if $\rho$ is satisfiable/valid.
So I suppose that $\neg(\phi \vee \psi)$ is on a branch $B$. The definition says that $\nu$ makes every formula on $B$ true. So I have:
$$\nu(\neg(\phi \vee \psi))=1$$
This means that $\tau$ is satisfied.
If we apply a rule then only one branch will occur by adding $\neg \phi$ and $\neg \psi$ to $B$. Then we see that $\nu(\neg(\phi \vee \psi))=1$ if:
$$\nu(\neg \phi)=1, \nu(\neg \psi)=1$$
And this means that $\rho$ is satisfied. Finally we can conclude that $\tau$ is satisfiable iff $\rho$ is satisfiable.
Am I correct?
This proof is contained in many standard textbooks (essentially, any formal treatment of tableau).
The general idea is that if a branch $b$ of a tableau $\tau$ is satisfied by a model $M$, and any tableau rule is applied to that branch $b$ to make a new tableau $\tau'$, then there will be some branch $b'$ of $\tau'$, extending $b$, that is also satisfied by $M$.
Thus, by induction, if $\tau$ is satisfiable and $\rho$ is obtained by applying some finite sequence of rules to $\tau$, then $\rho$ is also satisfiable.