Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-24T01:46:56.508Z Has data issue: false hasContentIssue false
  • English
  • Français

A Survey of Propositional Realizability Logic

Published online by Cambridge University Press:  15 January 2014

Valery Plisko
Valery Plisko*
Affiliation:
Faculty of Mechanics and Mathematics, Moscow State University, Moscow, 119991, RussiaE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The study of propositional realizability logic was initiated in the 50th of the last century. Some interesting results were obtained in the 60-70th, but many important problems in this area are still open. Now interest to these problems from new generation of researchers is observed. This survey contains an exposition of the results on propositional realizability logic and corresponding techniques. Thus reading this paper can be the start point in exploring and development of constructive logic.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 15 , Issue 1 , March 2009 , pp. 1 - 42
Copyright
Copyright © Association for Symbolic Logic 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Artemov, S., Logic of proofs, Annals of Pure and Applied Logic, vol. 67 (1994), pp. 29–59.CrossRefGoogle Scholar
[2] Chernov, A. V., Skvortsov, D. P., Skvortsova, E. Z., and Vereshchagin, N. K., Variants of realizability for propositional formulas and the logic of weak excluded middle, Proceedings of the Steklov Institute of Mathematics, vol. 242 (2003), pp. 67–85.Google Scholar
[3] Dragalin, A. G., Mathematical intuitionism, American Mathematical Society, Providence, Rhode Island, 1988.Google Scholar
[4] Gentzen, G., Untersuchungen über das logische Schliessen. I, II, Mathematische Zeitschrift, vol. 39 (1934–1935), pp. 176–210, 405–431.Google Scholar
[5] Glivenko, V. I., Sur quelques points de la logique de M. Brouwer, Bulletin Classe des Sciences Academie Royal Belgique, Série 5, vol. 15 (1929), pp. 183–188.Google Scholar
[6] Gödel, K., Eine Interpretation des intuitionistischen Aussagenkalküls, Ergebnisse eines mathematischen Kolloquiums, vol. 4 (1933), pp. 39–40.Google Scholar
[7] Heyting, A., Die formalen Regeln der intuitionistischen Logik, Sitzungsberichte der Preussischen Akademie der Wissenschaften. Physikalisch-mathematische Klasse, (1930), pp. 42–52.Google Scholar
[8] Hilbert, D. and Bernays, P., Grundlagen der Mathematik. I, 2nd ed., Springer-Verlag, 1968.Google Scholar
[9] Jankov, V. A., On realizable formulas of propositional logic (Russian), Doklady Akademii Nauk SSSR, vol. 151 (1963), pp. 1035–1037, translation Soviet Mathematics Doklady , vol. 4, pp. 1146–1148.Google Scholar
[10] Jankov, V. A., On the connection between deducibility in the intuitionistic propositional calculus and finite implicative structures (Russian), Doklady Akademii Nauk SSSR, vol. 151 (1963), pp. 1293–1294, translation Soviet Mathematics Doklady , vol. 4, pp. 1203–1204.Google Scholar
[11] Jaśkowski, S., Recherches sur le système de la logique intuitioniste, Actes du Congrès International de Philosophie Scientifique, VI, Philosophie des mathématique. Actualités scientifique et industrielle, vol. 393 (1936), pp. 58–61.Google Scholar
[12] Johansson, I., Der Minimalkalkül, ein reduzierte intuitionistischer Formalismus, Compositio Mathematica, vol. 4 (1937), pp. 119–136.Google Scholar
[13] Kabakov, F. A., Intuitionistic deducibility of some realizable formulae of propositional logic (Russian), Doklady Akademii Nauk SSSR, vol. 192 (1970), pp. 269–271, translation Soviet Mathematics Doklady , vol. 11, pp. 612–614.Google Scholar
[14] Kabakov, F. A., On modelling of pseudo-boolean algebras by realizability (Russian), Doklady Akademii Nauk SSSR, vol. 192 (1970), pp. 16–18, translation Soviet Mathematics Doklady , vol. 11, pp. 562–564.Google Scholar
[15] Kipnis, M. M., On a property of propositional formulas (Russian), Doklady Akademii Nauk SSSR, vol. 174 (1967), pp. 277–278, translation Soviet Mathematics Doklady , vol. 8 (1967), pp. 620–621.Google Scholar
[16] Kipnis, M. M., The constructive classification of arithmetic predicates and the semantic bases of arithmetic (Russian), Zapiski Nauchnykh Seminarov LOMI, vol. 8 (1968), pp. 53–65, translation Seminars in Mathematics. V.A.Steklov Mathematical Institute Leningrad , vol. 8 (1970), pp. 22–27.Google Scholar
[17] Kipnis, M. M., On the realizations of predicate formulas (Russian), Zapiski Nauchnykh Seminarov LOMI, vol. 20 (1971), pp. 40–48, translation Journal of Soviet Mathematics , vol. 1, (1973), pp. 22–27.Google Scholar
[18] Kleene, S. C., On the interpretation of intuitionistic number theory, The Journal of Symbolic Logic, vol. 10 (1945), pp. 109–124.Google Scholar
[19] Kleene, S. C., Introduction to metamathematics, North-Holland, 1952.Google Scholar
[20] Kolmogorov, A. N., On the tertium non datur principle (Russian), Matematicheskii sbornik, vol. 32 (1925), pp. 646–667, translation [44], pp. 414–437.Google Scholar
[21] Kolmogorov, A. N., Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift, vol. 35 (1932), pp. 58–65.Google Scholar
[22] Maksimova, L. L., Skvortsov, D. P., and Shekhtman, V. B., The impossibility of a finite axiomatization of Medvedev's logic of finitary problems (Russian), Doklady Akademii Nauk SSSR, vol. 245 (1979), pp. 1051–1054, translation Soviet Mathematics Doklady , vol. 20, pp. 394–398.Google Scholar
[23] Medvedev, Yu. T., Finite problems (Russian), Doklady Akademii Nauk SSSR, vol. 142 (1962), pp. 1015–1018, translation Soviet Mathematics Doklady , vol. 3, pp. 227–230.Google Scholar
[24] Medvedev, Yu. T., Interpretation of logical formulae by means of finite problems and its relation to the realizability theory (Russian), Doklady Akademii Nauk SSSR, vol. 148 (1963), pp. 771–774, translation Soviet Mathematics Doklady , vol. 4, pp. 180–183.Google Scholar
[25] Medvedev, Yu. T., Interpretation of logical formulae by means of finite problems (Russian), Doklady Akademii Nauk SSSR, vol. 169 (1966), pp. 20–23, translation Soviet Mathematics Doklady , vol. 7, pp. 857–860.Google Scholar
[26] Nelson, D., Recursive functions and intuitionistic number theory, Transactions of the American Mathematical Society, vol. 61 (1947), pp. 307–368.CrossRefGoogle Scholar
[27] Nishimura, I., On formulas of one variable in intuitionistic propositional calculus, The Journal of Symbolic Logic, vol. 25 (1960), pp. 327–331.Google Scholar
[28] Plisko, V. E., On realizable predicate formulae (Russian), Doklady Akademii Nauk SSSR, vol. 212 (1973), pp. 553–556, translation Soviet Mathematics Doklady , vol. 14, pp. 1420–1424.Google Scholar
[29] Plisko, V. E., A certain formal system that is connected with realizability (Russian), Teoriya algorifmov i matematicheskaya logika (Theory of algorithms and mathematical logic) (Kushner, B. A. and Nagornyi, N. M., editors), Vychislitelnyi Centr AN SSSR, 1974, pp. 148–158.Google Scholar
[30] Plisko, V. E., Recursive realizability and constructive predicate logic (Russian), Doklady Akademii Nauk SSSR, vol. 214 (1974), pp. 520–523, translation Soviet Mathematics Doklady , vol. 15, pp. 193–197.Google Scholar
[31] Plisko, V. E., Some variants of the notion of realizability for predicate formulas (Russian), Doklady Akademii Nauk SSSR, vol. 226 (1976), pp. 61–64, translation Soviet Mathematics Doklady , vol. 17, pp. 59–63.Google Scholar
[32] Plisko, V. E., The nonarithmeticity of the class of realizable predicate formulas (Russian), Izvestiya Akademii Nauk SSSR. Seriya Matematicheskaya, vol. 41 (1977), pp. 483–502, translation Mathematics of the USSR Izvestiya , vol. 11, pp. 453–471.Google Scholar
[33] Plisko, V. E., Some variants of the notion of realizability for predicate formulas (Russian), Izvestiya Akademii Nauk SSSR. Seriya Matematicheskaya, vol. 42 (1978), pp. 637–653, translation Mathematics of the USSR Izvestiya , vol. 12, pp. 588–604.Google Scholar
[34] Plisko, V. E., Absolute realizability of predicate formulas (Russian), Izvestiya Akademii Nauk SSSR. Seriya Matematicheskaya, vol. 47 (1983), pp. 315–334, translation Mathematics of the USSR Izvestiya , vol. 22, pp. 291–308.Google Scholar
[35] Plisko, V. E., The Kolmogorov calculus as a part of minimal calculus (Russian), Uspekhi Matematicheskikh Nauk, vol. 43 (1988), pp. 79–91, translation Russian Mathematical Surveys , vol. 43, pp. 95–110.Google Scholar
[36] Plisko, V. E., On arithmetic complexity of certain constructive logics, Matematicheskie Zametki, vol. 52 (1992), pp. 94–104, translation Mathematical Notes , vol. 52, pp. 701–709.Google Scholar
[37] Plisko, V. E., On the concept of relatively uniform realizability of propositional formulas (Russian), Vestnik Moskovskogo Universiteta. Seriya I. Matematika, Mekhanika, (1992), no. 2, pp. 77–79, translation Moscow University Mathematics Bulletin , vol. 47 (1992), pp. 41–42.Google Scholar
[38] Plisko, V. E., Arithmetic complexity of the predicate logics of certain complete arithmetic theories, Annals of Pure and Applied Logic, vol. 113 (2002), pp. 243–259.Google Scholar
[39] Rasiowa, H. and Sikorski, R., The mathematics of metamathematics, Polska Akademia Nauk. Monografie matematyczne, Państwowe Wydawnictwo Naukowe, Warszawa, 1963.Google Scholar
[40] Rogers, H., Theory of recursive functions and effective computability, McGraw-Hill Book Company, 1967.Google Scholar
[41] Rose, G. F., Propositional calculus and realizability, Transactions of the American Mathematical Society, vol. 75 (1953), pp. 1–19.Google Scholar
[42] Skvortsov, D. P., A comparison of the deductive power of realizable sentential formulas (Russian), Logicheskie issledovania (Logical investigations), vol. 3, Institut Filosofii RAN, 1995, pp. 38–52.Google Scholar
[43] Tseitin, G. S., The disjunctive rank of the formulas of constructive arithmetic (Russian), Zapiski Nauchnykh Seminarov LOMI, vol. 8 (1968), pp. 260–271, translation Seminars in Mathematics. V.A.Steklov Mathematical Institute Leningrad , vol. 8 (1970), pp. 126–132.Google Scholar
[44] van Heijenoort, J. (editor), From Frege to Gödel: A source book in mathematical logic, 1879-1931, Harvard University Press, Cambridge, MA, 1967.Google Scholar
[45] Varpakhovskii, F. L., On non-realizability of a disjunction of non-realizable formulas of the propositional logic (Russian), Doklady Akademii Nauk SSSR, vol. 161 (1965), pp. 1257–1258, translation Soviet Mathematics Doklady , vol. 1 (1965), pp. 568–570.Google Scholar
[46] Varpakhovskii, F. L., A class of realizable propositional formulas (Russian), Zapiski Nauchnykh Seminarov LOMI, vol. 20 (1971), pp. 8–23, translation Journal of Soviet Mathematics , vol. 1 (1973), pp. 1–11.Google Scholar
[47] Varpakhovskii, F. L., On the axiomatization of realizable propositional formulae (Russian), Doklady Akademii Nauk SSSR, vol. 314 (1990), pp. 32–36, translation Soviet Mathematics Doklady , vol. 42 (1991), pp. 260–264.Google Scholar
[48] Visser, A., Propositional logics of closed and open substitutions over Heyting Arithmetic, The Notre Dame Journal of Formal Logic, vol. 47 (2006), pp. 299–309.Google Scholar