Discrete Mathematics(Il) Spring 2012 Lecture 7: Tableau Proof System Lecturer. YiL 1 Overview In this lecture, we consider how to make proof. In previous lectures, we prove a proposition valid semantically, say according to truth table. But today we focus on proof in syntax 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 f or t in There are five connectives. We first give 12 atomic tableaux according to truth table of each (a∧B) T(a∧B) TA F FB F(avB) F(a) F F FB F(→B)T(a+)F(aB T O a F F T B FB TB FBFB T B With these atomic tableaux, we can expand a given proposition with a sign following this way entries, such that
Discrete Mathematics (II) Spring 2012 Lecture 7: Tableau Proof System Lecturer: Yi Li 1 Overview In this lecture, we consider how to make proof. In previous lectures, we prove a proposition valid semantically, say according to truth table. But today we focus on proof in syntax. 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 F or T in front of it. There are five connectives. We first give 12 atomic tableaux according to truth table of each connectives. 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 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
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 ir is obtained from t by adjoining the unique atomic tableau with root entry e to r 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 2 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(vo))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 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 a, Ta and Fa are both entries on P. P is finished if it is contradictory or every entry on P is reduced 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 Fa. A proposition is tableau provable, written H a, if it has a tableau proof. 2. A tableau refutation for a proposition a is a contradictory tableau starting with Ta. A propo- sition is tableau refutable if it has a tableau refutation roof and refutation are dual to each other. Consider the following question, is refutation neces S our proof system? 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 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
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. 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 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. 2
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 to be the unique atomic tableau urith 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. 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 finishe Proof. Reduce the E level by level and there is no E unreduced for any fixed level 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 finite tableau Proof. By K 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 -B, then d(a)=d(B)+1 3. if a is BV%,B∧y,orB→,tend(a)=d(6)+d()+1. The degree of a signed propostion 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 proposti p that are not reduced Theorem 8. Every CST is finite
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. 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 there is no E unreduced for any fixed level. 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. Proof. By K¨onig lemma. 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 propostion 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 propostions on P that are not reduced on P. Theorem 8. Every CST is finite. 3
Proof. Every path is finite with d(Pm+1)<d(pm) With this Theorem we do know something wrong if we run into a tableau which can never b Exercises 1. Ex 4/ page 2. Ex 6/ page 36 4. Prove the following tautology by tableau proof (a)(q→r)→(-q→-p)→(P→r) (b)(∧q)→r)+(p→(q→r) 5. Prove of refute the following proposition. (If negative, find the counterexample (a)(a→B→(a→)→(a→(→7) (b)(a→B)→(8→1)→(a→7)
Proof. Every path is finite with d(Pm+1) < d(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