The basic idea behind tableau systems

Here is the basic idea behind tableau systems. Imagine that your goal is to show that certain formulas of the language $\mathcal{L}_0$ are tautologies, or that in every structure $\mathbf{S}$, they are true. Now clearly, given a formula $X$, you cannot just consider every structure $\mathbf{S}$ individually to see whether that particular structure models $X$ or not. That would take an infinite amount of time. What you can do is employ some of the proofs we have given above to show that, e.g., $X \vee \neg X$ is a tautology. The problem with this is that as the formulas get more complex, the proofs get longer and longer, to the point where it is just not feasible to carry them out in natural language. Moreover, these solutions are not very systematic as they stand. If you are ingenious, you may be able to do them (up to a point), but we don’t want to rely on ingenuity to solve these problems. We need a method.

In the tableau method, the whole approach is based on the following facts, discussed above:

1. if $X$ is a tautology, $\neg X$ is a contradiction;

2. if something is a contradiction, then it hides an explicit contradictory claim of form $Y \wedge \neg Y$ (and indeed, for some atomic formula $P$, $P \wedge \neg P$).

If we put together these two facts, we get a strategy. We take the candidate tautology $X$. If it really is a tautology, then its negation $\neg X$ is a contradiction. If it is a contradiction, then with the help of some appropriate rules, we can hopefully show in what way it is a contradictory statement. In other words, we show which is the formula $Y$ it claims is both true and false.

On the other hand, if $X$ is not a tautology, then it is either a contradiction or contingent, so its negation $\neg X$ will either be a tautology or contingent (as described above). In such cases, we will find no contradiction.

To continue our example, take $X \vee \neg X$ again. We already know this is a tautology, but what if we want to show in our tableau system that it is? Well, since we want to show $X \vee \neg X$, what we put at the beginning of our proof is its negation $\neg (X \vee \neg X)$. Then come the rules, which will tease out where exactly is the contradictory statement hidden in the formula.