Fundamental Results in Propositional Logic

It should be intuitively obvious that any formula provable by the tableau method must really be a tautology, or, equivalently, the fact that a tableau closes must mean that the origin is not satisfiable (not true under any interpretation). This intuition can be justified by the following argument. If a tableau T is satisfiable, then any immediate extension T1 of T is satisfiable, hence any immediate extension T2 of the extension T1 is satisfiable, and so forth. Thus every extension of T is satisfiable, and hence no extension of T can close. If all finite subsets of a denumerable set S are satisfiable, then S is satisfiable. This is known as the Compactness Theorem for Propositional Logic. For a denumerable set S of formulas, if all finite subsets of S are satisfiable, then no tableau for S can close.