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<i<j< Solution: let Pi; means f()=j. Then we can describe everywhere defined property as ∧0 and we can describe single value as a1=A0≤i≤nA0≤j≠k<n-(PApk) Now we can describe pigeonhole principle as =(a1Aa2)∧(o≤<j≤nVo≤k<n(Pi∧Pk) Remark: This form of pigeonhole is much harder to recognize than its original version. However it is described by a much more rigid language compared with our natural languag result in ambiguities In fact, mathematical logic can be applied into program verification, model checking, and such other applications. European Space Agency only uses software which has gotten through program verification 8 Application of Compactness Theorem Compactness theorem is a very important result in mathematical logic. It establishes a connection between infinity and finitude Example 5. Given an infinite planar graph. If its every finite subgraph is R-colorable, then the graph itself is also k-colorable a graph is G=< V,E here v is the set of vertices and e c v2 is the set of all edges. If (a, b)EE, it is denoted as aEb sometimes. G is k-colorable if V can be decomposed into k-color classes V =C1U C2 U.U Ck, where Ci f0 and CinC=0 if i +3. It is obvious(a, b)EE if a,b∈C A finite subgraph is k-colorable. It means there is a k-colorable graph Go = Vo, Eo > 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 < j ≤ n. Solution: let pij means f(i) = j. Then we can describe everywhere defined property as α1 = ∧0≤i≤n ∨0≤j<n pij and we can describe single value as α1 = ∧0≤i≤n ∧0≤j6=k<n ¬(pij ∧ pik) Now we can describe pigeonhole principle as ϕ = (α1 ∧ α2) ∧ (∨0≤i<j≤n ∨0≤k<n (pik ∧ pj,k)) Remark: This form of pigeonhole is much harder to recognize than its original version. However, it is described by a much more rigid language compared with our natural language, which could result in ambiguities. In fact, mathematical logic can be applied into program verification, model checking, and such other applications. European Space Agency only uses software which has gotten through program verification. 8 Application of Compactness Theorem Compactness theorem is a very important result in mathematical logic. It establishes a connection between infinity and finitude. Example 5. Given an infinite planar graph. If its every finite subgraph is k-colorable, then the graph itself is also k-colorable. A graph is G =< V, E >, 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 =< V0, E0 > , 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