Discrete Mathematics(II) Spring 2013 Lecture 8: Soundness and Completeness of Propositional logic Lecturer. Yi l 1 Overview Syntax and semantics are two parts of mathematics logic. Soundness and completeness theorem bridge this two components. Soundness guarantees that our proof always yields valid proposition Completeness makes sure that there is definitely a proof to prove the validity of a valid proposition 2 Syntax and semantics We first consider some example in linguistic. Especially, the word of a language with very long history may has several meanings. Consider the following example, which is Example1. Give you two Chinese characters“更衣”,that' s it mean? It means change clothes in modern Chinese It means go to washroom in ancient Chines If we consider acronyms in science documents, we can find many examples like the following Example 2. Give an acronym "IP", what's it mean? Internet protocol in network Integer Programming in operation research Interactive Proof in complecity These two examples just shows that the same symbols represent different meaning, which would be known in the context We can also find examples in our experiences. Consider different programming languages Example 3. Give you the following programming segments 1. in C, printf("Hello World!") 2. in Java, system. print("Hello World!"); 3. in C++, cout<< Hello World! just output Hello World! on the screen
Discrete Mathematics (II) Spring 2013 Lecture 8: Soundness and Completeness of Propositional Logic Lecturer: Yi Li 1 Overview Syntax and semantics are two parts of mathematics logic. Soundness and completeness theorem bridge this two components. Soundness guarantees that our proof always yields valid proposition. Completeness makes sure that there is definitely a proof to prove the validity of a valid proposition. 2 Syntax and Semantics We first consider some example in linguistic. Especially, the word of a language with very long history may has several meanings. Consider the following example, which is Example 1. Give you two Chinese characters “更衣”, what’s it mean? • It means change clothes in modern Chinese. • It means go to washroom in ancient Chines. If we consider acronyms in science documents, we can find many examples like the following: Example 2. Give an acronym ”IP”, what’s it mean? • Internet Protocol in network. • Integer Programming in operation research. • Interactive Proof in complexity. These two examples just shows that the same symbols represent different meaning, which would be known in the context. We can also find examples in our experiences. Consider different programming languages. Example 3. Give you the following programming segments: 1. in C, printf(”Hello World!”); 2. in Java, system.print(”Hello World!”); 3. in C++, cout<<”Hello World!”; All of them just output ”Hello World!” on the screen. 1
In this example, different symbol sequences just try to complete one mission: print"Hello, World Briefly, syntax is a sequence of symbols, what you see; and semantics is the meaning behind the symbols, what you understand 3 Soundness theorem Example4. Given a proposition a=(A→B)→(A→C)→(B→C), there is a truth valuation which make it false. Consider the tableau with the root as F a Following the non-contradictory path of tableau with root F a, we observe that if truth value of a with truth valuation v is the same as sign of root, it also holds for each entry along that on-contradictory path In preceding example, we have observed that there is a mapping between a truth valuation and the sign of proposition of each entry along the non-contradictory paths. Generally, we have the following lemma. Lemma 1. Ifv is a valuation that agrees with the root entry of a given tableau T given as UTn then t has a path P every entry of which agrees with v Sketch. While the tableau is being extending, the non-contradictory path is also extended after entry is reduced. Then we can apply induction principle to the non-contradictory path. Let Pn the non-contradictory path. Then Pn+1 is the new non-contradictory path after the reduction of a By this lemma, we can easily prove the following soundness theorem Theorem 2 (Soundness). If a is tableau provable, then a is valid, i. e. H a=a Soundness theorem means that a proposition must be valid if it has a tableau proof 4 Completeness Theorem Tableaux proof system contains both syntax and semantics Example 5. Given a proposition(a+(B+2)), consider its tableau proof. We all know(a-(B-m)is never a valid proposition. Along the only one path, we can construct a assignment, where A()=F, A(B)=T, A(a)=T. a truth valuation V extended by A make it Generally, we have the following Lemma Lemma 3. Let P be a noncontradictory path of a finished tableau T. Define a truth assignment A on all propositional letters A as follows
In this example, different symbol sequences just try to complete one mission: print ”Hello, World!” on the screen. Briefly, syntax is a sequence of symbols, what you see; and semantics is the meaning behind the symbols, what you understand. 3 Soundness Theorem Example 4. Given a proposition α = ((A → B) → (A → C)) → (B → C), there is a truth valuation which make it false. Consider the tableau with the root as F α Following the non-contradictory path of tableau with root F α, we observe that if truth value of α with truth valuation V is the same as sign of root, it also holds for each entry along that non-contradictory path. In preceding example, we have observed that there is a mapping between a truth valuation and the sign of proposition of each entry along the non-contradictory paths. Generally, we have the following lemma. Lemma 1. If V is a valuation that agrees with the root entry of a given tableau τ given as ∪τn, then τ has a path P every entry of which agrees with V . Sketch. While the tableau is being extending, the non-contradictory path is also extended after a entry is reduced. Then we can apply induction principle to the non-contradictory path. Let Pn the non-contradictory path. Then Pn+1 is the new non-contradictory path after the reduction of a node. By this lemma, we can easily prove the following soundness theorem. Theorem 2 (Soundness). If α is tableau provable, then α is valid, i.e. ⊢ α ⇒⊨ α. Soundness theorem means that a proposition must be valid if it has a tableau proof. 4 Completeness Theorem Tableaux proof system contains both syntax and semantics. Example 5. Given a proposition (α → (β → γ)), consider its tableau proof. We all know (α → (β → γ)) is never a valid proposition. Along the only one path, we can construct a assignment, where A(γ) = F, A(β) = T, A(α) = T. A truth valuation V extended by A make it false. Generally, we have the following Lemma. Lemma 3. Let P be a noncontradictory path of a finished tableau τ . Define a truth assignment A on all propositional letters A as follows: 2
1.A(A)=T if TA is an entry on P 2. A(A)=F otherwise If v is the unique valuation extending the truth assignment A, then v agrees with all entries of P Sketch. We have known that a truth assignment can uniquely determine a truth valuation. Along a noncontradictory path, we can first construct a truth assignment with the method stated in lemma When the tableau is being extended, a complicated proposition would be decomposed into one/two relatively simpler proposition(s). Then we just reverse the course. The induction is on depth of a In this lemma, we should pay attention to the method to construct a truth assignment. All members of the support of a proposition occur on the leaf node of its formation tree. But some would not ccur on a noncontradictory path of a tableau. We only assign a proposition letter with sign T to true on that path. All others are assigned to false if it has a sign with f and does not occurs. This is called the minimal positive information principle With this lemma, we have completeness theorem Theorem 4(Completeness). If a is valid, then a is tableau provable, i.e. F a=H a. In fact, any finished tableau with root entry Fa is a proof of a and so, in particular, the complete systematic tableaux with root Fo is such a proof. Completeness theorem says that if a proposition is valid, we can find it a tableaux proof During the proof, we show a way to construct a model such that v(a)= f if the tableau is not contradictory 5 Hilbert Proof System We introduce Hilbert proof system, also known as axiom proof system, as a reference to tableaux proof system We first give all the axioms. There are only three Definition 5. The axioms of Hilbert system are all propositions of the following forms 1.(a→(B→a) 2.(a→(6→)→(a→3)→(a→) Actually, you can define different axioms. But we hope there are as few as possible. Just think about adequacy of connectives We also need the famous Modus Ponens principle, which is the only inference rule applying to propositions
1. A(A) = T if T A is an entry on P. 2. A(A) = F otherwise. If V is the unique valuation extending the truth assignment A, then V agrees with all entries of P. Sketch. We have known that a truth assignment can uniquely determine a truth valuation. Along a noncontradictory path, we can first construct a truth assignment with the method stated in lemma. When the tableau is being extended, a complicated proposition would be decomposed into one/two relatively simpler proposition(s). Then we just reverse the course. The induction is on depth of a proposition. In this lemma, we should pay attention to the method to construct a truth assignment. All members of the support of a proposition occur on the leaf node of its formation tree. But some would not occur on a noncontradictory path of a tableau. We only assign a proposition letter with sign T to true on that path. All others are assigned to false if it has a sign with F and does not occurs. This is called the minimal positive information principle. With this lemma, we have completeness theorem. Theorem 4 (Completeness). If α is valid, then α is tableau provable, i.e. ⊨ α ⇒⊢ α. In fact, any finished tableau with root entry F α is a proof of α and so, in particular, the complete systematic tableaux with root F α is such a proof. Completeness theorem says that if a proposition is valid, we can find it a tableaux proof. During the proof, we show a way to construct a model such that V(α) = F if the tableau is not contradictory. 5 Hilbert Proof System We introduce Hilbert proof system, also known as axiom proof system, as a reference to tableaux proof system. We first give all the axioms. There are only three. Definition 5. The axioms of Hilbert system are all propositions of the following forms: 1. (α → (β → α)) 2. ((α → (β → γ)) → ((α → β) → (α → γ))) 3. (¬β → ¬α) → ((¬β → α) → β) Actually, you can define different axioms. But we hope there are as few as possible. Just think about adequacy of connectives. We also need the famous Modus Ponens principle, which is the only inference rule applying to propositions. 3
Definition 6(Modus Ponens). From a and a-,B, we can infer B. This rule is written as follows a→ aββ Now we can define Hilbert proof system Definition 7. Let 2 be a set of propositions 1. A proof from 2 is a finite sequence a1, a2, .. an such that for each i n either (a)a; is a member of∑ (b)ai is an ariom (c)ai can be inferred from some of previous a, by an application of a rule of inference 2. a is provable from∑,∑hra, if there is a proof a1,a2,…,, an from∑ where an=a A proof of a is simply a proof from the empty set 0; a is provable if it is provable from 0 Example 6. Prove the following statements 1.(a→B)→(a→a) 2.{a}hH(-→a)→B) The first can also be proved by tableau proof system. The way to prove the second would not be introduced until the next class. However, you can experience the difference between these two of systems Exercises 1. If a is tableau refutable, then a is unsatisfiable 2. If a is unsatisfiable, then there is a tableau refutation of a 3. Prove that all axioms are valid in Hilbert proof system 4.Is(a→B)→(a→)→(a→(→) valid? Otherwise, construct a truth valuation which make it false
Definition 6 (Modus Ponens). From α and α → β, we can infer β. This rule is written as follows: α α → β β Now we can define Hilbert proof system. Definition 7. Let Σ be a set of propositions. 1. A proof from Σ is a finite sequence α1, α2, . . . , αn such that for each i ≤ n either: (a) αi is a member of Σ. (b) αi is an axiom; or (c) αi can be inferred from some of previous αj by an application of a rule of inference. 2. α is provable from Σ, Σ ⊢H α, if there is a proof α1, α2, . . . , αn from Σ where αn = α. 3. A proof of α is simply a proof from the empty set 0; α is provable if it is provable from 0. Example 6. Prove the following statements: 1. (α → β) → (α → α). 2. {¬α} ⊢H ((¬β → α) → β). The first can also be proved by tableau proof system. The way to prove the second would not be introduced until the next class. However, you can experience the difference between these two proof systems. Exercises 1. If α is tableau refutable, then α is unsatisfiable. 2. If α is unsatisfiable, then there is a tableau refutation of α. 3. Prove that all axioms are valid in Hilbert proof system. 4. Is ((α → β) → (α → γ)) → (α → (β → γ)) valid? Otherwise, construct a truth valuation which make it false. 4