Constructive formalization of the Tennenbaum theorem and its applications
type: Item
instance of: scholarly article
title: Constructive formalization of the Tennenbaum theorem and its applications
zbMATH Open document ID: 0727.03037
DOI: 10.1007/BF01157440
published in: Mathematical Notes
publication date: 1990-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03F30
zbMATH DE Number: 4200196
zbMATH Keywords: constructive arithmetic
zbMATH Keywords: Heyting arithmetic
zbMATH Keywords: Church's thesis
zbMATH Keywords: Markov's principle
zbMATH Keywords: predicate logics
zbMATH Keywords: Gödel numbers
author: Valery Plisko
MaRDI profile type: Publication
cites work: Q5559230
cites work: Q4047525
cites work: Formal systems for some branches of intuitionistic analysis
full work available at URL: https://doi.org/10.1007/bf01157440
OpenAlex ID: W1978287663
description: scientific article; zbMATH DE number 4200196