7.2.8 Sidetrack: Practical Enhancements for Tableaux
Additional, optional tableaux rules.
Now that we've seen a first application, let's make a practical improvement to our tableaux calculus. So far, we have only given tableaux expansion rules for the connectives 
and 
. While it is possible to get by with rules for only these two connectives in PLNQ, it is a bit unnatural and tedious: we always have to eliminate the other connectives. In this section, we will make the calculus less frugal by adding rules for them.
Derived Inference Rules
We add such new rules to our calculus as derived rule s, i.e. inference rules that only abbreviate deductions in the original calculus. Generally, adding derived inference rules does not change the logical behaviour of a calculus and is therefore a safe thing to do. In particular, we will add the following three rules for the connective 
to our tableaux system.
Chaining
We will now convince ourselves that theses rules are derived rules. Take for instance the third rule. It is so useful that we give it a name: We call it the chaining rule . The green formulae on the tableaux are the ones we take over into our derived inference rule.
In a similar way we derive rules for other common connectives 
and 
. By the way, it is a worthwhile exercise to spell out the abbreviated tableaux for some of the derived rules.
With these rules, the tableaux we have seen before has the following simpler form:
