Processing math: 100%

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 YZ, a disjunction YZ, a conditional YZ, or a negation ¬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 ¬P, the negation of a conjunction ¬(YZ), the negation of a disjunction ¬(YZ), the negation of a conditional ¬(YZ), or the negation of a negation ¬¬Y. This covers every possible negated formula form, and the two sets cover every possible formula form. Here is a diagram of this:

image

Remark 5.3. It might seem like there is a problem here, since ¬Y does not appear in the diagram, only ¬¬Y. But this is not the case, since if we consider ¬Y, and what Y could be, it could either be a negated formula or a non-negated one. If it is negated, then it is a double negation, which is covered by ¬¬Y. If it is a simple negation, then Y is either a complex or an atomic formula, which is also covered by the diagram. So there is nothing missing.

Now, as far as our rules are concerned, we will not have rules for P and ¬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 ¬¬X occurring on a branch of the tree, you can extend that branch with X. In practice, this simply looks like this:

image
Double negation rule

Why does this rule work? Simply because of the way structures are defined. In particular, if you have a structure 𝐒, and 𝐒¬¬X, then by definition of ¬, 𝐒⊭¬X, and so by the same definition, 𝐒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:

X ¬X ¬¬X
𝐓 F 𝐓
F T F

Conjunction

The conjunction rule is another one of these really simple rules. It says that if you have a formula of form XY 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:

image
image
Conjunction rule

Clearly, by two successive applications of the rule on XY, you can also get the following:

image

Now why does this rule work? Again, it is a simple matter of checking that whenever 𝐒XY, 𝐒X, and 𝐒Y. In fact, this is literally just the definition of how 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 :

X Y XY
𝐓 𝐓 𝐓
T F F
F T F
F F F

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 rule above.

image
image
Negated disjunction rule

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 ¬X¬Y):

Proposition 5.6. If 𝐒¬(XY), then 𝐒¬X and 𝐒¬Y.

Proof. Suppose 𝐒¬(XY). Then, 𝐒⊭XY. Now 𝐒XY iff either 𝐒X, 𝐒Y, or both. Thus if 𝐒⊭XY, that means none of these cases hold. So that leaves us with 𝐒⊭X and 𝐒⊭Y. Thus, 𝐒¬X and 𝐒¬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:

X Y ¬X ¬Y XY ¬(XY)
T T F F T F
T F F T F F
F T T F F F
F F 𝐓 𝐓 F 𝐓

We can stop now for a second and look at our initial question, that of proving that X¬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¬Y (for some Y). Thus:

image

The above is a complete proof of X¬X being a tautology. You might be asking what the symbol 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 , namely line 2 and 4. Line 2 has the formula ¬X, while line 4 has the formula X on it, so we have both X and ¬X. Thus, we have our desired explicit contradiction derived from the negation of the tautology candidate. This means that X¬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:

imageimage
Negated conditional rule

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

Proposition 5.7. If 𝐒¬(XY), then 𝐒X and 𝐒¬Y.

Proof. Suppose 𝐒¬(XY). Then, 𝐒⊭XY. But 𝐒XY iff whenever 𝐒X, 𝐒Y. So again, by negating both sides of the biconditional, 𝐒⊭XY iff it is not the case that if 𝐒X, then 𝐒Y. So 𝐒⊭XY iff 𝐒X but 𝐒⊭Y. Or in other words, iff 𝐒X and 𝐒¬Y. Which is what we wanted to show. ◻

Here is the truth-table fragment to compare:

X Y ¬Y XY ¬(XY)
T T F T F
𝐓 F 𝐓 F 𝐓
F T F T F
F F T T F

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:

image

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:

image
Disjunction rule

Here is the reasoning behind this rule. As we know, 𝐒XY iff 𝐒X or 𝐒Y (or both). The problem is that just the fact that 𝐒XY does not tell us whether 𝐒X or 𝐒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:

X Y XY
𝐓 𝐓 𝐓
𝐓 F 𝐓
F 𝐓 𝐓
F F F

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:

image
Negated conjunction rule

Again, we can show the following:

Proposition 5.8. If 𝐒¬(XY), then 𝐒¬X or 𝐒¬Y (or both).

Proof. Suppose 𝐒¬(XY). Then, 𝐒⊭XY. But 𝐒XY iff 𝐒X and 𝐒Y, so 𝐒⊭XY iff either 𝐒⊭X or 𝐒⊭Y, or both. So 𝐒¬X, or 𝐒¬Y, or both. ◻

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 ¬X is true, but nothing about ¬Y being true or false, and conversely for the right branch. In table representation:

X Y ¬X ¬Y XY ¬(XY)
T T F F T F
T F F 𝐓 F 𝐓
F T 𝐓 F F 𝐓
F F 𝐓 𝐓 F 𝐓

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.

image
Conditional rule

The reasoning behind it is as follows:

Proposition 5.9. If 𝐒XY, then 𝐒¬X or 𝐒Y (or both).

Proof. The proof follows the usual lines. Suppose 𝐒XY. Then, whenever 𝐒X, 𝐒Y. We have already seen that this is false when 𝐒X but 𝐒⊭Y. This leaves 3 other options left for it to be true.

  1. First, if 𝐒X and 𝐒Y, clearly, 𝐒XY. Note that 𝐒X only if 𝐒⊭¬X, but 𝐒Y.

  2. Second, if 𝐒⊭X but 𝐒Y, then 𝐒XY again. This is the case where both 𝐒¬X (because 𝐒⊭X) and 𝐒Y.

  3. Third, if 𝐒⊭X and 𝐒⊭Y, then still, 𝐒XY. Again, this means that 𝐒¬X, but 𝐒⊭Y in this case.

As you can see, in all three cases where 𝐒XY, it is true that either 𝐒¬X or 𝐒Y or both. Indeed, those are exactly the three options we have for XY to be true in 𝐒◻

Or in truth table form:

X Y ¬X XY
T 𝐓 𝐅 𝐓
T F F F
F 𝐓 𝐓 𝐓
F 𝐅 𝐓 𝐓

As usual, the rule form only explicitly represents the possibility where ¬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 ¬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 ¬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 ¬Y on each branch of the tree.

Suppose we want to show something quite elaborate, like the following: (XY)(¬XY)

Remark 5.4. You may note the similarity between this formula schema and the rule for conditionals. Of course, this is no accident. In fact, every one of our rules can be turned into a tautology in our system, with the use of .

Since the formula is (XY)(¬XY), again, we put its negation at the root, thus:

image

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:

image

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 ¬, so we can start with that, and apply it twice:

image

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:

image

Now most of the formulas in the proof are ‘exhausted’. There is no rule for ¬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 XY. This is a branching rule, so now we branch.

image

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 ¬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 ¬((XY)(¬XY)) to ¬X, the second branch is from ¬((XY)(¬XY)) 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 ¬X on it. So the first branch is closed. Thus:

image

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

image

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, (XY)(¬XY) is a theorem of zeroth order logic. We represent this as follows: (XY)(¬XY) The symbol 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: (XY)(¬XY) This makes sense, as it is just like writing 𝐒(XY)(¬XY), except we omit a specific structure designation 𝐒, since it is modeled by all structures, not just a specific one.

Definition 5.2 (Theorem). Let X, Y be any formulas. We call a branch of a tree closed provided there are some formulas of form Y, ¬Y occurring on it. We call a tree closed if all its branches are closed. Then, X is a theorem of zeroth-order logic provided there is a closed tree with ¬X at its root. In such cases, we also write X, and call the closed tree for ¬X the tableau (tree) proof of X.


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

image

Note that we could have made this derivation even longer, but we opted to apply ¬ 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 ¬(Y¬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¬Y)X)(X(Y¬Y)) is a tautology. If you look at the first half of the formula, it says that (Y¬Y)X. I.e., if Y¬Y, then X. But since Y¬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¬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¬Y and X must hold (both being tautologies).

Exercise 5.3. Prove that the following formulas are all theorems of the tableau system:

  1. Y(XY);

  2. (¬X¬Y)¬(XY);

  3. (¬X¬Y)¬(XY);

  4. ¬(XY)(¬X¬Y);

  5. ¬(XY)(¬X¬Y);

  6. (¬XY)(XY);

  7. (XY)(¬Y¬X);

  8. ((XY)((XZ)(YZ)))Z.

License

Icon for the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License

Learning Logic Backwards Copyright © by Peter Susanszky is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License, except where otherwise noted.

Share This Book