Some facts about the tableau system

On soundness and completeness

A fundamental goal for every logical system is to show that the semantics and the syntactic system agree on every formula. That is, if $X$ is a tautology according to the semantics, it can be proved in the system that $X$ is a theorem, and if $X$ is a theorem in the system, it really is a tautology in the semantics. This can be represented as follows: $$\models X \textit{ iff } \vdash X$$

Or again, $X$ is a theorem iff it is a tautology. I have been using these two terms somewhat interchangeably above, since as it stands, in the system I just introduced, they really do come down to the same thing. Usually, this is characterized two ways:

1. if whenever $\mathbf{S} \vdash X$, then $\mathbf{S} \models X$, the system relative to the semantics is sound;

2. if whenever $\mathbf{S} \models X$, then $\mathbf{S} \vdash X$, the system relative to the semantics is complete.

Of course, if you put together these two conditionals, you get the biconditional above. In general, it is important to keep in mind that our semantics and our deductive system are two distinct things, and that they coincide on their judgments using two distinct methods is not a trivial feat (in fact, large classes of logics cannot have a non-trivial sound and complete deductive system). On the other hand, proving soundness and completeness is rather involved and takes more machinery than we currently possess (or will possess by the end of this book). Thus, for now, you will have to trust the process.

The process, our tableau method, is in many ways better than other approaches you may have seen before, like natural deduction. The reason is because the tableau method does not require you to be creative in your proofs at all. In fact, it is provable that given a formula $X$, if $X$ is a tautology, then applying the relevant rule as many times as possible to $\neg X$ and each resulting formula completely mindlessly will result in a tree all of whose branches will close, and if $X$ is not a tautology, there will be at least one open branch left in the end. So in general, all you have to do is recognize for each formula which rules can be applied, and apply them. Of course, if you are an expert in using the system, you will be able to do shorter proofs by using your brain (e.g., by using non-branching rules only once, deriving the relevant side only).

Open tableaus and their uses

In fact, here is another way in which tableaus are better than natural deduction. Consider again the above crucial fact about our syntax and deductive system:

$$\models X \textit{ iff } \vdash X$$

Now using the usual technique on the biconditional, negate both sides. Thus:

$$\not\models X \textit{ iff } \nvdash X$$

Now we can think about what this means. First, $\not\models X$ means that $X$ is not a tautology. Second, $\nvdash X$ means that $X$ is not a theorem of the system. The latter in turn just means that $\neg X$ (!) does not (cannot) have a closed tableau. So it can only have open tableaus. So $X$ is not a tautology provided $\neg X$ only has open tableaus. So far so good. Let’s continue.

What does it mean for $X$ to not be a tautology? Well, by definition, it means that $X$ is either a contradiction or contingent. And in turn, if $X$ is either a contradiction or contingent, then $\neg X$ is either a tautology or contingent. So injecting this back to our previous line of reasoning, we get:

We can chase these facts a bit further. In particular, if $\neg X$ is either a tautology or contingent, that means that in either case, there is at least one structure $\mathbf{S}$ such that $\mathbf{S} \models \neg X$. In other words, if $\neg X$ does not have a closed tableau, we can immediately answer that it has a model! (And of course, the same goes for $X$.)