Compactness theorem

The compactness theorem, also called finiteness theorem, is one of the most important sentences of propositional logic and of first-order predicate logic. He states: A (possibly infinite) set of formulas is satisfiable (ie has a model ) if every finite subset of is satisfiable. For the logic of the second stage of this sentence does not apply.

An important implication of the compactness theorem is that any ( possibly infinite ) set of formulas which has arbitrarily large finite models, even an infinite model has. This conclusion is often the axiomatization of classes of finite structures rebuttable.

Evidence

For the first order predicate logic, the compactness theorem follows as a corollary from the Gödel's completeness theorem. Accordingly briefly also designed the proof:

"": Suppose that X has a model. Then this ( trivially ) is also a model of any finite subset of X.

" ": Assume that every finite set has a model. To generate a contradiction, it is assumed have no model. Then out in a complete and correct formal system a contradiction (eg ) derivable ( Completeness Theorem ). As a derivation in a formal system ( by definition) is finite, and only a finite number of formulas may have been used in this derivation. So from a finite subset of a contradiction derivable, and therefore this does not have a model ( accuracy rate). Contradiction. So it has a model.

At the core of the proof is the following result which follows directly from the Gödel's completeness theorem:

Following is a formula from a set of formulas, so there is a finite set, so that follows. (There are finite with ).

A totally different proof, which dispenses with the notion of syntactic derivability and also on the completeness theorem, results in the model theory of the set of Łoś.

Naming of the compactness theorem

If we consider the space of all theories of a particular language, which have a model, we can provide this space with a topology: The basic quantities are the. The compactness theorem now states precisely that this space is compact.

Position in set theory

In the proof of the compactness theorem transfinite methods such as Zorn's lemma can be used: The crucial point is the set of linden tree, which allows to pass from a consistent theory to a maximally consistent theory. Unlike, for example, the proposition that every vector space has a basis, the compactness theorem is not equivalent to Zorn's lemma and the axiom of choice. However, it is equivalent to a number of other sets such as the Boolean Primidealsatz