复旦大学：《离散数学 Discrete Mathematics》英文讲义_14 Soundness and Completeness of Predicate Logic

Discrete Mathematics(Il) Spring 2012 Lecture 14: Soundness and Completeness of Predicate logic Lecturer. YiL 1 Overview 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 propositon 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-Lowenheim theorem and compactness theorem Finally, we can establish a connection between size of model and compactness theorem by introduce new sentences 2 Soundness theorem What's the role of soundness theorem? It guarantees the validity of our proof Basically, a proof is just a procedure. Especially, tableau proof is a very mechanical approach. We just reduce the nodes according to the rules, atomic tableaux and reduce rules An example is given in class. Gong Sunlong, a famous Chinese old philosopher, once made a very ridiculous argument that a white horse is not a horse. Will you accept 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, Gong's argument just reflects the relation between the essence and the specifics However, we does not care about the philosophy view 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 The proof of soundness theorem is very similar to the one in propositional logic. We need only pay attention to the case of quantifiers

Discrete Mathematics (II) Spring 2012 Lecture 14: Soundness and Completeness of Predicate Logic 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 propositon 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 cardiniality 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 introduce new sentences. 2 Soundness theorem What’s the role of soundness theorem? It guarantees the validity of our proof. Basically, a proof is just a procedure. Especially, tableau proof is a very mechanical approach. We just reduce the nodes according to the rules, atomic tableaux and reduce rules. An example is given in class. Gong Sunlong, a famous Chinese old philosopher, once made a very ridiculous argument that a white horse is not a horse. Will you accept 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 philosophy view 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. The proof of soundness theorem is very similar to the one in propositional logic. We need only pay attention to the case of quantifiers. 1

3 Completeness theorem 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 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 3.1 Model construction Example 1. Is the sentence y(R(y, y)v P(, y))AVaR(, a )) invalid? Solution. If a sentence yp is invalid, then mp must be valid. So we can have the tableau proof in figure T y(R(y, y)v P(y, y))AVcR(, ) (R(, y)v P(y, ) T VarR(a, r) T(R(co, co)VP(co, co)), new constant co T VaR(a, r) T R(co, co) oR( P(c0,c0) F R(co, co) T VcR(, a) T R(t1, t1) T VTR(T, a) T R(t2, t2) Figure 1: An example of tableau proof The tableau is not contradictory. So the sentence is not invalid can construct a model along the non-contradictory path. Let domain A=(co, ti, t2, R=(co, co), (t1, t1), (t2, t2), P=I(co, co)1

3 Completeness theorem 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. 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. 3.1 Model construction Example 1. Is the sentence (∃y(¬R(y, y) ∨ P(y, y)) ∧ ∀xR(x, x)) invalid? Solution. If a sentence ϕ is invalid, then ¬ϕ must be valid. So we can have the tableau proof in figure ??. T (∃y(¬R(y, y) ∨ P(y, y)) ∧ ∀xR(x, x)) T ∃y(¬R(y, y) ∨ P(y, y)) T ∀xR(x, x) T (¬R(c0, c0) ∨ P(c0, c0)), new constant c0 T ∀xR(x, x) T R(c0, c0) T ¬R(c0, c0) T P(c0, c0) F R(c0, c0) ⊗ T ∀xR(x, x) T R(t1, t1) T ∀xR(x, x) T R(t2, t2) . . . Figure 1: An example of tableau proof The tableau is not contradictory. So the sentence is not invalid. We can construct a model along the non-contradictory path. Let domain A = {c0, t1, t2}, R = {(c0, c0),(t1, t1),(t2, t2)}, P = {(c0, c0)}. 2

This is a model of the sentence Here, we should be careful about the termination of a tableau proof. In practice, we always reduce B-style first if possible and try to leads contradiction by reducing V-style. The detail argument of when the proof is terminable. Please refer to the phrase in our text book on the page 115 below Fi 4 Size of model Given a language L, we can construct a model A(structure) which interprets constants, functi and predicates. As we have shown that L could have infinite constants, which means L is infinite and A is also infinite Definition 1(size of a model). The size of a model is the cadinality of the universe A in the structre A },{P={},R={ ,n>>. It is easy to check it is a model oj Gy)(R(, y)vP(y, u))V()R(a, Here, we give a finite model. You can also construct a infinite model Example 3. Suppose we have a language L=. Given two sentences e)P(c, r) and(va)(P(a, c)>P(, d)) k. We know that the structure A = is a infinite model of them You can also find a finite model 5 Skolem-Lowenheim theorem In previous case, we have only finite sentence. We are curious about the case that there are maybe infinite sentences. We have the following theorem Theorem 2. If a countable set of sentences s is satisfiable, then it has a countable mode In the proof of completeness theorem, we construct the model by collecting all constants introduced by 3-style node. As any sentence a could be taken as a sequence of symbols. It is obvious that a sentence could only contributes finite possible new constants Proof. Consider the tableau proof with the root F(aAna). The tree is not finite otherwise S unsatisfiable. It means there is a non-contradictory path. We can construct a model along that path. There are at most countable new constants

This is a model of the sentence. Here, we should be careful about the termination of a tableau proof. In practice, we always reduce ∃-style first if possible and try to leads contradiction by reducing ∀-style. The detail argument of when the proof is terminable. Please refer to the phrase in our text book on the page 115 below Figure 33. 4 Size of model Given a language L, we can construct a model A(structure) which interprets constants, functions, and predicates. As we have shown that L could have infinite constants, which means L is infinite and A is also infinite. Definition 1 (size of a model). The size of a model is the cadinality of the universe A in the structre A. Example 2. Let A =}, R = {, , . . . , } >. It is easy to check it is a model of α = (∃y)(¬R(y, y) ∨ P(y, y)) ∨ (∀x)R(x, x). Here, we give a finite model. You can also construct a infinite model. Example 3. Suppose we have a language L =. Given two sentences (∀x)P(c, x) and (∀x)(P(x, c) → P(x, d)). Remark. We know that the structure A = is a inifinite model of them. You can also find a finite model. 5 Skolem-L¨owenheim theorem In previous case, we have only finite sentence. We are curious about the case that there are maybe infinite sentences. We have the following theorem. Theorem 2. If a countable set of sentences S is satisfiable, then it has a countable model. In the proof of completeness theorem, we construct the model by collecting all constants introduced by ∃-style node. As any sentence α could be taken as a sequence of symbols. It is obvious that a sentence could only contributes finite possible new constants. Proof. Consider the tableau proof with the root F(α ∧ ¬α). The tree is not finite otherwise S is unsatisfiable. It means there is a non-contradictory path. We can construct a model along that path. There are at most countable new constants. 3

6 Compactness theorem Theorem 3. Let S=(a1, a2,.. be a set of sentences of predicate logic. S is satisfiable if and only if every finite subset of s is satisfiable Proof. Consider the tableau proof with the root F(aAna). The tree should not be finite otherwise it is contradictory, which means a A na 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 set of sentences with a fixed number. It contradicts to our premises that every finite subset ots.? methods used in the proof of completeness theorem to construct a model which can only satisfy a satisfiable Theorem 4. 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 i-1 01=()∧-(x=c)A∧-(=c) 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 nd sentences. We get a infinite model which also satisfies S Given any finite subset of SUz, 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 7 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

6 Compactness theorem Theorem 3. Let S = {α1, α2, . . .} be a set of sentences of predicate logic. S is satisfiable if and only if every finite subset of S is satisfiable. 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 4. 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. 7 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 4

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 Exercises Caution: In the question 4 and 5, we do not just consider a very special model. For the sentence or sentences you are given, you should consider all possible models, which means all possible interpretation of your predicates and functions 1.6/P126 3.10/P126 5.3/P125

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. Exercises Caution: In the question 4 and 5, we do not just consider a very special model. For the sentence or sentences you are given, you should consider all possible models, which means all possible interpretation of your predicates and functions. 1. 6/P126 2. 9/P126 3. 10/P126 4. 2/P125 5. 3/P125 6. 4/P125 5