4 Complete systematic tableau As we have shown, V-style may cause an infinite path for we can always try to reduce a node just generated. So we also need a mechanical way to guarantee every node could be reduced Similarly, we introduce complete systematic tableau. In it, we define how to introduce ground term ti and new constant ci. If we violate the rule, we may get wrong result Definition 5. We construct the CST, the complete systematic tableau, with any given signed sen ce as the label of its root, by induction. 1. We begin with To an atomic tableau with root the given signed sentence. This atomic tableau is uniquely specified by requiring that in Cases 7a and 8b we use the term ti and that in Cases 76 and Sa we use ci for the least allowable i 2. If e is not of the form T(Va)p(a)or F r(a), we adjoin the atomic tableau with aper E to the end of every noncontradictory path in T that contains w. For E of the form Tr)p(a or F(Va)p(a), we use the least constant ci not yet appearing in the tableau 3. If E is of the form T(Va)p(a)or FEx)p(a)and w is the ith occurrence of e on p we adjoin E To(ti) respectively, to the end of every noncontradictory path in T containing w. If premises S is introduced, it becomes more complicated. Because there may be infinite sentence S. We need determine when the sentence could be introduced into the current path. For example we can introduce one in the odd stage. if the root is defined as o Here, we strictly number all newly introduced constant uniformly. With premises S, we could split reduction into two stages, odd and For example, we can reduce entry in tableau at odd stage and introduce sentence in S at even stage 5 Properties With CST, we can guarantee that every tableau is finished. Even without premises, the tableau proof of a sentence still could be an infinite procedure because of v-style entry and semantics of cop(a) If it is a contradictory tableaux, which means a tableau proof or refutation, the CST is also finite It means that a proof could always terminate in finite steps Exercises 1. Let and w be any formula either with no free variables or with only a free as appropriate Give tableau proofs of each the following4 Complete systematic tableau As we have shown, ∀-style may cause an infinite path for we can always try to reduce a node just generated. So we also need a mechanical way to guarantee every node could be reduced. Similarly, we introduce complete systematic tableau. In it, we define how to introduce ground term ti and new constant ci . If we violate the rule, we may get wrong result. Definition 5. We construct the CST, the complete systematic tableau, with any given signed sen￾tence as the label of its root, by induction. 1. We begin with τ0 an atomic tableau with root the given signed sentence. This atomic tableau is uniquely specified by requiring that in Cases 7a and 8b we use the term ti and that in Cases 7b and 8a we use ci for the least allowable i. 2. If E is not of the form T(∀x)φ(x) or F(∃x)φ(x), we adjoin the atomic tableau with apex E to the end of every noncontradictory path in τ that contains ω. For E of the form T(∃x)φ(x) or F(∀x)φ(x), we use the least constant cj not yet appearing in the tableau. 3. If E is of the form T(∀x)φ(x) or F(∃x)φ(x) and ω is the i th occurrence of E on P we adjoin E T φ(ti) or E F φ(ti) respectively, to the end of every noncontradictory path in τ containing ω. If premises S is introduced, it becomes more complicated. Because there may be infinite sentence in S. We need determine when the sentence could be introduced into the current path. For example, we can introduce one in the odd stage, if the root is defined as 0. Here, we strictly number all newly introduced constant uniformly. With premises S, we could split reduction into two stages, odd and even. For example, we can reduce entry in tableau at odd stage and introduce sentence in S at even stage. 5 Properties With CST, we can guarantee that every tableau is finished. Even without premises, the tableau proof of a sentence still could be an infinite procedure because of ∀-style entry and semantics of ∀xφ(x). If it is a contradictory tableaux, which means a tableau proof or refutation, the CST is also finite. It means that a proof could always terminate in finite steps. Exercises 1. Let φ and ψ be any formula either with no free variables or with only x free as appropriate. Give tableau proofs of each the following. 5