A formal reduction of the general problem of the expressibility of formulas in the G\"odel-L\"ob provability logic

M. F. Raţă

Diskretnaya Matematika, Tome 14 (2002) no. 2, pp. 95-106.

Résumé

It is a well-known idea to embed the intuitionistic logic into the modal logic in order to interprete the modality ‘provable’ as the deducibility in the Peano arithmetics with also well-known difficulties. P. M. Solovay and A. V. Kuznetsov introduced into consideration the Gödel–Löb provability logic whose formulas are constructed from propositional variables with the use of the connectives $\$, $\vee$, $\supset$, $\neg$, and $\Delta$ (Gödelised provability). This logic is defined by the classic propositional calculus complemented by the three $\Delta$-axioms $$ \Delta(p\supset q)\supset(\Delta p\supset\Delta q),\quad \Delta(\Delta p\supset p)\supset\Delta p,\quad \Delta p\supset\Delta\Delta p, $$ and the extension rule (the Gödel rule). A formula $F$ is called (functionally) expressible in terms of a system of formulas $\Sigma$ in logic $L$ if, on the base of $\Sigma$ and variables, it is possible to obtain $F$ with the use of the weakened substitution rule and the rule of change by equivalent in $L$. The general problem of expressibility in a logic $L$ requires to give an algorithm which for any formula $F$ and any finite system of formulas $\Sigma$ recognises whether $F$ is expressible in terms of $\Sigma$ in $L$. In this paper, it is proved that in the Gödel–Löb provability logic and in many of extensions of this logic there is no algorithm which recognises the expressibility. In other words, the general expressibility problem is algorithmically undecidable in these logics.

Bibliographie

[1] Artemov S. N., “O modalnykh logikakh, aksiomatiziruyuschikh dokazuemost”, Izv. AN SSSR, Ser. matem., 49:6 (1985), 1123–1154 | MR | Zbl

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

[3] Kuznetsov A. V., “Analogi “shtrikha Sheffera” v konstruktivnoi logike”, Dokl. AN SSSR, 160:2 (1965), 274–277 | Zbl

[4] Kuznetsov A. V., “O funktsionalnoi vyrazimosti v superintuitsionistskikh logikakh”, Matem. issledovaniya, 6:4 (1971), 75–122 | MR | Zbl

[5] Kuznetsov A. V., “O sredstvakh dlya obnaruzheniya nevyvodimosti ili nevyrazimosti”, Logicheskii vyvod, Nauka, Moskva, 1979, 5–33

[6] Kuznetsov A. V., Muravitskii A. Yu., “Dokazuemost kak modalnost”, Aktualnye problemy logiki i metodologii nauki, Naukova Dumka, Kiev, 1980, 193–230

[7] Maksimova L. L., “Predtablichnye rasshireniya logiki $S4$ Lyuisa”, Algebra i logika, 14:1 (1975), 28–55 | MR | Zbl

[8] Maksimova L. L., “Modalnye logiki konechnykh sloev”, Algebra i logika, 14:3 (1975), 304–314 | MR

[9] Maksimova L. L., “Kontinuum normalnykh rasshirenii modalnoi logiki dokazuemosti s interpolyatsionnym svoistvom Kreiga”, Sib. matem. zh., 30:6 (1989), 122–131 | MR | Zbl

[10] Maksimova L. L., Rybakov V. V., “O reshetke normalnykh modalnykh logik”, Algebra i logika, 13:2 (1974), 188–216 | MR | Zbl

[11] Maltsev A. I., Algoritmy i rekursivnye funktsii, Nauka, Moskva, 1986 | MR

[12] Novikov P. S., Konstruktivnaya matematicheskaya logika s tochki zreniya klassicheskoi, Nauka, Moskva, 1977 | MR

[13] Rasëva E., Sikorskii R., Matematika metamatematiki, 1972, Nauka, Moskva | MR

[14] Ratsa M. F., “O funktsionalnoi polnote v intuitsionistskoi logike vyskazyvanii”, Probl. kibern., 39 (1982), 107–150 | MR | Zbl

[15] Ratsa M. F., “Nerazreshimost problemy funktsionalnoi vyrazimosti v modalnoi logike $S4$”, Dokl. AN SSSR, 268:4 (1983), 814–817 | MR | Zbl

[16] Ratsa M. F., “Algoritmicheskaya nerazreshimost problemy vyrazimosti v modalnykh logikakh”, Matem. probl. kibern., 2 (1989), 71–99 | MR | Zbl

[17] Ratsa M. F., Vyrazimost v ischisleniyakh vyskazyvanii, Shtiintsa, Kishinev, 1991 | MR | Zbl

[18] Feis R., Modalnaya logika, 1974, Nauka, Moskva | MR

[19] Chagrov A. V., “Netablichnost–predtablichnost, antitablichnost, ko-antitablichnost”, Algebro-logicheskie konstruktsii, Kalinin, 1989, 105–111 | Zbl

[20] Cherch A., Vvedenie v matematicheskuyu logiku, IL, Moskva, 1960

[21] Esakiya L. L., “O mnogoobraziyakh algebr Grzhegorchika”, Issledovaniya po neklassicheskim logikam i teorii mnozhestv, Nauka, Moskva, 1979, 257–287

[22] Yablonskii S. V., Gavrilov G. P., Kudryavtsev V. B., Funktsii algebry logiki i klassy Posta, Nauka, Moskva, 1974

[23] Yanov Yu. I., Muchnik A. A., “O suschestvovanii $k$-znachnykh zamknutykh klassov, ne imeyuschikh konechnogo bazisa”, Dokl. AN SSSR, 127:1 (1959), 44–46 | Zbl

[24] Bernardi C., “On the equational class of diagonalizable algebras”, Studia Logica, 34:4 (1975), 321–331 | DOI | MR

[25] Bernardi C., “Modal diagonalizable algebras”, Boll. Unione Matem. Italiana, 15-B:1 (1979), 15–30 | MR

[26] Blok W. J., “Pretabular varieties of modal algebras”, Studia Logica, 39:2–3 (1980), 101–124 | DOI | MR | Zbl

[27] Boolos G. S., Jeffrey R. C., Computability and Logic, Cambridge Univ. Press, Cambridge, 1989 | MR | Zbl

[28] Grzegorezyc A., “Some relational systems and the associated topological spaces”, Fund. Math., 1967, no. 60, 223–231 | MR

[29] Gödel K., “Eine interpretation des intuitionistischen aussagen kalkulus”, Ergebnisse Math. Koll., 1933, no. 4, 39–40 | Zbl

[30] Jaśkowski R., Part VI, Actes du Congrès Intern. de Philosophie Scientifique, Paris, 1936 | Zbl

[31] Kolmogoroff A., “Zur Deutung der intuitionistichen Logik”, Math. Z., 35 (1932), 58–61 | DOI | MR

[32] Löb M., “Solution of a problem of Leon Henkin”, J. Symb. Logic, 20:2 (1955), 115–118 | DOI | MR | Zbl

[33] Magari R., “The diagonalizable algebras”, Boll. Unione Matem. Italiana, 12 (1975), 117–125 | MR | Zbl

[34] Makinson D. C., “There are infinitely many Diodorean modal functions”, J. Symb. Logic, 31:3 (1966), 406–408 | DOI | MR | Zbl

[35] McKinsey J. C. C, Tarski A., “Some theorems about the sentential calculi of Lewis and Heyting”, J. Symb. Logic, 13 (1948), 1–15 | DOI | MR | Zbl

[36] Post E. L., Two-valued iterative systems of mathematical logic, Princeton Univ. Press, Princeton, 1941 | MR | Zbl

[37] Schumm G. F., “On modal system of D. Makinson and B. Sobocinski”, Notre Dame J. Form. Logic, 10:3 (1969), 263–265 | DOI | MR | Zbl

[38] Segerberg K., Theoria, 36, no. 3, 1970 | MR

[39] Segerberg K., Theoria, 36, 1970 | MR

[40] Sobocinski B., “Certain extensions of modal systems $S4$”, Notre Dame J. Form. Logic, 11:3 (1970), 347–368 | DOI | MR | Zbl

[41] Solovay R. M., “Provability interpretations of modal logic”, Israel J. Math., 25:3–4 (1975), 287–304 | MR

[42] Tarski A., “Der Aussagenkalkül und die Topologie”, Fund. Math., 31 (1938), 103–134 | Zbl