| ||||||||||||||||||||||||||||||
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 |
