05961421

j

05961421 Plisko, Valery On two attempts of describing propositional realizability logic. J. Log. Comput. 21, No. 4, 639-663 (2011). 2011 Oxford University Press, Oxford EN propositional logic recursive realizability Markov arithmetic Zbl 0063.03260 Zbl 0058.24901 Zbl 1170.03005 Zbl 0742.03002

doi:10.1093/logcom/exp045

Recursive realizability, introduced by {\it S. C. Kleene} [J. Symb. Log. 10, 109--124 (1945; Zbl 0063.03260)] as a semantics of arithmetical sentences, can be considered as a more precise definition of the informal intuitionistic semantics. It was proved by {\it D. Nelson} [Trans. Am. Math. Soc. 61, 307--368 (1947; Zbl 0058.24901)] that each formula provable in Heyting arithmetic is realizable. Every realizable propositional formula can be considered as a constructive logical principle (see [{\it V. E. Plisko}, Bull. Symb. Log. 15, No. 1, 1--42 (2009; Zbl 1170.03005)]). In this paper the author gives an extensive survey of Markov arithmetic, presenting an extension of Heyting arithmetic by Markov's Principle and Extended Church's Thesis, and Varpakhovskij calculus (see [{\it F. L. Varpakhovskij}, Sov. Math., Dokl. 42, No. 2, 260--264 (1991); translation from Dokl. Akad. Nauk SSSR 314, No. 1, 32--36 (1990; Zbl 0742.03002)]) based on an extended propositional language, and proves that every propositional formula provable in the Varpakhovskij calculus has the property that each of its closed arithmetical instances is provable in Markov arithmetic. Branislav Bori\v ci\'c (Beograd)