Variants of Realizability for Propositional Formulas and the Logic of Weak Excluded Middle

N. K. Vereshchagin ; D. P. Skvortsov ; E. Z. Skvortsova ; A. V. Chernov

Informatics and Automation, Mathematical logic and algebra, Tome 242 (2003), pp. 77-97.

Résumé

It is unknown whether the logic of propositional formulas that are realizable in the sense of Kleene has a finite or recursive axiomatization. In this paper, another approach to the realizability of propositional formulas is studied. This approach is based on the following informal idea: a formula is realizable if it has a “simple” realization for each substitution. More precisely, logical connectives are interpreted as operations on the sets of natural numbers, and a formula is interpreted as a combined operation; if some sets are substituted for variables, then elements of the result are called realizations. A realization (a natural number) is simple if it has low Kolmogorov complexity, and a formula is called realizable if it has at least one simple realization whatever sets are substituted. Similar definitions can be formulated in arithmetic terms. A few “realizabilities” of this kind are considered, and it is proved that all of them give the same finitely axiomatizable logic, namely, the logic of weak excluded middle. The proof uses characterizations of superintuitionistic logics with an intuitionistic positive fragment that was obtained in 1960s by Medvedev and Yankov.

Bibliographie

[1] Kolmogoroff A., “Zur Deutung der intuitionistischen Logik”, Math. Ztschr., 35:1 (1932), 58–65 | DOI | MR | Zbl

[2] Klini S. K., Vvedenie v metamatematiku, IL, M., 1957

[3] Medvedev Yu. T., “Finitnye zadachi”, DAN SSSR, 142:5 (1962), 1015–1018 | MR | Zbl

[4] Medvedev Yu. T., “Interpretatsiya logicheskikh formul posredstvom finitnykh zadach i svyaz ee s teoriei realizuemosti”, DAN SSSR, 148:4 (1963), 771–774 | MR | Zbl

[5] Medvedev Yu. T., “Ob interpretatsii logicheskikh formul posredstvom finitnykh zadach”, DAN SSSR, 169:1 (1966), 20–24

[6] Maksimova L. L., Skvortsov D. P., Shekhtman V. B., “Nevozmozhnost konechnoi aksiomatizatsii logiki finitnykh zadach Medvedeva”, DAN SSSR, 245:5 (1979), 1051–1054 | MR | Zbl

[7] Rose G. F., “Propositional calculus and realizability”, Trans. Amer. Math. Soc., 75:1 (1953), 1–19 | DOI | MR | Zbl

[8] Plisko V. E., “O realizuemykh predikatnykh formulakh”, DAN SSSR, 212:3 (1973), 553–556 | MR | Zbl

[9] Varpakhovskii F. L., “K voprosu ob aksiomatizatsii realizuemykh propozitsionalnykh formul”, DAN SSSR, 314:1 (1990), 32–36 | MR | Zbl

[10] Plisko V. E., “Absolyutnaya realizuemost predikatnykh formul”, Izv. AN SSSR. Ser. mat., 47:2 (1983), 315–334 | MR

[11] Shen A., Vereshchagin N., “Logical operations and Kolmogorov complexity”, Theor. Comput. Sci., 271 (2002), 125–129 | DOI | MR | Zbl

[12] Li M., Vitányi P., An introduction to Kolmogorov complexity and its applications, Springer, New York, 1997 | MR | Zbl

[13] Minari P., “Intermediate logics with the same disjunctionless fragment as intuitionistic logic”, Stud. Logica, 45:2 (1986), 207–222 | DOI | MR | Zbl

[14] Yankov V. A., “Ob ischislenii slabogo zakona isklyuchennogo tretego”, Izv. AN SSSR. Ser. mat., 32:5 (1968), 1044–1051

[15] Vereschagin N. K., Shen A., Yazyki i ischisleniya, MTsNMO, M., 2000

[16] Szatkowski M., “On fragments of Medvedev's logic”, Stud. Logica, 40:1 (1981), 39–54 | DOI | MR | Zbl

[17] Yankov V. A., “O svyazi mezhdu vyvodimostyu v intuitsionistskom ischislenii vyskazyvanii i konechnymi implikativnymi strukturami”, DAN SSSR, 151:6 (1963), 1293–1294 | Zbl