Henkin's theorem

The set of Henkin , named after Leon Henkin , is a set of the mathematical logic . He deals with the question of when the term interpretation for a given set of expressions of a first-order predicate logic is a model of this set. This theorem leads both to an alternative proof of Gödel's completeness theorem and to a proof of the Löwenheim-Skolem theorem .

Let it be a given set of expressions of a first-order language . If there is no contradiction, that is, if no expression of the form can be derived from it, Gödel's theorem of completeness ensures the existence of a model . The idea of using term interpretation for construction goes back to Leon Henkin . To do this, it must first be clarified under which conditions the term interpretation is a model for the set of expressions . Two definitions are necessary for Henkin's theorem, which deals with precisely this question. ${\displaystyle \Phi }$ ${\displaystyle L_{I}^{S}}$ ${\displaystyle \Phi }$ ${\displaystyle \varphi \land \neg \varphi }$ ${\displaystyle {\mathcal {T}}^{\Phi }}$ ${\displaystyle \Phi }$

A set of expressions is called faithful to negation , if for every expression it holds that or , that is , if an expression is not derivable from , then its negation is derivable. ${\displaystyle \Phi }$ ${\displaystyle \varphi }$ ${\displaystyle \Phi \vdash \varphi }$ ${\displaystyle \Phi \vdash \neg \varphi }$ ${\displaystyle \Phi }$

An expression set has examples if there is a language term for every expression of the form , so that it can be derived from . Stands for the expression that results from when the variable is replaced by the term . The set of expressions can therefore provide an example for every assertion of existence. ${\displaystyle \Phi }$ ${\displaystyle \exists x\varphi }$ ${\displaystyle t}$ ${\displaystyle (\exists x\varphi \rightarrow \varphi {\frac {t}{x}})}$ ${\displaystyle \Phi }$ ${\displaystyle \varphi {\frac {t}{x}}}$ ${\displaystyle \varphi }$ ${\displaystyle x}$ ${\displaystyle t}$

• Henkin's theorem : If a set of expressions is consistent and true to negation and contains examples, then the following applies to every expression : ${\displaystyle \Phi }$ ${\displaystyle \varphi }$

${\displaystyle {\mathcal {T}}^{\Phi }\vDash \varphi \quad \Leftrightarrow \quad \Phi \vdash \varphi }$.

Where means that a model is for . In particular, the term interpretation for is also a model of , that is, it applies . ${\displaystyle {\mathcal {T}}^{\Phi }\vDash \varphi }$ ${\displaystyle {\mathcal {T}}^{\Phi }}$ ${\displaystyle \varphi }$ ${\displaystyle \Phi }$ ${\displaystyle \Phi }$ ${\displaystyle {\mathcal {T}}^{\Phi }\vDash \Phi }$

Conflicting sets are usually neither true to negation nor do they contain examples. In order to apply Henkin's theorem to prove the existence of a model, one has to expand the set of expressions and the set of symbols in such a way that the requirements for this expanded situation are fulfilled. This is Henkin's proof of the theorem of completeness. If the set of symbols is at most countable from the start , then the extended set of symbols is also at most countable. Since the set of terms is then at most countable, the term interpretation according to Henkin's theorem represents a model that can at most be counted and one easily obtains the Löwenheim-Skolem theorem . ${\displaystyle \Phi }$ ${\displaystyle S}$

literature

• Heinz-Dieter Ebbinghaus , Jörg Flum, Wolfgang Thomas: Introduction to mathematical logic . 4th edition. Spectrum Akademischer Verlag, Heidelberg 1998, ISBN 3-8274-0130-5 , in particular Chapter V, §1.