2. if r is a finite tableau, P a path on T, E and entry of T occurring on P. TI is obtained from T by adjoining an atomic tableau with root entry e to t at the end of the path P, then T/ is also a tableau. Here the requirement that c be new in Case 7b and &a means that it is one of the ci that do not appear in any entries on P.(In actual practice it is simpler in terms of pokkeeping to choose one not appearing at any node of T) 3. If To is a finite tableau and To, T1, .. Tn,... is a sequence of tableaux such that, for every n>0, Tn+1 is constructed from Tn by an application of 2, then T= UTn is also a tableau For 3-style, we always introduce new constant which does not occur before along the path which it is in. If the constant is not new to this language, it should name a specified element. So when different structure is concerned, c could not just be that witness. However, if it is a new constant it can be interpreted as your wish. Then we would not be in trouble in this way. Simply, we can relax to a constant is not in current tableau It is important that we should always introduce a new constant when handle a 3-style entry Consider the following example Example1.Is(彐x)B(x)→(x)R(x) valid? Proof. With a semantic approach, we know that it is false for the truth that some member has a property does not mean that all members have the same property. But if we use tableau proof, we could prove it by wrongly using 3-style tableaux. Just show you the proof as shown in Figure 2 T(x)R(x)→(x)f(x) T rR(E) F(a)R(a) T R(c. for a new constant c F R(c) Figure 2: A wrong example about 3-style This is a tableau proof. But we should be aware the entry within a box. Actually, it should also introduce a new constant. Then the tableau is noncontradictory. So when a 3-style tableau is applied, you must introduce a new constant never ever occurs before Definition 2. Tableaur from S. The definition for tableaux from s is the same as for ordinary tableaux except that we include an additional formation rule 2. If T is a finite tableau from S, p a sentence from S, P a path on T and r/ is obtained from T by adjoining T'y to the end of the path P, then r/ is also a tableau from s2. if τ is a finite tableau, P a path on τ , E and entry of τ occurring on P. τ ′ is obtained from τ by adjoining an atomic tableau with root entry E to τ at the end of the path P, then τ ′ is also a tableau. Here the requirement that c be new in Case 7b and 8a means that it is one of the ci that do not appear in any entries on P. (In actual practice it is simpler in terms of bookkeeping to choose one not appearing at any node of τ .) 3. If τ0 is a finite tableau and τ0, τ1, . . . , τn, . . . is a sequence of tableaux such that, for every n ≥ 0, τn+1 is constructed from τn by an application of 2, then τ = ∪τn is also a tableau. For ∃-style, we always introduce new constant which does not occur before along the path which it is in. If the constant is not new to this language, it should name a specified element. So when different structure is concerned, c could not just be that witness. However, if it is a new constant, it can be interpreted as your wish. Then we would not be in trouble in this way. Simply, we can relax to a constant is not in current tableau. It is important that we should always introduce a new constant when handle a ∃-style entry. Consider the following example. Example 1. Is (∃x)R(x) → (∀x)R(x) valid? Proof. With a semantic approach, we know that it is false for the truth that some member has a property does not mean that all members have the same property. But if we use tableau proof, we could prove it by wrongly using ∃-style tableaux. Just show you the proof as shown in Figure 2. T (∃x)R(x) → (∀x)R(x) T (∃x)R(x) F (∀x)R(x) T R(c), for a new constant c F R(c) ⊗ Figure 2: A wrong example about ∃-style This is a tableau proof. But we should be aware the entry within a box. Actually, it should also introduce a new constant. Then the tableau is noncontradictory. So when a ∃-style tableau is applied, you must introduce a new constant never ever occurs before. Definition 2. Tableaux from S. The definition for tableaux from S is the same as for ordinary tableaux except that we include an additional formation rule: 2. If τ is a finite tableau from S, φ a sentence from S, P a path on τ and τ ′ is obtained from τ by adjoining T φ to the end of the path P, then τ ′ is also a tableau from S. 2