zbMATH — the first resource for mathematics

Modified realizability and predicate logic. (English. Russian original) Zbl 0912.03027
Math. Notes 61, No. 2, 212-220 (1997); translation from Mat. Zametki 61, No. 2, 259-269 (1997).
Summary: Semantics of predicate formulas based on the notion of modified realizability for arithmetic formulas and interpretations of the language of arithmetic in all finite types are considered. For a number of natural constructive intepretations, the corresponding predicate logic of modified realizability is proved to be nonarithmetical.

03F30 First-order arithmetic and fragments
03C62 Models of arithmetic and set theory
03F50 Metamathematics of constructive systems
Full Text: DOI
[1] S. C. Kleene, ”On the interpretation of intuitionistic number theory,”J. Symbolic Logic.,10, No. 4, 109–124 (1945). · Zbl 0063.03260 · doi:10.2307/2269016
[2] N. A. Shanin, ”On some logical problems of arithmetic,”Trudy Mat. Inst. Steklov [Proc. Steklov Inst. Math.],43, 1–112 (1955).
[3] F. L. Varpakhovskii, ”On axiomatization of realizable propositional formulas,”Dokl. Akad. Nauk SSSR [Soviet Math. Dokl.],314, No. 1, 32–36 (1990). · Zbl 0742.03002
[4] V. E. Plisko, ”On realizable predicate formulas,”Dokl. Akad. Nauk SSSR [Soviet Math. Dokl.],212, No. 3, 553–556 (1973). · Zbl 0295.02009
[5] V. E. Plisko, ”Nonarithmeticity of the class of realizable predicate formulas,”Izv. Akad. Nauk SSSR Ser. Mat. [Math. USSR-Izv.],41, No. 3, 483–502 (1977). · Zbl 0382.03043
[6] G. Kreisel, ”Interpretation of analysis by means of constructive functionals of finite type,” in:Constructivity in Math, North-Holland, Amsterdam (1959), pp. 101–128.
[7] S. Tennenbaum, ”Non-archimedean systems of arithmetic,”Not. Amer. Math. Soc.,6, No. 3, 270–283 (1959).
[8] V. E. Plisko, ”Formalization of the Tennenbaum theorem and its applications,” [in Russian] Dep. VINITI No. 1853-92, Moscow (1992). · Zbl 0727.03037
[9] V. E. Plisko, ”Constructive formalization of the Tennenbaum theorem and its applications,”Mat. Zametki [Math. Notes],48, No. 3, 108–118 (1990). · Zbl 0727.03037
[10] Metamathematical investigation of intuitionistic arithmetic and analysis, Lect. Notes in Math, Vol. 344 (A. S. Troelstra, editor), Springer Verlag, Berlin (1973). · Zbl 0275.02025
[11] S. C. Kleene,Introduction to Metamathematics, Van Nostrand, New York (1952). · Zbl 0047.00703
[12] H. Rogers, Jr.,Theory of Recursive Functions and Effective Computability, MIT Press, Cambridge (1987).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.