Tutorial Contents Tutorial Three: Propositional Calculus: Tableaux - The Sentence Tableaux Rules - Testing Arguments for Validity - Sequents - Syntactic Sequents - Semantic Sequents - Soundness and Completeness - Correctness of Sequents and Validity of Arguments
More Tutorials
 

Soundness and completeness

 

As we have seen syntactic sequents are different from semantic sequents. But there is a close connexion between the correctness of a syntactic sequent and the correctness of the corresponding semantic sequent. In fact

 

 

If a syntactic sequent is correct, so is the corresponding semantic sequent, and

If a semantic sequent is correct, so is the corresponding syntactic sequent.

 

In virtue of the first fact, the tableau system is said to be sound – it enables one to prove only the sequents one would like to be able to prove.

 

In virtue of the second fact, the tableau system is said to be complete – it enables one to prove all the sequents one would like to be able to prove.

 

The completeness of the tableau system means that, as well as the direct way of showing that a syntactic sequent is correct, by showing that its counterexample set generates a closed tableau, there is also an indirect way, by showing that the corresponding semantic sequent is correct.

 

The soundness of the tableau system means that, as well as a direct way of showing that a syntactic sequent is incorrect, by showing that its counterexample set does not generate a closed tableau, there is an indirect way, by showing that the corresponding semantic sequent is incorrect: by finding a counterexample. (The availability of an indirect way of showing a syntactic sequent to be incorrect is going to be important, as we shall see, when we come to the predicate calculus.)

 

Print this page Print this page
BackNext