Turing machine computations in finitely axiomatizable theories (Q1059628)

In this paper we describe a general method for interpreting how Turing machines perform computations in finitely axiomatizable theories. The method can be used to construct finitely axiomatizable theories whose properties are determined by Turing machine computations. This method is used to prove that the Lindenbaum Boolean algebra for any recursively enumerable theory \({\mathcal T}\) is recursively isomorphic to the Lindenbaum algebra of a suitable finitely axiomatizable theory \({\mathcal F}\). In addition, the axiom system of the theory \({\mathcal F}\) and the recursive isomorphism of the Boolean algebras \({\mathcal T}\) and \({\mathcal F}\) can be found uniformly with respect to a recursively enumerable index for the axiom system of \({\mathcal T}\). This solves a problem due to \textit{W. Hanf} [Theory of models, Proc. 1963 Int. Symp. Berkeley, 132-145 (1965; Zbl 0166.258)], given as No.22 in H. Friedman's list. \textit{W. Hanf} announced the solution of this problem in Bull. Am. Math. Soc. 81, 587-589 (1975; Zbl 0324.02044) but no proof was ever published. We then use the above method of interpretation to study the properties of simple models. We construct a finitely axiomatizable complete theory possessing a nonconstructivizable simple model, thereby solving a problem posed by \textit{L. Harrington} [J. Symb. Logic 39, 305-309 (1974; Zbl 0332.02055)]. In Section 7 we estimate the complexity of some classes of formulas. The interpretations are based on the author's construction of a complete finitely axiomatizable superstable theory. The models for this theory can be represented as planes on which Turing machines can operate.