Discrete Mathematics(ID) Spring 2013 Lecture 14: Tableau proof of predicate logic 1 Overview In this lecture, we will show you how to prove the validity of sentences of predicate logic To handle quantifiers, we introduce new atomic tableau. In this lecture, we focus on how to handle quantifiers 2 Atomic tableau In predicate logic, we have introduced variables and two quantifiers 3 and v. All sentences without quantifiers are handled in the same way as propositions in propositional logic, we just consider the cases with quantifiers As we have done in propositional logic, we introduce the atomic tableaux according to their se- mantics. In previous lecture, we already have (Var)p(ar)= x)mp(ar). We have the following new tomic tableaux as in Figure 1. For convenience, we call the tableaux with" for all ground term t T(a)p(a) F(a)p(a) F rp(a) T(V)p(r) T(t) Fp(c) Fp(t) T y(c) for any ground fo term t of Lc constant c term t of Lo constant c Figure 1: Atomic Tableaux with Quantifiers V-style and the other two 3-style According to the definition of truth of Vxy(), all elements in domain of a given structure should be referred as a witness. For V-style, we use for any ground term t. However, once we fix it for some special element in a domain in a tableau, it can not name some others. Then we must duplicate the reducing node in order to guarantee that we can make sure every ground term is its witness e need treat it specially when we define what entry is reduced. It will be introduced late Definition 1. We define tableaux as binary trees labeled with signed sentence(of Lc) called entries by indi action 1. All atomic tableau are tableaux. The requirement that c be new in Cases 7b and 8a here simply means that c is one of the constants ci added on to L to get Cc(which therefore does not appear in p
Discrete Mathematics (II) Spring 2013 Lecture 14: Tableau Proof of Predicate Logic Lecturer: Yi Li 1 Overview In this lecture, we will show you how to prove the validity of sentences of predicate logic. To handle quantifiers, we introduce new atomic tableau. In this lecture, we focus on how to handle quantifiers. 2 Atomic tableau In predicate logic, we have introduced variables and two quantifiers ∃ and ∀. All sentences without quantifiers are handled in the same way as propositions in propositional logic, we just consider the cases with quantifiers. As we have done in propositional logic, we introduce the atomic tableaux according to their semantics. In previous lecture, we already have ¬(∀x)φ(x) ≡ (∃x)¬φ(x).We have the following new atomic tableaux as in Figure 1. For convenience, we call the tableaux with “for all ground term t” T (∀x)φ(x) T φ(t) for any ground term t of LC F (∀x)φ(x) F φ(c) for a new constant c F (∃x)φ(x) F φ(t) for any ground term t of LC T (∀x)φ(x) T φ(c) for a new constant c Figure 1: Atomic Tableaux with Quantifiers ∀-style and the other two ∃-style. According to the definition of truth of ∀xφ(x), all elements in domain of a given structure should be referred as a witness. For ∀-style, we use for any ground term t. However, once we fix it for some special element in a domain in a tableau, it can not name some others. Then we must duplicate the reducing node in order to guarantee that we can make sure every ground term is its witness. We need treat it specially when we define what entry is reduced. It will be introduced late. Definition 1. We define tableaux as binary trees labeled with signed sentence( of LC) called entries by induction. 1. All atomic tableaux are tableaux. The requirement that c be new in Cases 7b and 8a here simply means that c is one of the constants ci added on to L to get LC(which therefore does not appear in φ ). 1
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 s
2. 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
3 Tableau proof In predicate logic, there are formulas and sentence. Here we only consider the proof system for a sentence, a special formula without free variables. We only consider the tableau proof of sentence With these atomic tableaux, we can define tableau and corresponding properties similarly as in Definition 3. Tableau proofs(from S): Let t be a tableau and p a path in T 1.P is contradictory if, for some sentence a, Ta and Fa both appear as labels of nodes of p 2. T is contradictory if every path on T is contradictory 3.T is a proof of a(from S) if r is a finite contradictory tableau( from S) with its root node labeled Fa. If there is proof T of a(from S), we say a is provable( from S) and write a(Sha) 4. S is inconsistent if there is a proof of aA na from S for some sentence a In proposition logic, every signed proposition is reduced exactly only once. Here, we should pay attention to sentence leading with quantifiers. For sentence r)p(a), it contains no more infor- mation than (c). Then we can claim to have finished it. However, (t) far from exhausts the information of sentence (Va)p(a). It just give us one instance asserted by entry T(Va)p(a). with this in mind, we can define reduction and finish of an entry in V-style Definition 4. Let T= UTn be a tableau( from S), P a path in T, E an entry on P and w the it occurrence of e on P(i.e, the in node on P labeled with E) ed on P if (a)e is neither of the form T(V p(a) nor Fro(r)and, for some j, Ti+1 is gotten from T, by an application Rule (ii)of Definition I to E and a path on T, which is an initial segment of P.(In this case, we say that E occurs on P as the root entry of an atomic (b)e is of the form T(Va)p(a)or F xo(), Tp(ti) or Fp(ti), respectively, is an entry P and there is an(i+1)st occurrence of E on P. 2. T is finished if every occurrence of every entry on T is reduced on every noncontradictory path containing it( and Ty appears on every noncontradictory path of r for every p in S). It is unfinished otherwise. Example 2. Check the following formulas 1.(x)y(x)→(彐x)y(x) 2.(v)(P(x)→Q(x)→(x)P(x)→(vx)Q(x) In previous examples, all tableaux are finite. However, it is only a small part of them. Consider the following example
3 Tableau proof In predicate logic, there are formulas and sentence. Here we only consider the proof system for a sentence, a special formula without free variables. We only consider the tableau proof of sentence. With these atomic tableaux, we can define tableau and corresponding properties similarly as in propositional logic. Definition 3. Tableau proofs (from S): Let τ be a tableau and P a path in τ . 1. P is contradictory if, for some sentence α, T α and F α both appear as labels of nodes of P. 2. τ is contradictory if every path on τ is contradictory. 3. τ is a proof of α ( from S) if τ is a finite contradictory tableau ( from S) with its root node labeled F α. If there is proof τ of α (from S), we say α is provable ( from S ) and write ⊢ α (S ⊢ α). 4. S is inconsistent if there is a proof of α ∧ ¬α from S for some sentence α. In proposition logic, every signed proposition is reduced exactly only once. Here, we should pay attention to sentence leading with quantifiers. For sentence (∃x)φ(x), it contains no more information than φ(c). Then we can claim to have finished it. However, φ(t) far from exhausts the information of sentence (∀x)φ(x). It just give us one instance asserted by entry T(∀x)φ(x). With this in mind, we can define reduction and finish of an entry in ∀-style. Definition 4. Let τ = ∪τn be a tableau ( from S ), P a path in τ , E an entry on P and ω the i th occurrence of E on P ( i.e., the i th node on P labeled with E). 1. ω is reduced on P if (a) E is neither of the form T(∀x)φ(x) nor F(∃x)φ(x) and , for some j, τj+1 is gotten from τj by an application Rule (ii) of Definition 1 to E and a path on τj which is an initial segment of P. (In this case, we say that E occurs on P as the root entry of an atomic tableau.) or (b) E is of the form T(∀x)φ(x) or F(∃x)φ(x), T φ(ti) or F φ(ti), respectively, is an entry on P and there is an (i + 1)st occurrence of E on P. 2. τ is finished if every occurrence of every entry on τ is reduced on every noncontradictory path containing it ( and T φ appears on every noncontradictory path of τ for every φ in S). It is unfinished otherwise. Example 2. Check the following formulas: 1. ((∀x)φ(x) → (∃x)φ(x)). 2. (∀x)(P(x) → Q(x)) → ((∀x)P(x) → (∀x)Q(x)) In previous examples, all tableaux are finite. However, it is only a small part of them. Consider the following example. 3
Example 3. Is the sentence y(R(y, y)VP(, y))AVaR(a, r)) invalid? Solution. If a sentence op is invalid, then mop must be valid. So we can have the tableau proof in n) P(y, y))A VaR(, r)) By(R(, y)v P(y, y)) VcR(a T GR(co, co)V P(co, co)), new constant co T Var R(a, r) T R(co, co) T -R(Co, Co F R(Co, co) T VcR(a, a) R(t1,t1) T V R(T, T R(t2, t2) Figure 3: An example of tableau proof The tableau is not contradictory. So the sentence is not invalid Obviously, no contradiction could be introduced in the right branch. For T(V)R(, a)exists, we can always generate new unreduced entries. So it is a infinite path. Then, when should we erminate reduction procedure? We observe that we are reducing the same set of entries periodically without introducing any valuable information in the non-contradictory path in previous example. With this observation we could terminate the reduction on that path. Generally, we always reduce those 3-style entries first. If a V-style entry use all constants generated by 3-style entries on that path, we could also terminate reduction on that path To prove a formula, we should transform it into a sentence by adding universal quantifier closure in front of it and then apply tableau proof of sentence Example 4. Check the statement
Example 3. Is the sentence (∃y(¬R(y, y) ∨ P(y, y)) ∧ ∀xR(x, x)) invalid? Solution. If a sentence φ is invalid, then ¬φ must be valid. So we can have the tableau proof in figure 3. T (∃y(¬R(y, y) ∨ P(y, y)) ∧ ∀xR(x, x)) T ∃y(¬R(y, y) ∨ P(y, y)) T ∀xR(x, x) T (¬R(c0, c0) ∨ P(c0, c0)), new constant c0 T ∀xR(x, x) T R(c0, c0) T ¬R(c0, c0) T P(c0, c0) F R(c0, c0) ⊗ T ∀xR(x, x) T R(t1, t1) T ∀xR(x, x) T R(t2, t2) . . . Figure 3: An example of tableau proof The tableau is not contradictory. So the sentence is not invalid. Obviously, no contradiction could be introduced in the right branch. For T(∀x)R(x, x) exists, we can always generate new unreduced entries. So it is a infinite path. Then, when should we terminate reduction procedure? We observe that we are reducing the same set of entries periodically without introducing any valuable information in the non-contradictory path in previous example. With this observation, we could terminate the reduction on that path. Generally, we always reduce those ∃-style entries first. If a ∀-style entry use all constants generated by ∃-style entries on that path, we could also terminate reduction on that path. To prove a formula, we should transform it into a sentence by adding universal quantifier closure in front of it and then apply tableau proof of sentence. Example 4. Check the statement {(ψ(x) → (∃x)φ(x))} ⊢ (∃x)(ψ(x) → φ(x)) 4
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 following
4 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 sentence 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
(a)(vx)(y(x)Vv(x)+(Vr)yp(x)V(vx)v(x) (b)(三x)(y→v(x)→(→(x)v(x), not free in y. (c)(彐x)(y?(x)→v(x)→(y(x)→(m)(x) (d)(x)y(x)→v)→(vax)((x)→v), r is not free in y 2. Let y and a be any formula with free variables y and z: let w be any variable not appearing p and v. Give tableau proofs of the following (a) 3. Vy (Vap V)+3rvyVw(p(a/w)vv) (b)ry(y→Vzv(2)→V3yvu(y→(z/) 3. Let p(a1,., n) be a formula in a languange L with all free variables displayed and let n be constant symbols not in L. Show that Var1... V np(a1, .. In) is tableau prov- able if and only if P(c1
(a) (∀x)(φ(x) ∨ ψ(x)) ↔ (∀x)φ(x) ∨ (∀x)ψ(x) (b) (∃x)(φ → ψ(x)) → (φ → (∃x)ψ(x)), x not free in φ. (c) (∃x)(φ(x) → ψ(x)) → (φ(x) → (∃x)ψ(x)). (d) ((∃x)φ(x) → ψ) → (∀x)(φ(x) → ψ), x is not free in ψ. 2. Let φ and ψ be any formula with free variables x, y and z; let w be any variable not appearing in φ and ψ. Give tableau proofs of the following. (a) ∃x∀y(∀zφ ∨ ψ) ↔ ∃x∀y∀w(φ(z/w) ∨ ψ). (b) ∀x∃y(φ → ∀zψ(z)) → ∀x∃y∀w(φ → ψ(z/w)). 3. Let φ(x1, . . . , xn) be a formula in a languange L with all free variables displayed and let c1, . . . , cn be constant symbols not in L. Show that ∀x1 . . . ∀xnφ(x1, . . . , xn) is tableau provable if and only if φ(c1, . . . , c2) is. 6