复旦大学：《离散数学》习题课讲稿（李弋）15 Soundness, Completeness and Compactness.pdf_大学文库

Discrete Mathematics(ID) Spring 2013 Lecture 15: Soundness, Completeness and Compactness 1 Overview In this lecture, we will prvoe the soundness and completeness of tableau proof system, as we did for proposition logic proof system. These two theorems are the fundamental theorems of the first order logic. You can think it as two generals Hen and Ha, who are always posted on the door traditionally. We hope that they can protect our home The proof of the theorems is the same as the one used in proposition logic but the technique is special on how to handle quantifiers. We can also use this technique to construct a model,a tructure, which can satisfy all the sentences Furthermore, we discuss the model size, actually the cardinality of universe in structure. Then we proved Skolem-LOwenheim theorem and compactness theorem. Finally, we can establish a connection between size of model and compactness theorem by intro- ducing infinite new sentences. Actually, it is just an application of compactness theorem 2 Soundness theorem Once you are told about something. You may say it sounds reasonable. It means that you may think the fact you know may be true. How about the proof system. It's the role of soundness theorem, which guarantees the validity of our proof Gong Sunlong, a famous Chinese old philosopher, once made a very ridiculous argument that a white horse is not a horse. Will you agree with his view? If you can not be persuaded by him, can you find the faw in his proof? In the point of view of Philosophy, Gongs argument just reflects the relation between the essence and the specifics However, we does not care about the view of philosophy here. His proof is our focus. As we know, we may know how to write a program and we have written so many correct programs. But we may still make mistakes and write wrong program. Sometimes, you may even doubt the compiler is wrong. And actually, compiler sometimes really generate wrong binary but your program correct Similarly, we may make wrong proof. And furthermore, would you doubt the validity of our proof itself? Soundness is the very theorem to eliminate our doubts. Basically, a proof is just a procedure. Especially, it is a very mechanical approach to prove that a sentence is a consequence of a set by using tableau proof. We just reduce and generate the nodes according to the rules atomic tableaux and reduce rules

Discrete Mathematics (II) Spring 2013 Lecture 15: Soundness, Completeness and Compactness Lecturer: Yi Li 1 Overview In this lecture, we will prvoe the soundness and completeness of tableau proof system, as we did for proposition logic proof system. These two theorems are the fundamental theorems of the first order logic. You can think it as two generals Hen and Ha, who are always posted on the door traditionally. We hope that they can protect our home. The proof of the theorems is the same as the one used in proposition logic but the technique is special on how to handle quantifiers. We can also use this technique to construct a model, a structure, which can satisfy all the sentences. Furthermore, we discuss the model size, actually the cardinality of universe in structure. Then we proved Skolem-L¨owenheim theorem and compactness theorem. Finally, we can establish a connection between size of model and compactness theorem by introducing infinite new sentences. Actually, it is just an application of compactness theorem. 2 Soundness theorem Once you are told about something. You may say it sounds reasonable. It means that you may think the fact you know may be true. How about the proof system. It’s the role of soundness theorem, which guarantees the validity of our proof. Gong Sunlong, a famous Chinese old philosopher, once made a very ridiculous argument that a white horse is not a horse. Will you agree with his view? If you can not be persuaded by him, can you find the flaw in his proof? In the point of view of Philosophy, Gong’s argument just reflects the relation between the essence and the specifics. However, we does not care about the view of philosophy here. His proof is our focus. As we know, we may know how to write a program and we have written so many correct programs. But we may still make mistakes and write wrong program. Sometimes, you may even doubt the compiler is wrong. And actually, compiler sometimes really generate wrong binary but your program is correct. Similarly, we may make wrong proof. And furthermore, would you doubt the validity of our proof itself? Soundness is the very theorem to eliminate our doubts. Basically, a proof is just a procedure. Especially, it is a very mechanical approach to prove that a sentence is a consequence of a set by using tableau proof. We just reduce and generate the nodes according to the rules: atomic tableaux and reduce rules. 1

In predicate language, we introduce predicate, quantifier, function, constant, and variable to en hance the expressing power. In order to accommodate the changes, several new tableaux are introduced. The soundness of the proof system looks broken because of these new ones. So we need to reprove the soundness of the new tableau proof system. However the proof of soundness theorem is very similar to the one in propositional logic. We need only pay attention to the case of quantifiers. Here, we mean how to establish the connection between syntax and semantics of tableaux related with quantifiers. Especially, the interpretations associated with all-style quantifier are very difficult to understand. Because we want to use information as little as possible to check all cases Lemma 1. If T=UTn is a tableau from a set of sentences S with root Fa, then any C-structure A that is a model of Suna can be extended to one agreeing with every entry on some path P through T. Recall that A agrees with Ta(Fa) if a is true(false) in A Theorem 2(Soundness). If there is a tableau proof r of a from S, then Sha 3 Completeness theorem 3.1 Proof In our life, sometimes you know something is definitely right. But you may find it is hard to persuade others for you cannot give a reasonable argument. Is there any problem which is right but we can not give a proof? The answer is positive. Completeness theorem guarantees that there must exist a proof if it is right in first order logic. If you cannot prove it, it just means that you are unlucky and you need do better and harder work Theorem 3. Suppose P is a noncontradictory path through a complete systematic tableau t from S with root Fa. There is then a structure A in which a is false and every sentence in s is true 1. If FB occurs on P, then B is false in A 2. If TB occurs on P, then B is true in A Corollary 4. For every sentence a and set of sentences S of L, either 1. the CST from S with root Fa is a tableau proof of a from S 2. there is a noncontradictory branch through the complete systematic tableau that yields a struc ture in that a is false and every element of s is true 3.2 Model construction Actually, the proof show us a way to construct a real model to show that a sentence is true or fal while the model is still abstract because we may not find a real example

In predicate language, we introduce predicate, quantifier, function, constant, and variable to enhance the expressing power. In order to accommodate the changes, several new tableaux are introduced. The soundness of the proof system looks broken because of these new ones. So we need to reprove the soundness of the new tableau proof system. However the proof of soundness theorem is very similar to the one in propositional logic. We need only pay attention to the case of quantifiers. Here, we mean how to establish the connection between syntax and semantics of tableaux related with quantifiers. Especially, the interpretations associated with all-style quantifier are very difficult to understand. Because we want to use information as little as possible to check all cases. Lemma 1. If τ = ∪τn is a tableau from a set of sentences S with root F α, then any L-structure A that is a model of S ∪ {¬α} can be extended to one agreeing with every entry on some path P through τ .( Recall that A agrees with T α(F α) if α is true(false) in A.) Theorem 2 (Soundness). If there is a tableau proof τ of α from S, then S |= α. 3 Completeness theorem 3.1 Proof In our life, sometimes you know something is definitely right. But you may find it is hard to persuade others for you cannot give a reasonable argument. Is there any problem which is right but we can not give a proof? The answer is positive. Completeness theorem guarantees that there must exist a proof if it is right in first order logic. If you cannot prove it, it just means that you are unlucky and you need do better and harder work. Theorem 3. Suppose P is a noncontradictory path through a complete systematic tableau τ from S with root F α. There is then a structure A in which α is false and every sentence in S is true. 1. If F β occurs on P, then β is false in A. 2. If T β occurs on P, then β is true in A. Corollary 4. For every sentence α and set of sentences S of L, either 1. the CST from S with root F α is a tableau proof of α from S. or 2. there is a noncontradictory branch through the complete systematic tableau that yields a structure in that α is false and every element of S is true. 3.2 Model construction Actually, the proof show us a way to construct a real model to show that a sentence is true or false, while the model is still abstract because we may not find a real example. 2

Proof. Consider the tableau proof with the root F(aM-a). The tree should not be finite otherwise it is contradictory, which means a A no could be proved from S and hence S is unsatisfiable However, if we have a tableau proof, it means that the tree only has finite path. We can follow the methods used in the proof of completeness theorem to construct a model which can only satisfy a set of sentences with a fixed number. It contradicts to our premises that every finite subset of s is satisfiable Theorem 9. Let L be a first-order language. Any set S of sentences of l that is satisfiable in arbitrarily large finite models is satisfiable in some infinite model. Suppose S is satisfiable in arbitrary large finite models. Let R be a two-ary relation symbol that is not part of the language L, and enlarge L to L by adding R We can modify the interpretation of R without affecting the truth values of members of s, since R does not occur in members of S. So we can write a sentence on that asserts there are at least n different elements After we construct a new structure, which can satisfy all sentences. Now we can get rid of newly introduced sentences and predicates. It can be implied that this model can satisfy S. Proof. We can introduce a new predicates and a set of new constants(C1, c2,..., Ci,... Now we construct a set of sentences 2=oi, i>21, where o1=(n)∧-(x=c)A∧-(q=c) 1≤i<j<i-1 which means there are at least i elements in the domain Now consider the set of sentence SU2. If we can prove that its any finite subset of sentence is satisfiable we can prove that itself is satisfiable by applying Compactness Theorem. It is obvious that the size of model is infinite. Now we just eliminate all newly introduced constants, predicate and sentences. We get a infinite model which also satisfies s Given any finite subset of su2, 2 implies there is a finite model. Premises guarantee that s also has a model with the same number of elements. We just prove that any finite subset of Sux is satisfiable 6 Conclusion In the proof, we use induction methods. Top-down approach is adopted for soundness theorem. For the base step, the root node satisfies. Given a noncontradictory path, we can prove the augmented path also satisfies if it satisfy. While bottom-up method is used in the proof of completeness theorem. Where we consider the simplest symbols first like constant and ground terms. Then we consider the atomic predicates and sentences with quantifiers and connectives Finally, we introduce the model theory of first order logic. Compactness Theorem and an application of it are given

Proof. Consider the tableau proof with the root F(α∧¬α). The tree should not be finite otherwise it is contradictory, which means α ∧ ¬α could be proved from S and hence S is unsatisfiable. However, if we have a tableau proof, it means that the tree only has finite path. We can follow the methods used in the proof of completeness theorem to construct a model which can only satisfy a set of sentences with a fixed number. It contradicts to our premises that every finite subset of S is satisfiable. Theorem 9. Let L be a first-order language. Any set S of sentences of L that is satisfiable in arbitrarily large finite models is satisfiable in some infinite model. Suppose S is satisfiable in arbitrary large finite models. Let R be a two-ary relation symbol that is not part of the language L, and enlarge L to L ′ by adding R. We can modify the interpretation of R without affecting the truth values of members of S, since R does not occur in members of S. So we can write a sentence σn that asserts there are at least n different elements. After we construct a new structure, which can satisfy all sentences. Now we can get rid of newly introduced sentences and predicates. It can be implied that this model can satisfy S. Proof. We can introduce a new predicates = and a set of new constants {c1, c2, . . . , ci , . . .}. Now we construct a set of sentences Σ = {σi , i ≥ 2}, where σi = (∃x)( i ∧−1 k=1 ¬(x = ck) ∧ ∧ 1≤i<j≤i−1 ¬(ci = cj )), which means there are at least i elements in the domain. Now consider the set of sentence S ∪ Σ. If we can prove that its any finite subset of sentence is satisfiable we can prove that itself is satisfiable by applying Compactness Theorem. It is obvious that the size of model is infinite. Now we just eliminate all newly introduced constants, predicate, and sentences. We get a infinite model which also satisfies S. Given any finite subset of S ′ ∪ Σ ′ , Σ′ implies there is a finite model. Premises guarantee that S ′ also has a model with the same number of elements. We just prove that any finite subset of S ∪ Σ is satisfiable. 6 Conclusion In the proof, we use induction methods. Top-down approach is adopted for soundness theorem. For the base step, the root node satisfies. Given a noncontradictory path, we can prove the augmented path also satisfies if it satisfy. While bottom-up method is used in the proof of completeness theorem. Where we consider the simplest symbols first like constant and ground terms. Then we consider the atomic predicates and sentences with quantifiers and connectives. Finally, we introduce the model theory of first order logic. Compactness Theorem and an application of it are given. 5