1.A(A)=T if TA 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 Sketch. We have known that a truth assignment can uniquely determine a truth valuation. Along a noncontradictory path, we can first construct a truth assignment with the method stated in lemma When the tableau is being extended, a complicated proposition would be decomposed into one/two relatively simpler proposition(s). Then we just reverse the course. The induction is on depth of a In this lemma, we should pay attention to the method to construct a truth assignment. All members of the support of a proposition occur on the leaf node of its formation tree. But some would not ccur on a noncontradictory path of a tableau. We only assign a proposition letter with sign T to true on that path. All others are assigned to false if it has a sign with f and does not occurs. This is called the minimal positive information principle With this lemma, we have completeness theorem Theorem 4(Completeness). If a is valid, then a is tableau provable, i.e. F a=H a. In fact, any finished tableau with root entry Fa is a proof of a and so, in particular, the complete systematic tableaux with root Fo is such a proof. Completeness theorem says that if a proposition is valid, we can find it a tableaux proof During the proof, we show a way to construct a model such that v(a)= f if the tableau is not contradictory 5 Hilbert Proof System We introduce Hilbert proof system, also known as axiom proof system, as a reference to tableaux proof system We first give all the axioms. There are only three Definition 5. The axioms of Hilbert system are all propositions of the following forms 1.(a→(B→a) 2.(a→(6→)→(a→3)→(a→) Actually, you can define different axioms. But we hope there are as few as possible. Just think about adequacy of connectives We also need the famous Modus Ponens principle, which is the only inference rule applying to propositions1. 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. Sketch. We have known that a truth assignment can uniquely determine a truth valuation. Along a noncontradictory path, we can first construct a truth assignment with the method stated in lemma. When the tableau is being extended, a complicated proposition would be decomposed into one/two relatively simpler proposition(s). Then we just reverse the course. The induction is on depth of a proposition. In this lemma, we should pay attention to the method to construct a truth assignment. All members of the support of a proposition occur on the leaf node of its formation tree. But some would not occur on a noncontradictory path of a tableau. We only assign a proposition letter with sign T to true on that path. All others are assigned to false if it has a sign with F and does not occurs. This is called the minimal positive information principle. With this lemma, we have completeness theorem. Theorem 4 (Completeness). If α is valid, then α is tableau provable, i.e. ⊨ α ⇒⊢ α. In fact, any finished tableau with root entry F α is a proof of α and so, in particular, the complete systematic tableaux with root F α is such a proof. Completeness theorem says that if a proposition is valid, we can find it a tableaux proof. During the proof, we show a way to construct a model such that V(α) = F if the tableau is not contradictory. 5 Hilbert Proof System We introduce Hilbert proof system, also known as axiom proof system, as a reference to tableaux proof system. We first give all the axioms. There are only three. Definition 5. The axioms of Hilbert system are all propositions of the following forms: 1. (α → (β → α)) 2. ((α → (β → γ)) → ((α → β) → (α → γ))) 3. (¬β → ¬α) → ((¬β → α) → β) Actually, you can define different axioms. But we hope there are as few as possible. Just think about adequacy of connectives. We also need the famous Modus Ponens principle, which is the only inference rule applying to propositions. 3