Completeness Theorems, Incompleteness Theorems and Models of Arithmetic
Let & be a consistent extension of Peano arithmetic and let 6EJJ denote the set of TL°„ consequences of &. Employing incompleteness theorems to generate independent formulas and completeness theorems to construct models, we build nonstandard models of SP„+2 m which the standard integers are A°+1 -definable. We thus pinpoint induction axioms which are not provable in éE¡¡+2; in particular, we show that (parameter free) A?-induction is not provable in Primitive Recursive Arithmetic. Also, we give a solution of a problem of Gaifman on the existence of roots of diophantine equations in end extensions and answer questions about existentially complete models of 3^. Furthermore, it is shown that the proof of the Gödel Completeness Theorem cannot be formalized in 6E§ and that the MacDowell-Specker Theorem fails for all truncated theories (£¡¡. The completeness theorems of the title are the usual completeness and compactness theorems for the predicate calculus and strong variants of them which are obtained by virtue of the fact that the Henkin proof of the usual completeness theorem can be formalized in arithmetic. The incompleteness theorems are the Gödel theorems and the variants due to Rosser and Mostowski. Using model theoretic methods, Ryll-Nardzewski and also Rabin proved that (Peano) arithmetic was not finitely axiomatizable by showing that all finite subsystems of arithmetic have nonstandard models in which some induction axiom fails. On the other hand, using proof-theoretic methods, Mostowski and also Montague showed that in arithmetic one can prove the consistency of any finite subsystem of arithmetic, which again establishes nonfinite axiomatizability. In this paper we combine these techniques playing off the completeness theorems against the incompleteness theorems and construct nonstandard models of subsystems of arithmetic in which the standard integers and definable (§§3 and 6). The nonfinite axiomatizability results that we obtain in this way are optimal (from the point of view of quantifier complexity). We introduce the notion of representability of a theory in a model, cf. §2, which enables us to apply the incompleteness Received by the editors August 4, 1976. AMS (MOS) subject classifications (1970). Primary 02H05, 02H25, 02G15. (^Various results of this paper were announced in [Mc]. © American Mathematical Society 1978