On a~class of realizable propositional formulas
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part IV, Tome 20 (1971), pp. 8-23
Voir la notice de l'article provenant de la source Math-Net.Ru
Propositional formula is called regularly realizable if there exists a number realizing (in Kleene's sense) every closed, arithmetical substitution instance of the formula. In this paper there is constructed a class $R$ of propositional formulas with the following properties: I) $R$ contains all intuitionistically derivable propositional formulas and is closed relative to rules of intuitionistic propositional calculus; 2) $R$ is recursively decidable; 3) every formula of $R$ is regularly realizable.
All realizable propositional formulas known to the author are contained in $R$.
@article{ZNSL_1971_20_a1,
author = {F. L. Varpakhovskii},
title = {On a~class of realizable propositional formulas},
journal = {Zapiski Nauchnykh Seminarov POMI},
pages = {8--23},
publisher = {mathdoc},
volume = {20},
year = {1971},
language = {ru},
url = {http://geodesic.mathdoc.fr/item/ZNSL_1971_20_a1/}
}
F. L. Varpakhovskii. On a~class of realizable propositional formulas. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part IV, Tome 20 (1971), pp. 8-23. http://geodesic.mathdoc.fr/item/ZNSL_1971_20_a1/