i tried to construct a proof for the following theorem about the tableau calculus in propositional logic:
If {$\Sigma,H,\lnot G$} and {$\Sigma, \lnot H, \lnot G$} have a closed tableau, then {$\Sigma, \lnot G$} has a closed tableau as well.
However, I'm not sure if my proof is correct (I could for example have missed a case or have chosen the wrong proof-method from the start) or - if the proof is correct - whether there are more elegant solutions. Perhaps my formulation of the proof could also be formulated more clearly at some points. I would really appreciate your comments!
Proof
Let {$\Sigma,H,\lnot G$} and {$\Sigma, \lnot H, \lnot G$} have a closed tableau. Then one of the following cases holds:
a) $\Sigma$ or $\lnot G$ has a closed tableau. Then obviously {$\Sigma, \lnot G$} has a closed tableau as well.
b) $H$ has a closed tableau. Then $\lnot H$ cannot have a closed tableau. But by assumption {$\Sigma, \lnot H, \lnot G$} has a closed tableau, so {$\Sigma, \lnot G$} has one as well. The same reasoning holds for the assumption that $\lnot H$ has a closed tableau.
c) $G \in \Sigma$. Then obviously {$\Sigma, \lnot G$} has a closed tableau as well.
d) $H \in \Sigma$. By assumption, {$\Sigma, H, \lnot G$} has a closed tableau, so {$\Sigma, \lnot G$} as well. The same reasoning holds for $\lnot H \in \Sigma$.
e) The application of the rules on the nodes {$\Sigma,H,\lnot G$} and {$\Sigma, \lnot H, \lnot G$} yield two closed tableaux $T_1$ and $T_2$ with two expressions $D$ and $\lnot D$ both being part of both $T_1$ and $T_2$. Then the manipulation of $\Sigma$ yields $D$ (or $\lnot D$) and the manipulation of $\lnot G$ yields $\lnot D$ (or $D$). In this case {$\Sigma, \lnot G$} has a closed tableau as well.
The remaining two cases f-g are identical to case a).
f) The manipulation of $\Sigma$ yields $D$ (or $\lnot D$) and the manipulation of $H$ yields $\lnot D$ (or $D$). But because {$\Sigma,\lnot H,\lnot G$} has a closed tree, the manipulation of $\lnot H$ has to yield $\lnot D$ (or $D$) as well. In this case, both $\vdash H \rightarrow \lnot D$ and $\vdash \lnot H \rightarrow \lnot D$ hold, out of which follows that $\vdash \lnot D$. In this case, $\lnot \lnot D$ is a contradiction which is entailed by $\Sigma$. But this can only be the case if $\Sigma$ is a contradiction as well. This, however, amounts to saying that $\Sigma$ has a closed tableau, which is equivalent to case a).
g) The manipulation of $\lnot G$ yields $D$ (or $\lnot D$) and the manipulation of $H$ yields $\lnot D$ (or $D$). Similar reasoning as in f) leads to the conclusion that $\lnot G$ needs to have a closed tableau for the case to hold.
So, if {$\Sigma,H,\lnot G$} and {$\Sigma, \lnot H, \lnot G$} have a closed tableau, then {$\Sigma, \lnot G$} has a closed tableau as well.