Constructive formalization of the Tennenbaum theorem and its applications (Q803126)

The author introduces the theory \(CHA=HA+CT+M\), i.e. Heyting arithmetic extended by Church's thesis and Markov's principle. Some other theories closely related to CHA are introduced and investigated (e.g. \(CHA^ 2)\). An interesting analogue of Tennenbaum's result (there are no recursive nonstandard models of arithmetic - cf. \textit{S. Tennenbaum}, ``Non- archimedean systems of arithmetic'', Am. Math. Soc., Notices 6, 270 (1959)) is proved. Using it the author establishes new results on predicate logics. Two of them are stated below. Any class of arithmetical formulas closed via derivability in CHA is called a constructive arithmetical theory (CAT). Let T be a CAT. A predicate formula \({\mathcal U}(P_ 1,...,P_ n)\) is called T-universal iff for all arithmetical formulas \(F_ 1,...,F_ n\) the formula \({\mathcal U}(F_ 1,...,F_ n)\) lies in T. The class of all T-universal formulas is denoted by L(T). [For details cf. the author's paper in Izv. Akad. Nauk SSSR, Ser. Mat. 41, 483-502, 717 (1977; Zbl 0373.02032).] Theorem. If T is a CAT, then \(T\leq_ lL(T)\), i.e. the set of Gödel numbers of formulas of T is l-reducible to the set of the ones of L(T). Theorem. The structure of all CATs together with the relation \(\subseteq\) of inclusion is isomorphic to the structure of all predicate logics L(T) (where T denotes a CAT) together with the relation \(\subseteq.\) Reviewer's remark. There are some misprints in the paper. The most serious one takes place in Theorem 3, where derivability of \(\forall x\exists y R(x,y)\) is stated but derivability of \(\forall x\exists y R(y,x)\) is proved.