# 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$.