Set of traditional bread

The Trachtenbrot phrase , named after Boris Trachtenbrot , is a phrase taken from mathematical logic . It was proved in 1950 and states that the sentences of first order predicate logic that are generally valid in all finite models cannot be recursively enumerated . This has consequences for the second level predicate logic .

Formulations of the sentence

Let it be the set of symbols with a countably infinite number of constant symbols and a countably infinite number of function and relation symbols for each arity . Furthermore, let the set of all - sentences of the first order predicate logic be satisfied in all finite - structures . Then: ${\displaystyle S_{\infty }}$ ${\displaystyle \Phi _{a}}$ ${\displaystyle L_{I}^{S_{\infty }}}$ ${\displaystyle S_{\infty }}$

${\displaystyle \Phi _{a}}$ is not recursively enumerable.

Abstract: The finite general sentences of the first level cannot be recursively enumerated.

Let us also be the set of all -Sorems for which there is a - structure in which they are fulfilled. Then: ${\displaystyle \Phi _{e}}$ ${\displaystyle L_{I}^{S_{\infty }}}$ ${\displaystyle S_{\infty }}$

${\displaystyle \Phi _{e}}$ is not decidable.

Abstract: The first-order propositions that can be fulfilled in the finite are not decidable.

Comment on evidence

The second formulation is traced back to the unsolvability of the halting problem by exploiting the fact that Turing machines can be described in finite models. The first-mentioned version then results from this, for the propositions generally valid in the finite are precisely the negations of the propositions which can not be fulfilled in the finite.

Second level predicate logic incompleteness

As an application we show how the incompleteness of the second order predicate logic follows from the Trachtenbrot theorem. Let it be the set of sentences of second order predicate logic that are valid in all models. Then: ${\displaystyle \Phi }$

${\displaystyle \Phi }$ is not recursively enumerable.

This state of affairs is called the incompleteness of the second order predicate logic. To prove it, let us consider a second order theorem of predicate logic that is true in finite models, for example ${\displaystyle \varphi _{endl}}$

${\displaystyle \varphi _{endl}=\forall X\,((\forall x\,\exists ^{1}y\,Xxy\,\land \,\forall xyz\,(Xxz\land Xyz\rightarrow x\equiv y))\rightarrow \forall y\,\exists x\,Xxy)}$,

d. H. for all , if a function is and is injective, then is surjective. If it were recursively enumerable, then an enumeration procedure should be started and whenever this produces a statement of the form with a sentence of the first-order predicate logic, it is output. In this way, all of the finite, generally applicable first-order sentences are enumerated, which contradicts the principle of Trachtenbrot. ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle \Phi }$ ${\displaystyle \varphi _{endl}\rightarrow \varphi }$ ${\displaystyle L_{I}^{S_{\infty }}}$ ${\displaystyle \varphi }$ ${\displaystyle \varphi }$

Individual evidence

1. ↑ B. Trakhtenbrot: The impossibility of an algorithm for the decision problem in the finite (Russian), Doklady Akademii Nauk SSSR (1950), volume 70, pages 569-572. English translation in American Mathematical Society, Translations (1963), Series 2, Volume 23, pages 1-5.
2. ↑ H.-D. Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic , spectrum Akademischer Verlag, ISBN 3-8274-0130-5 , X, sentence 5.4
3. ↑ H.-D. Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic , spectrum Akademischer Verlag, ISBN 3-8274-0130-5 , X, sentence 5.3
4. ↑ H.-D. Ebbinghaus, J. Flum, W. Thomas: Finite Model Theory , Springer Verlag, ISBN 3-540-28787-6 , Theorem 7.2.1
5. ↑ H.-D. Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic , spectrum Akademischer Verlag, ISBN 3-8274-0130-5 , X, sentence 5.5