In this example, different symbol sequences just try to complete one mission: print"Hello, World 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 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 non-contradictory path 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 It sets up a connection between truth valuation V and sign of entries along noncontradictory path 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. Ha=a Soundness theorem means that a proposition must be valid if it has a tableaux pro 4 Completeness Theorem Tableaux proof system contains both syntax and semantics Example 5. Given a proposition(a-(B-7m), 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(y)=F, A(B)=T, A(a=T. a truth valuation V extended by A make it fal 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 follows 1.A(A)=T if TA is an entry on P 2.A(A)=F If v is the unique valuation extending the truth assignment A, then v agrees with all entries ofIn 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. 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 . It sets up a connection between truth valuation V and sign of entries along noncontradictory path. 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 tableaux 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: 1. A(A) = T if T A is an entry on P. 2. A(A) = F otherwise. If V is the unique valuation extending the truth assignment A, then V agrees with all entries of P. 2