There is something fundamental that stops me from understanding the proofs for the propositional tableau.
- (1) soundness proves that all theorems that can be proved are valid
- (2) completeness proves that all the valid statements are theorems.
When proving soundness and completeness of the tableau:
- (3) For soundness: given a fully expanded open branch with root $A$, then there is a $v \vDash A$ [i.e.$A$ is satisfiable -- MA].
- (4) For completeness: given a tableau with a [should be every -- PS] branch closed, then $A$ is unsatisfiable.
Now, I understand soundness and completeness on their own, and the practical proofs that we do for (3) and (4). But I can’t understand why we prove exactly those statements and I can’t draw the relation between (1) to (3) and (2) to (4). Why would those make it sound and complete?
Instead of (4) I was expecting the inverse of (3) like: given a $v \vDash A$, then the tree has an open branch.
Can someone clarify on how we can prove it sound and complete and why this would do it?
It is the other way about: you use (4) to prove (1), and (3) to prove (2)! For remember, a wff $\varphi$ is declared proved by a tableau if the tree stating with the negation of $\varphi$ closes.
Thus, for soundness (1): We want to show that if a tableau starting with $\neg\varphi$ closes, so the tableau declares $\varphi$ to be proved, then $\varphi$ really is valid.
By the corrected version of (4), if a tree starting $\neg\varphi$ closes, then $\neg\varphi$ is unsatisfiable, so $\varphi$ is always true, i.e. is valid. QED.
For completeness (2): We want to show that if $\varphi$ is valid, a tableau starting $\neg\varphi$ closes. That is to say, contraposing, if some tableau starting $\neg\varphi$ stays open, then $\varphi$ is not valid.
But by (3) if some tableau starting $\neg\varphi$ stays open, i.e. has an open branch, there is a valuation which makes $\neg\varphi$ true, so $\varphi$ is not valid. QED.