Discrete Mathematics(ID) Spring 2012 Lecture 9: Deduction from Premises, Compactness, and Applications Lecturer. yil 1 Overview In lecture 7, we introduce a tableau proof system to prove the validity of a proposition. But we should handle whether a is a logic consequence of or not. Here, 2 is called a set of premises Mathematical Logic is a corner stone of modern computer science. In this lecture, we also show you how to apply propositional logic to other problems 2 Deduction from premises luse a set of premises is introduced, we should define a new type of tableau proof system to le the premises If a is a consequence of 2, then any v satisfing 2 should also make a true. The problem can be simplified by considering the case when ai E 2. Then, we can introduce a proposition ai into tableau in the form of ta Definition 1(Tableaux from premises). Let 2 be(possibly infinite) set of propositions. We define the finite tableaux with premises from 2 by induction 1. Every atomic tableau is a finite tableau from 2 2. If r is a finite tableau from 2 and a E 2, then the tableau formed by putting Ta at the end of every noncontradictory path not containing it is also a finite tableau from 2 3. If T is a finite tableau from 2,P a path in 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 the end of the ath P, then /T is also a finite tableau from 2 厅0,,rn,…,isa( finite or infinite) sequence of finite tableaux from∑ such that, for each n≥ 0, Tn+1 is constructed from Tn by an application of (2) and (3), then T=UTn is a tableau from 2 Similarly, we can redefine tableau proof as following Definition 2. A tableau proof of a proposition a from 2 is a tableau from 2 with root entry Fa that is contradictory, that is, one in which every path is contradictory. If there is such a proof we say that a is provable from∑ and write it as∑a To CST, we have the following property
Discrete Mathematics (II) Spring 2012 Lecture 9: Deduction from Premises,Compactness, and Applications Lecturer: Yi Li 1 Overview In lecture 7, we introduce a tableau proof system to prove the validity of a proposition. But we should handle whether α is a logic consequence of Σ or not. Here, Σ is called a set of premises. Mathematical Logic is a corner stone of modern computer science. In this lecture, we also show you how to apply propositional logic to other problems. 2 Deduction from Premises Because a set of premises is introduced, we should define a new type of tableau proof system to handle the premises. If α is a consequence of Σ, then any V satisfing Σ should also make α true. The problem can be simplified by considering the case when αi ∈ Σ. Then, we can introduce a proposition αi into tableau in the form of T αi . Definition 1 (Tableaux from premises). Let Σ be (possibly infinite) set of propositions. We define the finite tableaux with premises from Σ by induction: 1. Every atomic tableau is a finite tableau from Σ 2. If τ is a finite tableau from Σ and α ∈ Σ, then the tableau formed by putting T α at the end of every noncontradictory path not containing it is also a finite tableau from Σ. 3. If τ is a finite tableau from Σ, P a path in τ , E an entry of τ occurring on P and 0τ is obtained from τ by adjoining the unique atomic tableau with root entry E to the end of the path P, then 0τ is also a finite tableau from Σ. If τ0, . . . , τn, . . . is a (finite or infinite) sequence of finite tableaux from Σ such that, for each n ≥ 0, τn+1 is constructed from τn by an application of (2) and (3), then τ = ∪τn is a tableau from Σ. Similarly, we can redefine tableau proof as following: Definition 2. A tableau proof of a proposition α from Σ is a tableau from Σ with root entry F α that is contradictory, that is, one in which every path is contradictory. If there is such a proof we say that α is provable from Σ and write it as Σ ` α. To CST, we have the following property. 1
Theorem 3. Every CST from a set of premises is finished Unlike the CST in previous lecture, we can not guarantee the tableau to be finite. Because 2 could be a infinite set. It means we can introduce premises as many as possible into our tableau Anyway, every entry in CST would be finally reduced. We can give several ways to expand CSt in detail. Even if the proposition is an infinite sequence, we can also obtain the same property 3 Soundness theorem We first give the following lemma Lemma 4. If a valuation v makes every aE 2 true and agrees with the root of a tableau t from 2, then there is a path in T every entry of which agrees with v It sets up a connection between truth valuation v and sign of entries along noncontradictory path When giving proof, we need handle propositions introduced from 2 whose corresponding entry is always with sign T By this lemma, we can easily prove the following soundness theorem Theorem 5( Soundness). If there is a tableau proof of a from a set of premises 2, then a is a consequence of∑,te.∑卜a→∑Fa Soundness theorem means that a propositon must be a logic consequence of 2 if it can be deduced 4 Completeness Theorem Similarly, we have the following Lemma Lemma 6. Let P be a noncontradictory path in a finished tableau T from 2. Define a valuation v as the last section, then it agrees with all entries on P and so in particular makes every proposition B∈∑ true. It is nearly the same as previous proof for completeness theorem without premises except that propositions from 2 should be handled specially With this lemma, we have completeness theorem Theorem 7(Completeness). If a is consequence of a set 2 of premises, then there is a tableau uction of a from∑,i.e,∑Fa→∑a. Completeness theorem says that if a propostion is a consequence of a set of propositions, it can be deduced from this set
Theorem 3. Every CST from a set of premises is finished. Unlike the CST in previous lecture, we can not guarantee the tableau to be finite. Because Σ could be a inifinite set. It means we can introduce premises as many as possible into our tableau. Anyway, every entry in CST would be finally reduced. We can give several ways to expand CST in detail. Even if the proposition is an infinite sequence, we can also obtain the same property. 3 Soundness Theorem We first give the following lemma. Lemma 4. If a valuation V makes every α ∈ Σ true and agrees with the root of a tableau τ from Σ, then there is a path in τ every entry of which agrees with V. It sets up a connection between truth valuation V and sign of entries along noncontradictory path. When giving proof, we need handle propositions introduced from Σ whose corresponding entry is always with sign T. By this lemma, we can easily prove the following soundness theorem. Theorem 5 (Soundness). If there is a tableau proof of α from a set of premises Σ, then α is a consequence of Σ, i.e. Σ ` α ⇒ Σ α. Soundness theorem means that a propositon must be a logic consequence of Σ if it can be deduced from Σ. 4 Completeness Theorem Similarly, we have the following Lemma. Lemma 6. Let P be a noncontradictory path in a finished tableau τ from Σ. Define a valuation V as the last section, then it agrees with all entries on P and so in particular makes every proposition β ∈ Σ true. It is nearly the same as previous proof for completeness theorem without premises except that propositions from Σ should be handled specially. With this lemma, we have completeness theorem. Theorem 7 (Completeness). If α is consequence of a set Σ of premises, then there is a tableau deduction of α from Σ, i.e., Σ α ⇒ Σ ` α. Completeness theorem says that if a propostion is a consequence of a set of propositions, it can be deduced from this set. 2
5 Compactness Theorem Theorem 8(finite proof). If T= UTn is a contradictory tableau from X, then for some m, Tm is a finite contradictory tableau from 2. In particular, if a Cst from 2 is a proof, it is finite It means a tableau proof is a finite sequence of trees. Otherwise we can imply contradiction that the tableau is not a tabeau proof With finite proof theorem, we have a type of compactness theorem by using completeness and soundness theore Theorem 9. a is a consequence of 2 if and only if a is a consequence of some finite subset of 2 Sketch. We apply completeness theorem first and get 2Ha. For any tableau proof must be finite, we can collect all proposition introduced from 2 and form a finite set 2o. The tableau also shows Eo Ha. We then apply soundness theorem and obtain Zo a. It is proved now However, compactness theorem can be directly proved. We have the following version Theorem 10( Compactness). Let 2= aili e w be an infinite set of a propositions. E is satisfiable if and only if every finite subset r of 2 is satisfiable Generally, if V1 and v2 satisfy >l and 22 respectively, it does not mean the union of two truth valuation would satisfy all propositions in two sets Sketch. Consider the tableau with root F(=a∧a) We already know that (a A a) is always false, which means that any truth valuation V always agrees with the root entry. If it is a finite tableau, every path of tableau is contradictory. It means that all propositions in 2 along a contradictory path is unsatisfiable. It is contradictory to every finite subset is satisfiable. So there is a infinite path in the tableau This compactness theorem transform a problem with infinite propositions to a infinite sequence of finite propositions 6 Circuit and Proposition Let's take 0, 1 as F, T respectively. We can use circuit gate to represent A, V and as and, or, not respectively. So given any proposition, we can design a circuit to compute the truth value with the specific inpu Example 1. Consider the circuit for the following propositions The circuit will be drawn in the future
5 Compactness Theorem Theorem 8 (finite proof). If τ = ∪τn is a contradictory tableau from Σ, then for some m, τm is a finite contradictory tableau from Σ. In particular, if a CST from Σ is a proof, it is finite. It means a tableau proof is a finite sequence of trees.Otherwise we can imply contradiction that the tableau is not a tabeau proof. With finite proof theorem, we have a type of compactness theorem by using completeness and soundness theorem. Theorem 9. α is a consequence of Σ if and only if α is a consequence of some finite subset of Σ. Sketch. We apply completeness theorem first and get Σ ` α. For any tableau proof must be finite, we can collect all proposition introduced from Σ and form a finite set Σ0. The tableau also shows Σ0 ` α. We then apply soundness theorem and obtain Σ0 |= α. It is proved now. However, compactness theorem can be directly proved. We have the following version. Theorem 10 (Compactness). Let Σ = {αi |i ∈ ω} be an infinite set of a propositions. Σ is satisfiable if and only if every finite subset Γ of Σ is satisfiable. Generally, if V1 and V2 satisfy Σ1 and Σ2 respectively, it does not mean the union of two truth valuation would satisfy all propositions in two sets. Sketch. Consider the tableau with root F(¬α ∧ α). We already know that (¬α ∧ α) is always false, which means that any truth valuation V always agrees with the root entry. If it is a finite tableau, every path of tableau is contradictory. It means that all propositions in Σ along a contradictory path is unsatisfiable. It is contradictory to every finite subset is satisfiable. So there is a infinite path in the tableau. This compactness theorem transform a problem with infinite propositions to a infinite sequence of finite propositions. 6 Circuit and Proposition Let’s take 0, 1 as F, T respectively. We can use circuit gate to represent ∧, ∨ and ¬ as and,or,not respectively. So given any proposition, we can design a circuit to compute the truth value with the specific input. Example 1. Consider the circuit1 for the following propositions: 1The circuit will be drawn in the future. 3
1.(41∧A2)V(-A3) 2.( AABAD)V(A∧BA=C) The complexity of circuits depends on the complexity of proposition. We usually call the depth of proposition as delay of circuit and the number of gates as power consumption. To design a good circuit, we try to minimize delay and power consumption Example 2. Consider the boolean function majority of (A, B, C]. It means that the value of function depends on the majority of input Solution: We first consider its truth value table, we can simple connectives to represent majority m(A, B, C)=(AABAC)V(AABANC)V(AA-BAC)VGAABAC) (B∧C)V(A∧C)V(A∧B) (A∧(BVO)∨(BAC) In another way, we can depict the boolean function with a state diagram and then design the circuit accroding it. This method will be introduced in the successor course Digital Component Desing 7 Formalize Problems with Propositions Example 3. Suppose there is a murder case with three suspects. The police queried them about murder case A said, "I didn 't do it. The victim is a friend of B. And C hates him. B said, "I didn't do it. Even I don't know him. And I am not present. C said, I didn't do it. I saw A and B stayed writh the victim in that day. The murder must be one of them. Solution: Suppose only murder would lie. We try to formalize it with the following propositions A: a killed victim 2. BKV: B knows the victim 3. AP: A is present 4. CHV: C hates the victim 5.(A∧=B)V(A∧B): murder is either a or B Now we can represent the satement of each sucpects as following 1.A:-A∧BKV∧CHV 2. B: BABKVA-BP 3. C: CA APABPA((AAB)V(AAB)
1. (A1 ∧ A2) ∨ (¬A3)) 2. (A ∧ B ∧ D) ∨ (A ∧ B ∧ ¬C) The complexity of circuits depends on the complexity of proposition. We usually call the depth of proposition as delay of circuit and the number of gates as power consumption. To design a good circuit, we try to minimize delay and power consumption. Example 2. Consider the boolean function majority of {A, B, C}. It means that the value of function depends on the majority of input. Solution: We first consider its truth value table, we can simple connectives to represent majority. m(A, B, C) = (A ∧ B ∧ C) ∨ (A ∧ B ∧ ¬C) ∨ (A ∧ ¬B ∧ C) ∨ (¬A ∧ B ∧ C) = (B ∧ C) ∨ (A ∧ C) ∨ (A ∧ B) = (A ∧ (B ∨ C)) ∨ (B ∧ C) In another way, we can depict the boolean function with a state diagram and then design the circuit accroding it. This method will be introduced in the successor course Digital Component Desing. 7 Formalize Problems with Propositions Example 3. Suppose there is a murder case with three suspects. The police queried them about murder case. A said,”I didn’t do it. The victim is a friend of B. And C hates him.” B said, ”I didn’t do it. Even I don’t know him. And I am not present.” C said, ”I didn’t do it. I saw A and B stayed with the victim in that day. The murder must be one of them.” Solution: Suppose only murder would lie. We try to formalize it with the following propositions: 1. A: A killed victim. 2. BKV : B knows the victim. 3. AP: A is present. 4. CHV : C hates the victim. 5. (A ∧ ¬B) ∨ (¬A ∧ B): murder is either A or B. Now we can represent the satement of each sucpects as following: 1. A: ¬A ∧ BKV ∧ CHV . 2. B: ¬B ∧ ¬BKV ∧ ¬BP. 3. C: ¬C ∧ AP ∧ BP ∧ ((A ∧ ¬B) ∨ (¬A ∧ B)). 4
It is easy to know that the maximal satisfiable set of propositions can only contain As and Cs statement. Then we can imply that B would be the murder Example 4. Consider the pigeonhole principle: f: n+,n, 3i, j, f()=f(, where where Vo CV is a finite set and Eo C E is the set determined by t Proof. Let Pa i represent vertex a is colored with i. We can formulate a graph which is k-colorable with the following propositions 1. Pa 1 VPa.2V..VPa.k, for every a E v. It means every vertex could be colored with at least one of k colors 2.-(Pa∧pa),1≤i<j≤ k for all ae v. It means CinC=0
It is easy to know that the maximal satisfiable set of propositions can only contain A’s and C’s statement. Then we can imply that B would be the murder. Example 4. Consider the pigeonhole principle: f : n + → n, ∃i, j, f(i) = f(j), where 0 ≤ i , where V is the set of vertices and E ⊆ V 2 is the set of all edges. If (a, b) ∈ E, it is denoted as aEb sometimes. G is k-colorable if V can be decomposed into k-color classes V = C1 ∪ C2 ∪ · · · ∪ Ck, where Ci 6= ∅ and Ci ∩ Cj = ∅ if i 6= j. It is obvious (a, b) 6∈ E if a, b ∈ Ci . A finite subgraph is k-colorable. It means there is a k-colorable graph G0 = , where V0 ⊂ V is a finite set and E0 ⊂ E is the set determined by V0. Proof. Let pa,i represent vertex a is colored with i. We can formulate a graph which is k-colorable with the following propositions. 1. pa,1 ∨ pa,2 ∨ · · · ∨ pa,k, for every a ∈ V . It means every vertex could be colored with at least one of k colors. 2. ¬(pa,i ∧ pa,j ), 1 ≤ i < j ≤ k for all a ∈ V . It means Ci ∩ Cj = ∅. 5
3. (Pa, i A pb, i), i=l,., k for all aEb. It means no neighbors have the same color Then we get a set X with infinite propositions. For any finite subset Xo cx, we can extract vertices Vo from it and construct a set X1 which describe the graph Go generated by Vo. For every finite subgraph is k-colorable, X1 is satisfiable. Xo must be satisfiable According to compactness theorem, X is satisfiable which means the graph is k-colorable Remark: Generally, this theorem is not easy to prove via graph approach. Because there effective way to find it possible that a big graph is still k-colorable merged by two k-colorable gra However, Compactness Theorem does not need this requirement. Here, we should be aware that set of constructed and we try to prove that every finite subset of it is satisfiable which is the essence of Compactness Theorem Example 6. Every set S can be(totally ) ordered Similarly, it can be proved like k-colorable infinite graph. The point is to represent our problem with a set of propositions. This is left as an exercise. Hints: A set is partial order at least. If you can change a partially ordered set into a linear order set, you successfully complete the proof 9 Konig Lemma and Compactness Theorem In our textbook, Compactness Theorem is proved by Konig lemma. Now we will show you that it can be proved by Compactness Theorem Lemma 11(Konig). A infinite tree with finite branch has a infinite path Actually, the problem can be represented as following. If every a E T has only finitely many immediate successor and T contains arbitrarily long finite paths, then there is a infinite path in T starts at root Proof. Tree is a hierarchical structure. It means that the vertices of a tree could be divided into many sets which corresponds to vertices in some level. So we can define So the root) and Sk=tb TI there is aa E Sk and b is a immediate successor of a. For every k, Sk is finite and no Sk is empty because of infinity of given tree Denote Pa as that vertex a is in path P. We now represent a tree with a set of propositions, following 1. Vask Pa: there is at least one vertex of level k in a path 2. Va bes, -(pa A pb: there is only one vertex of level k in path 3. Pa, Pb: b is a immediate successor of a
3. ¬(pa,i ∧ pb,i), i = 1, . . . , k for all aEb. It means no neighbors have the same color . Then we get a set X with infinite propositions. For any finite subset X0 ⊂ X, we can extract vertices V0 from it and construct a set X1 which describe the graph G0 generated by V0. For every finite subgraph is k-colorable, X1 is satisfiable. X0 must be satisfiable. According to compactness theorem, X is satisfiable which means the graph is k-colorable. Remark: Generally, this theorem is not easy to prove via graph approach. Because there is no effective way to find it possible that a big graph is still k-colorable merged by two k-colorable graph. However, Compactness Theorem does not need this requirement. Here, we should be aware that a set of propositions is constructed and we try to prove that every finite subset of it is satisfiable, which is the essence of Compactness Theorem. Example 6. Every set S can be (totally) ordered. Similarly, it can be proved like k-colorable infinite graph. The point is to represent our problem with a set of propositions. This is left as an exercise. Hints: A set is partial order at least. If you can change a partially ordered set into a linear order set, you successfully complete the proof. 9 K¨onig Lemma and Compactness Theorem In our textbook, Compactness Theorem is proved by K¨onig lemma. Now we will show you that it can be proved by Compactness Theorem. Lemma 11 (K¨onig). A infinite tree with finite branch has a infinite path. Actually, the problem can be represented as following. If every a ∈ T has only finitely many immediate successor and T contains arbitrarily long finite paths, then there is a infinite path in T starts at root. Proof. Tree is a hierarchical structure. It means that the vertices of a tree could be divided into many sets which corresponds to vertices in some level. So we can define S0 = {c|c is the root} and Sk = {b ∈ T| there is a a ∈ Sk and b is a immediate successor of a}. For every k, Sk is finite and no Sk is empty because of infinity of given tree. Denote pa as that vertex a is in path P. We now represent a tree with a set of propositions, Σ, as following: 1. ∨a∈Sk pa: there is at least one vertex of level k in a path; 2. ∨a,b∈Sk¬(pa ∧ pb): there is only one vertex of level k in path p. 3. pa → pb: b is a immediate successor of a. 6
For there are infinite vertices, we have infinite propositions. If they are all satisfiable. We do know there is a infinite path. Given a subset 2o, it is just a part of subtree with height k. Then we just add missed propositions into 2o and obtain the subtree represented by 2o. As the tree has arbitrarily long finite paths. We know 2o is satisfiable and also 2o. Now we just apply compactness theorem to get final result In textbook, compactness theorem of proposition logic is proved based on Konig lemma. Here we prove inversely Exercises 1. Let 2 be finite set of propositions and Ae the conjunction of its members. Prove that for any proposition a the following are equivalent (a)∑F (b)}A→a d)hA∑→a. 2. Suppose X is a finite set of propositions Show that every CST from 2 is finite. 3. Prove AV-B, BV-C,CV-DJF(D+A) 4. Suppose proposition could be infinite long. Define a new method to construct a CSt and prove that every CST is finished 5. Design a circuit for multiply with twotwo bits input and four bits output. For example, we have 1*1=1,10*11=110
For there are infinite vertices, we have infinite propositions. If they are all satisfiable. We do know there is a infinite path. Given a subset Σ0, it is just a part of subtree with height k. Then we just add missed propositions into Σ0 and obtain the subtree represented by Σ0 0 . As the tree has arbitrarily long finite paths. We know Σ0 0 is satisfiable and also Σ0. Now we just apply compactness theorem to get final result. In textbook, compactness theorem of proposition logic is proved based on K¨onig lemma. Here we prove inversely. Exercises 1. Let Σ be finite set of propositions and ∧Σ the conjunction of its members. Prove that for any proposition α the following are equivalent: (a) Σ |= α. (b) |= ∧Σ → α. (c) Σ ` α (d) ` ∧Σ → α. 2. Suppose Σ is a finite set of propositions. Show that every CST from Σ is finite. 3. Prove {A ∨ ¬B, B ∨ ¬C, C ∨ ¬D} |= (D → A). 4. Suppose proposition could be infinite long. Define a new method to construct a CST and prove that every CST is finished. 5. Design a circuit for multiply with two two bits input and four bits output. For example, we have 1 ∗ 1 = 1, 10 ∗ 11 = 110. 7
