Discrete Mathematics(II) Spring 2012 Lecture 8: Soundness and Completeness of Propositional logic Lecturer. yil 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”更衣”,uhat' 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 e screen
Discrete Mathematics (II) Spring 2012 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 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 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 non-contradictory path 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 It sets up a connection between truth valuation V and sign of entries along noncontradictory path 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. Ha=a Soundness theorem means that a proposition must be valid if it has a tableaux pro 4 Completeness Theorem Tableaux proof system contains both syntax and semantics Example 5. Given a proposition(a-(B-7m), 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(y)=F, A(B)=T, A(a=T. a truth valuation V extended by A make it fal 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 1.A(A)=T if TA is an entry on P 2.A(A)=F If v is the unique valuation extending the truth assignment A, then v agrees with all entries of
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. 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 . It sets up a connection between truth valuation V and sign of entries along noncontradictory path. 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 tableaux 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: 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. 2
With this lemma, we have completeness theorem Theorem 4(Completeness). If a is valid, then a is tableau provable, i.e. Fa=Ha. 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 tableaux is not contradictory Hilbert Proof System We introduce Hilbert proof system, also known as axiom proof system, as a reference to tableaux 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→(8→1)→(a→3)→(a→1) 9.(-6→-a)→(-B→a)→B) 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 Definition 6(Modus Ponens). From a and a+B, we can infer B. This rule is written as follows a→ B 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, 02, -. 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
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 tableaux 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. 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. 3
2. a is provable from 2, ZHH a, if there is a proof a1, 02, .. an from 2 where an=a 3. 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(B→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 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→1)→(a→(6→) valid? Otherwise, construct a truth valuation which make it false
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
