Discrete Mathematics(II) Spring 2013 Lecture 7: Tableau proof system 1 Overview In last lecture, we have defined consequence, the relationship between a proposition and a set of propositions, on side of semantics. we prove the validity of a proposition semantically, according to truth table. This lecture will consider how to prove the validity of a tautology. But the validity would be guaranteed in the next lecture 2 Atomic tableaux For a given proposition, we can guess it true or false. In order to show our guess, we just associate it with a sign T or F in front of it. A string like Fa and Ta is called signed proposition In preceding lectures, we have known that a compound proposition is constructed by some simpler ones and the truth valuation between them must obey truth table. Because of the Adequacy Theorem, all connective function can be represent by ,A, V. For convenience, there are totall five connectives in proposition logic We first figure out 12 atomic tableaux according to truth table as shown in Figure 1. We just take (a-B)as the example. If a truth valuation V make(a-B)true, we must have either a is false or B is true. Otherwise, we have a true or B false simultaneously. Vividly, we can use a branch to represent“ or"and a chain to represent“both…and With these atomic tableaux, we can expand a given proposition with a sign following this way Definition 1(Tableaux). A finite tableau is a binary tree, labeled with signed propositions called entries. such that 1. All atomic tableaux are finite tableaux 2. If T is a finite tableau, P a path on T,E an entry of T occurring on P and It is obtained from T by adjoining the unique atomic tableau with root entry e to t at the end of the path P, then /T is also a finite tableau If To, T1,..., Tn,... is a(finite or infinite) sequence of the finite tableaux such that, for each n 0, Tn+1 is constructed from Tn by an application of(2), then T= UTn is a tableau Example 1. A tableau with the signed proposition F(((a-B)v(va))A(avB)) In order to characterize a tableaux, we define the following terms Definition 2. Let t be a tableau, P a path on T and e an entry occurring on P
Discrete Mathematics (II) Spring 2013 Lecture 7: Tableau Proof System Lecturer: Yi Li 1 Overview In last lecture, we have defined consequence, the relationship between a proposition and a set of propositions, on side of semantics. we prove the validity of a proposition semantically, according to truth table. This lecture will consider how to prove the validity of a tautology. But the validity would be guaranteed in the next lecture. 2 Atomic tableaux For a given proposition, we can guess it true or false. In order to show our guess, we just associate it with a sign T or F in front of it. A string like F α and T α is called signed proposition. In preceding lectures, we have known that a compound proposition is constructed by some simpler ones and the truth valuation between them must obey truth table. Because of the Adequacy Theorem, all connective function can be represent by {¬, ∧, ∨}. For convenience, there are totally five connectives in proposition logic. We first figure out 12 atomic tableaux according to truth table as shown in Figure 1. We just take (α → β) as the example. If a truth valuation V make (α → β) true, we must have either α is false or β is true. Otherwise, we have α true or β false simultaneously. Vividly, we can use a branch to represent “or” and a chain to represent “both ... and ...”. With these atomic tableaux, we can expand a given proposition with a sign following this way: Definition 1 (Tableaux). A finite tableau is a binary tree, labeled with signed propositions called entries, such that: 1. All atomic tableaux are finite tableaux. 2. If τ is a finite tableau, P a path on τ , E an entry of τ occurring on P and ′τ is obtained from τ by adjoining the unique atomic tableau with root entry E to τ at the end of the path P, then ′τ is also a finite tableau. If τ0, τ1, . . . , τn, . . . is a (finite or infinite) sequence of the finite tableaux such that, for each n ≥ 0, τn+1 is constructed from τn by an application of (2), then τ = ∪τn is a tableau. Example 1. A tableau with the signed proposition F(((α → β) ∨ (γ ∨ δ)) ∧ (α ∨ β)). In order to characterize a tableaux, we define the following terms: Definition 2. Let τ be a tableau, P a path on τ and E an entry occurring on P. 1
F(a∧B) T(a∧B) TA T a F B F(avB T(-a) T(avB) Fa Fa T B F B F(a→B) T(a分B) F T(a→B) Ta Fa t a fa FB TB FBFB Figure 1: Atomic tableaux of propositional logic E has been reduced on P if all the entries on one path through the atomic tableau with root e occur on p 2. P is contradictory if, for some proposition a, Ta and Fa are both entries on P. P is finished if it is contradictory or every entry on P is reduced on P 3. T is finished if every path through T is finished 4. T is contradictory if every path through T is contradictory Based on these terms, we can define what is a proof in a way with tableaux. Actually, we just prove a proposition valid by contradiction, which means we just negate its every contrary side. Definition 3. 1. A tableau proof of a proposition a is a contradictory tableau with root entry a. A proposition is tableau provable, written F a, if it has a tableau proof. 2. A tableau refutation for a proposition a is a contradictory tableau starting ith Ta. A propo sition is tableau refutable if it has a tableau refutation Of course, proof and refutation are dual to each other. Consider the following question, is refutation necessary in our proof system? 3 Complete systematic tableaux As we already know, there are many possible ways to expand the tableaux, which we mean which entry is chosen and be reduced. If the proposition is complicated enough, the parsing tree would
T A F A T (α ∧ β) F α T β F (α ∧ β) T α F β T (¬α) F α F (¬α) T α F (α ∨ β) F α F β T (α ∨ β) T α T β T (α → β) F α T β F (α → β) T α F β T (α ↔ β) T α F α T β F β F (α ↔ β) T α F α F β T β Figure 1: Atomic tableaux of propositional logic 1. E has been reduced on P if all the entries on one path through the atomic tableau with root E occur on P. 2. P is contradictory if, for some proposition α, T α and F α are both entries on P. P is finished if it is contradictory or every entry on P is reduced on P. 3. τ is finished if every path through τ is finished. 4. τ is contradictory if every path through τ is contradictory. Based on these terms, we can define what is a proof in a way with tableaux. Actually, we just prove a proposition valid by contradiction, which means we just negate its every contrary side. Definition 3. 1. A tableau proof of a proposition α is a contradictory tableau with root entry F α. A proposition is tableau provable, written ⊢ α, if it has a tableau proof. 2. A tableau refutation for a proposition α is a contradictory tableau starting with T α. A proposition is tableau refutable if it has a tableau refutation. Of course, proof and refutation are dual to each other. Consider the following question, is refutation necessary in our proof system? 3 Complete systematic tableaux As we already know, there are many possible ways to expand the tableaux, which we mean which entry is chosen and be reduced. If the proposition is complicated enough, the parsing tree would 2
be big and it means there many nodes to handle. The we just run into a problem, how can you guarantee that every entry in generated tableau are all reduced, which means the tableau is really finishe As a tableau is at most a binary-branching tree and also be a partial ordered set. However, if we can make it order we can reduce node by node without omitting. Then we just assure a lexical graphical order, which is defined level by level and left to right on a given tableau. We just call this approach Complete Systematic Tableaux(CST)as the following Definition 4(Complete systematic tableaux. Let r be a signed proposition. We define th complete systematic tableau(Cst)with root entry R by induction 1. Let To be the unique atomic tableau with R at its root 2. Assume that Tm has been defined. Let n be the smallest level of Tm and let e be the leftmost such entry of level n 3. Let Tm+1 be the tableau gotten by adjoining the unique atomic tableau with root e to the end of every noncontradictory path of Tm on which e is unreduced The union of the sequence Tm is our desired complete systematic tableau. This method is tedious for us when the size of a proposition is small. However, it is proper for a program to reduce a given proposition with sign mechanically. CST can guarantee that no unreduced nodes are left for every entry is ordered with a number and CSt just reduce them one by one according to that order. We can check the procedure in detail. The entries are examined level by level and from left to right in the same level. Suppose CSt is processing the entries on level n. The atomic tableau corresponding to the current unreduced entry must be adjoined to the entries on the level no less than n However, there are still some issue should be taken into consideration if we really think algorith- mically. What's the time complexity for a node to be reduced and be adjoined in every noncontra dictory path which pass that node? 4 Properties of CSt There are some good properties of CSt, which will be introduced in the next class Theorem 5. Every CsT is finished Proof. Reduce the E level rel and from left to right until that there is no E unreduced for any fixed level. Every entry has a number. Given an unreduced entry En, say n. If th e current processing entry is m. After finite step, actually n-m steps, it will be reduced Theorem 6. If T= UTn is a contradictory tableau, then for some m, Tm is a finite contradictory tableau. Thus, in particular, if a CsT is a proof, it is a fimite tableau
be big and it means there many nodes to handle. The we just run into a problem, how can you guarantee that every entry in generated tableau are all reduced, which means the tableau is really finished. As a tableau is at most a binary-branching tree and also be a partial ordered set. However, if we can make it order we can reduce node by node without omitting. Then we just assure a lexical graphical order, which is defined level by level and left to right on a given tableau. We just call this approach Complete Systematic Tableaux (CST) as the following. Definition 4 (Complete systematic tableaux). Let R be a signed proposition. We define the complete systematic tableau(CST) with root entry R by induction. 1. Let τ0 be the unique atomic tableau with R at its root. 2. Assume that τm has been defined. Let n be the smallest level of τm and let E be the leftmost such entry of level n. 3. Let τm+1 be the tableau gotten by adjoining the unique atomic tableau with root E to the end of every noncontradictory path of τm on which E is unreduced. The union of the sequence τm is our desired complete systematic tableau. This method is tedious for us when the size of a proposition is small. However, it is proper for a program to reduce a given proposition with sign mechanically. CST can guarantee that no unreduced nodes are left for every entry is ordered with a number and CST just reduce them one by one according to that order. We can check the procedure in detail. The entries are examined level by level and from left to right in the same level. Suppose CST is processing the entries on level n. The atomic tableau corresponding to the current unreduced entry must be adjoined to the entries on the level no less than n. However, there are still some issue should be taken into consideration if we really think algorithmically. What’s the time complexity for a node to be reduced and be adjoined in every noncontradictory path which pass that node? 4 Properties of CST There are some good properties of CST, which will be introduced in the next class. Theorem 5. Every CST is finished. Proof. Reduce the E level by level and from left to right until that there is no E unreduced for any fixed level. Every entry has a number. Given an unreduced entry En, say n. If the current processing entry is m. After finite step, actually n − m steps, it will be reduced. Theorem 6. If τ = ∪τn is a contradictory tableau, then for some m, τm is a finite contradictory tableau. Thus, in particular, if a CST is a proof, it is a finite tableau. 3
Proof. By Konig lemma. Because a contradictory path must be finite and infinite tree with finite branch must has a infinite path. It is contradictory In order to prove the finiteness of every CSt, we first give the following definition Definition 7. We define d(a), the degree of a proposition a by induction 1. if a is a propositional letter, then d(a)=0 2. if a is nB, then d(a)=d(B)+ 3. if a is BV?,B∧γ,orB→T, then d(a)=d(B)+d()+1 The degree of a signed proposition. Ta or Fa is the degree of a. If P is a path in a tableau T, then d(p) the degree of P is the sum of the degree of the signed propositions on P that are not reduced Theorem 8. Every CsT is finite Proof. While path extending, an entry could be split into two branches. whatever, the degree of every path decrease for each reduction. So we have d(Pm+1)< d(Pm) where Pm+1 is an extension of p With this Theorem, we do know something wrong if we run into a tableau which can never be finished Exercises 1. Ex 4/ page 36 2. Ex 6/ page 36 3. Ex 9/ page 36 4. Prove the following tautology by tableau proof (a)(q→r)→(-q→→p)→(p→r) (b)(P∧q)→r)+(p→(q→+r) 5. Prove of refute the following proposition. (If negative, find the counterexample) (a)(a→B)→(a→7)→(a→(3→) (b)(a→B)→(6→1)→(a→)
Proof. By K¨onig lemma. Because a contradictory path must be finite and infinite tree with finite branch must has a infinite path. It is contradictory. In order to prove the finiteness of every CST, we first give the following definition. Definition 7. We define d(α), the degree of a proposition α by induction. 1. if α is a propositional letter, then d(α) = 0. 2. if α is ¬β, then d(α) = d(β) + 1. 3. if α is β ∨ γ, β ∧ γ, or β → γ, then d(α) = d(β) + d(γ) + 1. The degree of a signed proposition T α or F α is the degree of α. If P is a path in a tableau τ , then d(P) the degree of P is the sum of the degree of the signed propositions on P that are not reduced on P. Theorem 8. Every CST is finite. Proof. While path extending, an entry could be split into two branches. whatever, the degree of every path decrease for each reduction. So we have d(Pm+1) < d(Pm) where Pm+1 is an extension of Pm. With this Theorem, we do know something wrong if we run into a tableau which can never be finished. Exercises 1. Ex 4/ page 36 2. Ex 6/ page 36 3. Ex 9/ page 36 4. Prove the following tautology by tableau proof (a) (q → r) → ((¬q → ¬p) → (p → r)) (b) ((p ∧ q) → r) ↔ (p → (q → r)) 5. Prove of refute the following proposition.(If negative, find the counterexample) (a) ((α → β) → (α → γ)) → (α → (β → γ)) (b) (α → β) → ((β → γ) → (α → γ)) 4