The Varpakhovskh calculus and Markov arithmetic

Abstract

The study of propositional realizability logic was initiated in the 50th of the last century. Unfortunately, no description of the class of realizable propositional formulas is found up to now. Nevertheless some attempts of such a description were made. In 1974 the author proved that every known realizable propositional formula has the property that every one of its closed arithmetical instances is deducible in the system obtained by adding Extended Church Thesis and Markov Principle as axiom schemes to Intuitionistic Arithmetic. A. Visser calles this system Markov Arithmetic. In 1990 another attempt of describing the class of realizable propositional formulas was made by F. L. Varpakhovskii who proposed a calculus in an extended propositional language and proved that all known realizable propositional formulas are deducible in this calculus. In this paper we prove that every propositional formula deducible in Varpakhovskii’s calculus has the property that every one of its closed arithmetical instances is deducible in Markov Arithmetic.