View source for Essentially-undecidable theory

An algorithmically-undecidable logical theory, all consistent extensions of which are also undecidable (see [[Undecidability|Undecidability]]). An [[Elementary theory|elementary theory]] is an essentially-undecidable theory if and only if every model of it has an undecidable elementary theory. Every complete undecidable theory is an essentially-undecidable theory, as is formal arithmetic (cf. [[Arithmetic, formal|Arithmetic, formal]]); no theory with a finite model can be an essentially-undecidable theory.

The essential undecidability of a suitable finitely-axiomatizable elementary theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e0362701.png" /> is often used in proving the undecidability of a given theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e0362702.png" /> (see [[#References|[1]]], [[#References|[2]]]). In this proof, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e0362703.png" /> is interpreted in any model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e0362704.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e0362705.png" />. The domain of interpretation and the values of the elements of the signature of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e0362706.png" /> are defined using values in the model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e0362707.png" /> of suitable formulas in the language of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e0362708.png" />. If the interpretation is a model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e0362709.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e03627010.png" /> is undecidable; moreover, this theory is hereditarily undecidable, i.e. all of its subtheories of the same signature as <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e03627011.png" /> are undecidable. This method is used to prove the undecidability of elementary predicate logic, elementary group theory, elementary field theory, etc. Finitely-axiomatized formal arithmetic is often used as the essentially-undecidable theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/e/e036/e036270/e03627012.png" />.

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Tarski,   A. Mostowski,   R.M. Robinson,   "Undecidable theories" , North-Holland  (1953)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  Yu.L. Ershov,   I.A. Lavrov,   A.D. Taimanov,   M.A. Taitslin,   "Elementary theories"  ''Russian Math. Surveys'' , '''20''' :  4  (1965)  pp. 35–105  ''Uspekhi Mat. Nauk'' , '''20''' :  4  (1965)  pp. 37–108</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  S.C. Kleene,   "Introduction to metamathematics" , North-Holland  (1951)</TD></TR></table>