In symbolic logic, the compactness theorem asserts that a set of first-order sentences is satifiable, i.e., has a model, if and only if every finite subset of it is satifiable. Goedel's completeness theorem says that any consistent set of sentences in logic has a model, so the compactness theorem is a corollary of the completeness theorem. Goedel originally proved the compactness theorem in just that way, but later some "purely semantic" proofs of the compactness theorem were found, i.e., proofs that refer to truth but not to provability. The concept of "consistency", which occurs in the statement of the completeness theorem, relies essentially on the idea of "provability", since a set of sentences is consistent if and only if no contradiction is provable from sentences in the set. The finite nature of proofs entails the finiteness in the compactness theorem when Goedel's way of proving the compactness theorem is followed.
This is a basic fact in logic and model theory, and has very far-reaching consequences. For instance, it follows that if some first-order sentence can be true in fields of arbitrary large characteristic, it must also be true in some field of characteristic zero. In other words, if some sentence holds for every field of characteristic zero it must hold for every field of characteristic larger than some constant.
Also, it follows that any theory that has an infinite model has models of arbitrary large cardinality. So, for instance, there are nonstandard models of Peano arithmetic with uncountably many natural numbers. The nonstandard analysis is another example where infinite natural numbers appear, a possibility that cannot be excluded by any axiomatization - also a consequence of the compactness theorem.