In this example, different symbol sequences just try to complete one mission: print"Hello, World Briefly, syntax is a sequence of symbols, what you see; and semantics is the meaning behind the symbols, what you understand 3 Soundness theorem Example4. Given a proposition a=(A→B)→(A→C)→(B→C), there is a truth valuation which make it false. Consider the tableau with the root as F a Following the non-contradictory path of tableau with root F a, we observe that if truth value of a with truth valuation v is the same as sign of root, it also holds for each entry along that on-contradictory path In preceding example, we have observed that there is a mapping between a truth valuation and the sign of proposition of each entry along the non-contradictory paths. Generally, we have the following lemma. Lemma 1. Ifv is a valuation that agrees with the root entry of a given tableau T given as UTn then t has a path P every entry of which agrees with v Sketch. While the tableau is being extending, the non-contradictory path is also extended after entry is reduced. Then we can apply induction principle to the non-contradictory path. Let Pn the non-contradictory path. Then Pn+1 is the new non-contradictory path after the reduction of a By this lemma, we can easily prove the following soundness theorem Theorem 2 (Soundness). If a is tableau provable, then a is valid, i. e. H a=a Soundness theorem means that a proposition must be valid if it has a tableau proof 4 Completeness Theorem Tableaux proof system contains both syntax and semantics Example 5. Given a proposition(a+(B+2)), consider its tableau proof. We all know(a-(B-m)is never a valid proposition. Along the only one path, we can construct a assignment, where A()=F, A(B)=T, A(a)=T. a truth valuation V extended by A make it Generally, we have the following Lemma Lemma 3. Let P be a noncontradictory path of a finished tableau T. Define a truth assignment A on all propositional letters A as followsIn this example, different symbol sequences just try to complete one mission: print ”Hello, World!” on the screen. Briefly, syntax is a sequence of symbols, what you see; and semantics is the meaning behind the symbols, what you understand. 3 Soundness Theorem Example 4. Given a proposition α = ((A → B) → (A → C)) → (B → C), there is a truth valuation which make it false. Consider the tableau with the root as F α Following the non-contradictory path of tableau with root F α, we observe that if truth value of α with truth valuation V is the same as sign of root, it also holds for each entry along that non-contradictory path. In preceding example, we have observed that there is a mapping between a truth valuation and the sign of proposition of each entry along the non-contradictory paths. Generally, we have the following lemma. Lemma 1. If V is a valuation that agrees with the root entry of a given tableau τ given as ∪τn, then τ has a path P every entry of which agrees with V . Sketch. While the tableau is being extending, the non-contradictory path is also extended after a entry is reduced. Then we can apply induction principle to the non-contradictory path. Let Pn the non-contradictory path. Then Pn+1 is the new non-contradictory path after the reduction of a node. By this lemma, we can easily prove the following soundness theorem. Theorem 2 (Soundness). If α is tableau provable, then α is valid, i.e. ⊢ α ⇒⊨ α. Soundness theorem means that a proposition must be valid if it has a tableau proof. 4 Completeness Theorem Tableaux proof system contains both syntax and semantics. Example 5. Given a proposition (α → (β → γ)), consider its tableau proof. We all know (α → (β → γ)) is never a valid proposition. Along the only one path, we can construct a assignment, where A(γ) = F, A(β) = T, A(α) = T. A truth valuation V extended by A make it false. Generally, we have the following Lemma. Lemma 3. Let P be a noncontradictory path of a finished tableau τ . Define a truth assignment A on all propositional letters A as follows: 2