Tutorial Contents Tutorial Five: Predicate Calculus: Tableaux - The $xj rule - Bad Mistakes and Technical Mistakes - Ticking - Finished Tableaux - Sequents - Soundness and Completeness - Proof of a syntactic sequent: example
More Tutorials


Finished tableaux


There are two cases in which a tableau may be regarded as finished. It may be regarded as finished if all its branches have closed. (Indeed there is now nothing that can be added to it.) It may also be regarded as finished if every formula in an unclosed branch either (a) has been ticked (for one of the reasons given above), or (b) is a formula beginning """, and nothing new would result if one applied the "xj rule to it again, or (c) is a formula to which no rule may be applied. Here is a simple example:




However, whereas propositional tableaux are bound to finish, some predicate tableaux can never be regarded as finished. Here is a simple example:



And so on.


Print this page Print this page