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:

 

  [$xFx"xGx]
$xFx
"xGx
Fa
Ga

 

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

 

 

Fa
"x$yFxy
$yFay
Fab
$yFby
Fbc
And so on.

 

Print this page Print this page
BackNext