Editing First-order logic (section)

===The compactness theorem===
The [[compactness theorem]] states that a set of first-order sentences has a model if and only if every finite subset of it has a model.<ref>Hodel, R. E., ''An Introduction to Mathematical Logic'' ([[Mineola, New York|Mineola NY]]: [[Dover Publications|Dover]], 1995), [https://books.google.com/books?id=SxRYdzWio84C&pg=PA199 p. 199].</ref> This implies that if a formula is a logical consequence of an infinite set of first-order axioms, then it is a logical consequence of some finite number of those axioms. This theorem was proved first by Kurt Gödel as a consequence of the completeness theorem, but many additional proofs have been obtained over time. It is a central tool in model theory, providing a fundamental method for constructing models.

The compactness theorem has a limiting effect on which collections of first-order structures are elementary classes. For example, the compactness theorem implies that any theory that has arbitrarily large finite models has an infinite model. Thus, the class of all finite [[Graph (discrete mathematics)|graphs]] is not an elementary class (the same holds for many other algebraic structures).

There are also more subtle limitations of first-order logic that are implied by the compactness theorem. For example, in computer science, many situations can be modeled as a [[directed graph]] of states (nodes) and connections (directed edges).  Validating such a system may require showing that no "bad" state can be reached from any "good" state. Thus, one seeks to determine if the good and bad states are in different [[connected component (graph theory)|connected components]] of the graph. However, the compactness theorem can be used to show that connected graphs are not an elementary class in first-order logic, and there is no formula φ(''x'',''y'') of first-order logic, in the [[logic of graphs]], that expresses the idea that there is a path from ''x'' to ''y''. Connectedness can be expressed in [[second-order logic]], however, but not with only existential set quantifiers, as <math>\Sigma_1^1</math> also enjoys compactness.