Namespaces
Variants
Actions

Difference between revisions of "Essentially-undecidable theory"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX done)
 
Line 1: Line 1:
 
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.
 
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" />.
+
The essential undecidability of a suitable finitely-axiomatizable elementary theory $S$ is often used in proving the undecidability of a given theory $T$ (see [[#References|[1]]], [[#References|[2]]]). In this proof, $S$ is interpreted in any model $M$ of $T$. The domain of interpretation and the values of the elements of the signature of $S$ are defined using values in the model $M$ of suitable formulas in the language of $T$. If the interpretation is a model of $S$, then $T$ is undecidable; moreover, this theory is hereditarily undecidable, i.e. all of its subtheories of the same signature as $T$ 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 $S$.
  
 
====References====
 
====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>
+
<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>
 +
 
 +
{{TEX|done}}

Latest revision as of 20:42, 19 October 2017

An algorithmically-undecidable logical theory, all consistent extensions of which are also undecidable (see Undecidability). An 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); no theory with a finite model can be an essentially-undecidable theory.

The essential undecidability of a suitable finitely-axiomatizable elementary theory $S$ is often used in proving the undecidability of a given theory $T$ (see [1], [2]). In this proof, $S$ is interpreted in any model $M$ of $T$. The domain of interpretation and the values of the elements of the signature of $S$ are defined using values in the model $M$ of suitable formulas in the language of $T$. If the interpretation is a model of $S$, then $T$ is undecidable; moreover, this theory is hereditarily undecidable, i.e. all of its subtheories of the same signature as $T$ 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 $S$.

References

[1] A. Tarski, A. Mostowski, R.M. Robinson, "Undecidable theories" , North-Holland (1953)
[2] 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
[3] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
How to Cite This Entry:
Essentially-undecidable theory. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Essentially-undecidable_theory&oldid=17241
This article was adapted from an original article by A.L. Semenov (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article