The rules of the system

Each rule in our tableau system codifies some simple facts about our semantics. This is a general feature of deductive systems in logic. What is less so is the fact that tableau systems are not linear, but take a tree form. In fact, our tableau deductions will look something like the syntax trees we covered before. However, despite the similarities, do not confuse the two. They are entirely different systems with a different purpose. Tableau tree deductions are used to show whether $X$ is a tautologous formula, syntax tree derivations are used to show whether $X$ is a formula at all.

Just as syntax trees, tableau trees are also binary. This means that at any one point, the tree may branch to at most two separate points. But sometimes, there is no branching, and only one additional point is connected. Because of this, we may classify our rules as those which branch, and those which do not.

The basic idea behind the rules is that given a complex formula $X$ of the language assumed to be true, we can infer what other, less complex formulas must also be true as a consequence. For this, we need to know what formulas we may encounter in our language, and what we can do with them.

First, we have the basic case, where everything is either an atomic formula $P$, a conjunction $Y \wedge Z$, a disjunction $Y \vee Z$, a conditional $Y \rightarrow Z$, or a negation $\neg Y$. Now as it turns out, it is a good idea to take the negation of each of these formulas separately. So we have the negation of an atomic formula $\neg P$, the negation of a conjunction $\neg (Y \wedge Z)$, the negation of a disjunction $\neg(Y \vee Z)$, the negation of a conditional $\neg (Y \rightarrow Z)$, or the negation of a negation $\neg \neg Y$. This covers every possible negated formula form, and the two sets cover every possible formula form. Here is a diagram of this:

Now, as far as our rules are concerned, we will not have rules for $P$ and $\neg P$, but we will have rules for every other form. The principles behind these rules will be familiar if you have ever taken a logic course before.

Non-branching rules

First, we will consider non-branching rules, since they are simpler. And we shall start with the simplest of them all.

Double negation

The double negation rule is extremely simple. If you have a formula of form $\neg \neg X$ occurring on a branch of the tree, you can extend that branch with $X$. In practice, this simply looks like this:

Why does this rule work? Simply because of the way structures are defined. In particular, if you have a structure $\mathbf{S}$, and $\mathbf{S} \models \neg \neg X$, then by definition of $\neg$, $\mathbf{S} \not\models \neg X$, and so by the same definition, $\mathbf{S} \models X$. This works the other way around too, but we are always moving from more complex to simpler formulas in tableau systems, so we do not need to consider the reverse.

Here is a representation of the above in a truth table:

Conjunction

The conjunction rule is another one of these really simple rules. It says that if you have a formula of form $X \wedge Y$ on a branch, then you can extend that branch with either $X$ or $Y$, i.e., with either the left or the right side. Like this:

Clearly, by two successive applications of the rule on $X \wedge Y$, you can also get the following:

Now why does this rule work? Again, it is a simple matter of checking that whenever $\mathbf{S} \models X \wedge Y$, $\mathbf{S} \models X$, and $\mathbf{S} \models Y$. In fact, this is literally just the definition of how $\wedge$ behaves in any structure, so we don’t have to show anything. Of course, we can represent this in a truth table, the exact one that was given above for $\wedge$:

Negated disjunction

The next type of non-branching rule that we cover is a bit more elaborate than the previous ones. It is of the following form, similar to the simple $\wedge$ rule above.

Now why does this work? The above is an instance of what may be called DeMorgan’s laws. The relevant instance is the following (usually formulated in the second part as a single conjunction $\neg X \wedge \neg Y$):

As you can see, our rule just codifies the above instance of DeMorgan’s law. And once again, with two successive application of the rule, you can get the negation of either formula $X$ or formula $Y$, if needed. Compare the following table:

We can stop now for a second and look at our initial question, that of proving that $X \vee \neg X$ is a tautology. As mentioned, in order to do this, we need to put its negation at the top of our tree. Then, we have to apply our rules until we get to an explicit contradiction of form $Y \wedge \neg Y$ (for some $Y$). Thus:

The above is a complete proof of $X \vee \neg X$ being a tautology. You might be asking what the symbol $\otimes$ stands for at the end. It represents that the branch (the only one of the tree) is ‘closed’, because both a formula and its negation occurs on it. Where? Well, that is given by the numbers below $\otimes$, namely line 2 and 4. Line 2 has the formula $\neg X$, while line 4 has the formula $X$ on it, so we have both $X$ and $\neg X$. Thus, we have our desired explicit contradiction derived from the negation of the tautology candidate. This means that $X \vee \neg X$ is a tautology according to our system. Nice!

Let’s get back to our other rules before we go further into examples.

Negated conditional

The negated conditional is another one of those non-branching rules that are not immediately obvious. It is specified as follows:

Why does this work? Again, it just codifies a fact, the following fact, from our semantics:

Here is the truth-table fragment to compare:

This concludes our non-branching rules. Now we turn to our branching ones.

Branching rules

As mentioned above, our tree only ever branches to two separate branches from any one point. Thus, our branching rules are all of the form:

Why do we need branching rules? Note that in all of the above examples, the assumption that a certain complex formula is true determined exactly the truth values of some simpler formulas. In the truth table illustrations, this just means that for each complex formula, they were only true in one, and only one, row (the one in gray), so we just had to check what truth values the simpler formulas received in that row (put in bold). However, many formulas are true in several rows in a truth-table. In that case, we need to consider the possibilities that afford the complex formula to be true separately. And this gets compounded if we go further and encounter another such formula, and another one, and so on.

Disjunction

The disjunction rule is the simplest rule of the branching ones. In many ways, it is like the conjunction rule. It looks like this:

Here is the reasoning behind this rule. As we know, $\mathbf{S} \models X \vee Y$ iff $\mathbf{S} \models X$ or $\mathbf{S} \models Y$ (or both). The problem is that just the fact that $\mathbf{S} \models X \vee Y$ does not tell us whether $\mathbf{S} \models X$ or $\mathbf{S} \models Y$ or both. It only tells us that it is at least one of these. Given this lack of information, we need to consider the consequences separately. Interestingly, we need not consider the case where both $X$ and $Y$ is true separately. But we also don’t make any explicit assumptions about what the truth-value of the other formula is on either branch. So all we do is consider the case where $X$ is true, whatever truth value $Y$ may have ($T$ or $F$), and consider the case where $Y$ is true, whatever truth value $X$ may have ($T$ or $F$). Here is the table representation:

As described above, when we branch to $X$, we are considering either line 1 or line 2 of the truth table. When we branch to $Y$, we are considering either line 1 or line 3 of the truth table.

Negated conjunction

Negated conjunction is also an instance of DeMorgan’s laws. It is as follows:

Again, we can show the following:

Again, on either branch, we do not make assumptions about the truth value of the formula on the other branch. Thus, on the left branch, we assume $\neg X$ is true, but nothing about $\neg Y$ being true or false, and conversely for the right branch. In table representation:

Conditional

The rule for conditionals is our last rule for the system. It also has a form that may make you stop and think why it is formulated as such.

The reasoning behind it is as follows:

Or in truth table form:

As usual, the rule form only explicitly represents the possibility where $\neg X$ is true, and the possibility where $Y$ is true, leaving open whether $Y$ is true or false on the left branch (and similarly for $\neg X$ on the right one).

The strategy

Here is the strategy again, now with all our rules in hand. Suppose you have a formula $X$ that is a candidate for being a tautology. In order for us to show this in our system, we first have to take $\neg X$, and put that at the root of our tree. Then, we have to apply our rules until we have an explicit contradiction of form $Y$ and $\neg Y$ on each branch of the tree.

Suppose we want to show something quite elaborate, like the following: $$(X \rightarrow Y) \rightarrow (\neg X \vee Y)$$

Since the formula is $(X \rightarrow Y) \rightarrow (\neg X \vee Y)$, again, we put its negation at the root, thus:

The next step is to apply one of the rules. For this, you need to identify whether the formula is negated or not, and what the main connective of the formula is, or in the negated case, what the main connective after the negation sign is. Here, the answer is: it is a negated conditional. Obviously, you then apply the negated conditional rule. In fact, we don’t quite see where we are going yet, so we can apply it twice to get both possibilities. Thus:

Now that we have two formulas, we have a choice how we want to proceed. On the other hand, unlike with other systems, we do not have a choice about which rules to apply. Each formula admits of one, and only one, rule, depending on its form.

In general, it is usually better to apply first all the rules that do not branch, and then apply any branching rules. If you think about it, this makes sense, since each branching rule doubles the work we have to carry out. At any rate, the non-branching rule is the one for $\neg \vee$, so we can start with that, and apply it twice:

So far, we only have a single branch, and that branch is open. On the other hand, we still have formulas on which to apply rules. So we are certainly not done. One trivial step is to get rid of the double negation in line 4. This will not help us much, but it will simplify things a bit. Thus:

Now most of the formulas in the proof are ‘exhausted’. There is no rule for $\neg Y$ or $X$ to apply, and for all the other formulas (except one), we have applied the appropriate rules as many times as possible. So we are left with $X \rightarrow Y$. This is a branching rule, so now we branch.

Our tree is now complete, there are no more rules to apply. Now comes the crucial part. You have to see if each of the branches are closed. Again, this means that you have a formula of form $Z$ and a formula of form $\neg Z$ on each branch. Note that each branch is the sequence of formulas from the root to one of the leaves. Thus, the first branch here is from $\neg((X \rightarrow Y) \rightarrow (\neg X \vee Y))$ to $\neg X$, the second branch is from $\neg((X \rightarrow Y) \rightarrow (\neg X \vee Y))$ to $Y$, through all the other formulas.

Let’s take the first branch. Can you see a contradiction? I can, since line 6 has $X$ on it, and line 7 (left) has $\neg X$ on it. So the first branch is closed. Thus:

What about the second branch? Again, there is a contradiction, since line 5 has $\neg Y$, while line 7 (right) has $Y$. Thus:

This completes the proof. Once you have a complete proof of a formula in the system, you can say that that formula is a theorem of zeroth-order logic. Thus, $(X \rightarrow Y) \rightarrow (\neg X \vee Y)$ is a theorem of zeroth order logic. We represent this as follows: $$\vdash(X \rightarrow Y) \rightarrow (\neg X \vee Y)$$ The symbol $\vdash$ means something like ‘syntactically provable’. It is the syntactic equivalent to being a tautology in the semantics. In fact, being a tautology (in the semantics) can be represented as follows: $$\models(X \rightarrow Y) \rightarrow (\neg X \vee Y)$$ This makes sense, as it is just like writing $\mathbf{S} \models (X \rightarrow Y) \rightarrow (\neg X \vee Y)$, except we omit a specific structure designation $\mathbf{S}$, since it is modeled by all structures, not just a specific one.

Here is another proof to inspect, with more branching, before it is your turn:

Note that we could have made this derivation even longer, but we opted to apply $\neg\wedge$ to line 3 to extend only the right-side branch of the tree (to line 5). This is because it would not have made any difference on the left-hand side, given that it closed by $\neg (Y \vee \neg Y)$ alone (line 4, then 8 and 9). In any derivation, you are looking to close every branch and nothing more. Thus, you can make derivations significantly shorter if you cut out the steps that are not necessary to close a branch.

Here is an intuitive explanation of why $((Y \vee \neg Y)\rightarrow X) \rightarrow (X \wedge (Y \vee \neg Y))$ is a tautology. If you look at the first half of the formula, it says that $(Y \vee \neg Y) \rightarrow X$. I.e., if $Y \vee \neg Y$, then $X$. But since $Y \vee \neg Y$ is known to be a tautology that holds in all structures, if it entails $X$, then $X$ would also be a tautology (since again, $Y \vee \neg Y$ holds in every structure, and so if in every structure, it entails $X$, $X$ holds in every structure). But if that is the case, then both $Y \vee \neg Y$ and $X$ must hold (both being tautologies).