In predicate language, we introduce predicate, quantifier, function, constant, and variable to en hance the expressing power. In order to accommodate the changes, several new tableaux are introduced. The soundness of the proof system looks broken because of these new ones. So we need to reprove the soundness of the new tableau proof system. However the proof of soundness theorem is very similar to the one in propositional logic. We need only pay attention to the case of quantifiers. Here, we mean how to establish the connection between syntax and semantics of tableaux related with quantifiers. Especially, the interpretations associated with all-style quantifier are very difficult to understand. Because we want to use information as little as possible to check all cases Lemma 1. If T=UTn is a tableau from a set of sentences S with root Fa, then any C-structure A that is a model of Suna can be extended to one agreeing with every entry on some path P through T. Recall that A agrees with Ta(Fa) if a is true(false) in A Theorem 2(Soundness). If there is a tableau proof r of a from S, then Sha 3 Completeness theorem 3.1 Proof In our life, sometimes you know something is definitely right. But you may find it is hard to persuade others for you cannot give a reasonable argument. Is there any problem which is right but we can not give a proof? The answer is positive. Completeness theorem guarantees that there must exist a proof if it is right in first order logic. If you cannot prove it, it just means that you are unlucky and you need do better and harder work Theorem 3. Suppose P is a noncontradictory path through a complete systematic tableau t from S with root Fa. There is then a structure A in which a is false and every sentence in s is true 1. If FB occurs on P, then B is false in A 2. If TB occurs on P, then B is true in A Corollary 4. For every sentence a and set of sentences S of L, either 1. the CST from S with root Fa is a tableau proof of a from S 2. there is a noncontradictory branch through the complete systematic tableau that yields a struc ture in that a is false and every element of s is true 3.2 Model construction Actually, the proof show us a way to construct a real model to show that a sentence is true or fal while the model is still abstract because we may not find a real exampleIn predicate language, we introduce predicate, quantifier, function, constant, and variable to en￾hance the expressing power. In order to accommodate the changes, several new tableaux are introduced. The soundness of the proof system looks broken because of these new ones. So we need to reprove the soundness of the new tableau proof system. However the proof of soundness theorem is very similar to the one in propositional logic. We need only pay attention to the case of quantifiers. Here, we mean how to establish the connection between syntax and semantics of tableaux related with quantifiers. Especially, the interpretations associated with all-style quantifier are very difficult to understand. Because we want to use information as little as possible to check all cases. Lemma 1. If τ = ∪τn is a tableau from a set of sentences S with root F α, then any L-structure A that is a model of S ∪ {¬α} can be extended to one agreeing with every entry on some path P through τ .( Recall that A agrees with T α(F α) if α is true(false) in A.) Theorem 2 (Soundness). If there is a tableau proof τ of α from S, then S |= α. 3 Completeness theorem 3.1 Proof In our life, sometimes you know something is definitely right. But you may find it is hard to persuade others for you cannot give a reasonable argument. Is there any problem which is right but we can not give a proof? The answer is positive. Completeness theorem guarantees that there must exist a proof if it is right in first order logic. If you cannot prove it, it just means that you are unlucky and you need do better and harder work. Theorem 3. Suppose P is a noncontradictory path through a complete systematic tableau τ from S with root F α. There is then a structure A in which α is false and every sentence in S is true. 1. If F β occurs on P, then β is false in A. 2. If T β occurs on P, then β is true in A. Corollary 4. For every sentence α and set of sentences S of L, either 1. the CST from S with root F α is a tableau proof of α from S. or 2. there is a noncontradictory branch through the complete systematic tableau that yields a struc￾ture in that α is false and every element of S is true. 3.2 Model construction Actually, the proof show us a way to construct a real model to show that a sentence is true or false, while the model is still abstract because we may not find a real example. 2