Theorem 3. Every CST from a set of premises is finished Unlike the CST in previous lecture, we can not guarantee the tableau to be finite. Because 2 could be a infinite set. It means we can introduce premises as many as possible into our tableau Anyway, every entry in CST would be finally reduced. We can give several ways to expand CSt in detail. Even if the proposition is an infinite sequence, we can also obtain the same property 3 Soundness theorem We first give the following lemma Lemma 4. If a valuation v makes every aE 2 true and agrees with the root of a tableau t from 2, then there is a path in T every entry of which agrees with v It sets up a connection between truth valuation v and sign of entries along noncontradictory path When giving proof, we need handle propositions introduced from 2 whose corresponding entry is always with sign T By this lemma, we can easily prove the following soundness theorem Theorem 5( Soundness). If there is a tableau proof of a from a set of premises 2, then a is a consequence of∑,te.∑卜a→∑Fa Soundness theorem means that a propositon must be a logic consequence of 2 if it can be deduced 4 Completeness Theorem Similarly, we have the following Lemma Lemma 6. Let P be a noncontradictory path in a finished tableau T from 2. Define a valuation v as the last section, then it agrees with all entries on P and so in particular makes every proposition B∈∑ true. It is nearly the same as previous proof for completeness theorem without premises except that propositions from 2 should be handled specially With this lemma, we have completeness theorem Theorem 7(Completeness). If a is consequence of a set 2 of premises, then there is a tableau uction of a from∑,i.e,∑Fa→∑a. Completeness theorem says that if a propostion is a consequence of a set of propositions, it can be deduced from this setTheorem 3. Every CST from a set of premises is finished. Unlike the CST in previous lecture, we can not guarantee the tableau to be finite. Because Σ could be a inifinite set. It means we can introduce premises as many as possible into our tableau. Anyway, every entry in CST would be finally reduced. We can give several ways to expand CST in detail. Even if the proposition is an infinite sequence, we can also obtain the same property. 3 Soundness Theorem We first give the following lemma. Lemma 4. If a valuation V makes every α ∈ Σ true and agrees with the root of a tableau τ from Σ, then there is a path in τ every entry of which agrees with V. It sets up a connection between truth valuation V and sign of entries along noncontradictory path. When giving proof, we need handle propositions introduced from Σ whose corresponding entry is always with sign T. By this lemma, we can easily prove the following soundness theorem. Theorem 5 (Soundness). If there is a tableau proof of α from a set of premises Σ, then α is a consequence of Σ, i.e. Σ ` α ⇒ Σ  α. Soundness theorem means that a propositon must be a logic consequence of Σ if it can be deduced from Σ. 4 Completeness Theorem Similarly, we have the following Lemma. Lemma 6. Let P be a noncontradictory path in a finished tableau τ from Σ. Define a valuation V as the last section, then it agrees with all entries on P and so in particular makes every proposition β ∈ Σ true. It is nearly the same as previous proof for completeness theorem without premises except that propositions from Σ should be handled specially. With this lemma, we have completeness theorem. Theorem 7 (Completeness). If α is consequence of a set Σ of premises, then there is a tableau deduction of α from Σ, i.e., Σ  α ⇒ Σ ` α. Completeness theorem says that if a propostion is a consequence of a set of propositions, it can be deduced from this set. 2