Let $\tau$ be a closed tableau. Prove that $\tau$ is not satisfiable.
So let's say the statement can be expressed by $P \rightarrow Q$. To prove that this statement is true, we look at the assumption that $\neg (P \rightarrow Q)$. We know that $P \rightarrow Q$ being false means that $P$ is true and $Q$ is false.
So I have to prove $C \wedge \neg C$
Then I know that:
A tableau is complete iff every rule that can be applied has been appled.
A branch is closed iff there are formulas of the form $A$ and $\neg A$ on two of its nodes.
A branch is open iff it is not closed.
A tableau is closed iff every branch is closed, otherwise it is open.
So the statement, $\tau$ is a closed tableau then $\tau$ is not satisfiable, is true.
Am I correct?