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 rulesDiscrete 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 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 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