Example of a tableau proof

Suppose we wanted to prove the following:

A non-empty relation, which is connected, symmetric and transitive must be reflexive.

We could formalise the claim as a sequent thus:

$x$yRxy, "x"y[¬x=y®[RxyÚRyx]], "x"y[Rxy®Ryx], "x"y"z[[RxyÙRyz]®Rxz]|-"xRxx

We will now proceed to construct a tableau, or the outline of a tableau, because it would be a little tedious to set it out in full. (The missing steps are marked with dots. Ticks have been omitted.)

Comments:

Lines 1-5 are the members of the counterexample set.

Line 6 comes from line 5 by the ¬"xj rule.

At this stage it is sensible (as is usually the case) to apply the $xj rule where possible. We do that in lines 7-9.

At this stage it is worth seeing what our overall strategy is going to be. (It is often easiest when constructing a proof, first to work out the outline, and then to fill in the details.)

We have Rbc, and somehow or other, we are going to have to use it to arrive at some contradiction with ¬Raa. Well we can see that we can use line 3 (which says that Rxy is symmetrical) to get Rcb from Rbc (first gambit). And then we can use line 4 (which tells us that Rxy is transitive) to get Rbb from Rbc together with Rcb (second gambit). So far so good. But this doesn't give us a contradiction with Raa. However, we can think like this. Either a=b, in which case we can get Raa from Rbb (third gambit) or it isn't, in which case line 2 (which says that Rxy is connected) will let us infer that [RabÚ Rba]. But given Rab we can get Rba by repeating the pattern of our first gambit, and then from Rab and Rba we can get Raa by repeating the pattern of the second gambit. And that will give us our contradiction with ¬Raa (fourth gambit). Equally, given Rba we can get Rab, and again from Rab and Rba we can get Raa; so that alternative also gives us a contradiction (fifth gambit). And we are done.

So now we can fill in some of the details.

Lines 10-12 constitute our first gambit.

Line 10: from 3 by the "xj rule.

Line 11: from 10 by the "xj rule.

Line 12: from line 11 by the [j®y] rule, and the left branch closes.

Now we have Rcb in our only open branch.

Lines 12-16 together with line 19 in the left branch constitute our second gambit.

Line 13: from 4 by the"xj rule (the missing step is marked by dots).

Line 14: from 13 by the "xj rule.

Line 15: from 14 by the "xj rule.

Line 16: from 15 by the [j®y] rule.

Line 19: from 16 by the ¬[jÙy] rule; and both these branches close.

We are left with Rbb on the right in the only open branch.

Line 18 comes from line 2 by two applications of the "xj rule.

Line 20 comes from line 19 by the [j®y] rule, and constitutes our thought that either a=b or [RabÚRab].

Line 21 comes from line 20 by the ¬¬j rule.

Lines 22 comes from line 21 together with Rbb (line 16) by the right hand = rule.

Lines 20-22 constitute our third gambit.

Finally the two branches starting at line 23 constitute our fourth and fifth gambits – the details of which can be filled in by copying the first and second gambits with appropriate relettering.