Compactness theorem (logic)

The compactness theorem , also called finiteness theorem , is one of the most important theorems of propositional logic and first-order predicate logic . It says: A (possibly infinite) formula set is satisfiable (i.e. has a model) if and only if every finite subset of is satisfiable. This sentence does not apply to the logic of the 2nd level. ${\displaystyle \Sigma }$ ${\displaystyle \Sigma }$

An important consequence of the compactness theorem is that every (possibly infinite) set of formulas that has finite models of arbitrarily large also has an infinite model. With this conclusion the axiomatizability of classes of finite structures can often be refuted. ${\displaystyle \Sigma }$

proof

For the first-order predicate logic, the compactness theorem results as a corollary from Gödel's completeness theorem . The proof is correspondingly short:

" ": Assume has a model. Then this is (trivially) also a model of every finite subset of . ${\displaystyle \Rightarrow }$ ${\displaystyle \Sigma }$ ${\displaystyle \Sigma }$

" ": Assume that every finite set has a model. To generate a contradiction it is assumed that I have no model. Then there follows a semantic contradiction, e.g. B. . Formally: ${\displaystyle \Leftarrow }$ ${\displaystyle \Sigma _{\text{fin}}\subseteq \Sigma }$ ${\displaystyle \Sigma }$ ${\displaystyle \Sigma }$ ${\displaystyle \exists x:x\neq x}$

${\displaystyle \Sigma \models \exists x:x\neq x}$

(Every model that fulfills also fulfills the contradiction. This is true because there is no model for .) ${\displaystyle \Sigma }$ ${\displaystyle \Sigma }$

Gödel's completeness theorem now says that syntactically it already follows from . Formally: ${\displaystyle \exists x:x\neq x}$ ${\displaystyle \Sigma }$

${\displaystyle \Sigma \vdash \exists x:x\neq x}$

So there is a formal proof, a syntactic derivation of from . Since a derivation in a formal system (by definition) is finite, only a finite number of formulas can be used in this derivation . So a contradiction can be derived from a finite subset of , and this therefore has no model (correctness theorem). Contradiction. So you own a model. ${\displaystyle \exists x:x\neq x}$ ${\displaystyle \Sigma }$ ${\displaystyle \Sigma }$ ${\displaystyle \Sigma }$ ${\displaystyle \Sigma }$

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

If a formula follows from a formula set , there is a finite set such that from follows. ( there is finite with ). ${\displaystyle \varphi }$ ${\displaystyle \Sigma }$ ${\displaystyle \Sigma _{\text{fin}}\subseteq \Sigma }$ ${\displaystyle \varphi }$ ${\displaystyle \Sigma _{\text{fin}}}$ ${\displaystyle \Sigma \models \varphi \Rightarrow }$ ${\displaystyle \Sigma _{\text{fin}}\subseteq \Sigma }$ ${\displaystyle \Sigma _{\text{fin}}\models \varphi }$

A completely different proof, which dispenses with the concept of syntactic derivability and the completeness theorem, results in model theory from the theorem of Łoś through ultra-products .

Second order predicate logic

From the compactness theorem it follows that a set of formulas that has an infinite model also has arbitrarily large models. Because has an infinite model, then (infinite) for an arbitrary index set also ${\displaystyle \Sigma }$ ${\displaystyle I}$

${\displaystyle \Sigma \cup \{c_{i}\neq c_{j}|i,j\in I,i\neq j\}}$,

because every finite set has a model. (They are new constant symbols) ${\displaystyle c_{i}}$

In particular, first-order predicate logic can only characterize the finite, but not the infinite models except for isomorphism.

The Peano axioms describe the natural numbers in the second level predicate logic, except for isomorphism. If the set is the Peano axioms, then has no model, although every finite subset has a model. ${\displaystyle \Sigma }$ ${\displaystyle \Sigma \cup \{c>n|n\in \mathbb {N} \}}$

Origin of name

If one considers the space of all theories of a certain language that have a model, then this space can be provided with a topology : The base sets are the . The compactness theorem says that this space is compact . ${\displaystyle Th(L)}$ ${\displaystyle L}$ ${\displaystyle T_{\phi }:=\{T\in Th(L)\mid \phi \in T\}}$

Position in set theory

When proving the compactness theorem, transfinite methods such as For example, Zorn's lemma is used: The decisive point is Lindenbaum's theorem , which allows one to move from a consistent theory to a maximally consistent theory. Unlike z. For example, if the theorem that every vector space has a basis , the compactness theorem is not equivalent to Zorn's lemma or the axiom of choice . However, it is equivalent to a number of other theorems such as the Boolean prime ideal theorem .

literature

• Hans Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Introduction to mathematical logic . Spektrum Akademischer Verlag, Heidelberg 2007, ISBN 3-8274-1691-4 .

Web links

• Lecture slides on propositional logic at the TU Dresden by Steffen Hölldobler (finiteness theorem with proof from p. 86) ( Memento from April 17, 2016 in the Internet Archive ) (PDF; 293 kB)