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 givenProof. 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