Discrete Mathematics(Il) Spring 2012 Lecture 14: Tableau proof of predicate logic Lecturer. YiL 1 Overview n this lecture, we will show you how to prove the validity of sentences of predicate logic ndle 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 -(Vr)p(a)=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(V)p(a) F(r)p(a) F r)p( T(Va)p(a) Tφ(t) Fo(c Fp(t) for any ground for a new for any ground term t of Lc constant c term t of c tant c Figure 1: Atomic Tableaux with Quantifiers V-style and the other two 3-style. According to the definition of truth of Vr(a), 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 We need treat it specially when we define what entry is reduced. It will be introduced late 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
Discrete Mathematics (II) Spring 2012 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. 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. 1
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 n proposition logic, every signed proposition is reduced exactly only once. Here, we should pay attention to sentence leading with quantifiers. For sentence r)o(a), it contains no more infor- mation than p(c. Then we can claim to have finished it. However, p(t) far from exhausts the information of sentence (V r)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 a entry In class, we have introduced several examples. Fortunately, all tableaux are finite. Consider the following example Example 1. Is the sentence y(R(y, y)vP(, y))AVr(, m)) invalid? Solution. If a sentence yp is invalid, then -op must be valid. So we can have the tableau proof in figure 2 T y(R(y, y)v P(y, y))AVcR(, ) T 3y(R(g, y)v P(y, y)) T VaR(a, r) T(R(co, co)VP(co, co)), new constant co T VarR(a, r) T R(o, co) oR( P(co, co) F R(co, co) T VcR(, a) VarR(, a T R(t2, t2) Figure 2: An example of tableau proof The tableau is not contradictory. So the sentence is not invalid
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. 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 a entry. In class, we have introduced several examples. Fortunately, all tableaux are finite. Consider the following example. Example 1. 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 2. 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 2: An example of tableau proof The tableau is not contradictory. So the sentence is not invalid. 2
Obviously, no contradiction could be introduced in the right branch. For T(Var)R(a, a)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-contrad ath in previous example. With this observation 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 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 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 o Here, we strictly number all newly introduced constant uniformly. With premises S, we could split duction into two stages, odd and even. For example, we can reduce entry in tableau at odd 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 Varp(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 o and a be any formula either with no free variables or with only a free as appropriate Give tableau proofs of each the following (a)(vx)(y(x)Vv(x)+(x)y(x)V(vm)(x) (b)(x)(y→v(x)→(φ→(r)u(x), r not free in (c)(彐x)(y(x)→v(x)→(y(x)→(彐x)v(x)
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. 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. 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. (a) (∀x)(ϕ(x) ∨ ψ(x)) ↔ (∀x)ϕ(x) ∨ (∀x)ψ(x) (b) (∃x)(ϕ → ψ(x)) → (ϕ → (∃x)ψ(x)), x not free in ϕ. (c) (∃x)(ϕ(x) → ψ(x)) → (ϕ(x) → (∃x)ψ(x)). 3
(d)((x)y(x)→v)→(r)(g(x)→v), is not free in y. 2. Let p and a be any formula with free variables a, y and z; let w be any variable not appearing p and v. Give tableau proofs of the following (a)彐rvy(zyVv)分彐 cLyVe(y(x/)Vv) (b)xy(9→Vzv(2))→Vx3yu(y→v(x/u) 3. Let p(a1,., n) be a formula in a languange L with all free variables displayed and let C1,...,Cn be constant symbols not in C Show that V1.Vrnp(a1, .. n)is tableau prov able if and only if P(cl
(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. 4