On some properties of systems, complete with respect to expressibility, of formulas in the G\"odel--L\"ob provability logic

M. F. Raţă ; A. G. Russu

Diskretnaya Matematika, Tome 12 (2000) no. 4, pp. 63-82.

Résumé

The ideas of embedding the intuitionistic logic into the modal logic and the following interpretation of the modality as a provable deducibility in the Peano arithmetic and also difficulties arising here are well known. R. M. Solovay and A. V. Kuznetsov introduced a Gödel–Löb provability logic in which formulas consist of propositional variables and the connectives $\$, $\vee$, $\supset$, $\neg$, and $\Delta$ (the Gödelized provability). This logic is defined by the classical propositional calculus together with 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 also the strengthening rule (the Gödel rule). A formula is called (functionally) expressible in a logic $L$ over a system of formulas $\Sigma$ if it can be obtained from $\Sigma$ and variables by the weakened substitution rule and by the replacement by an equivalent in $L$ rule. The notions of completeness and precompleteness (by expressibility) are defined in a logic in the traditional way. A system $\Sigma$ is called a formular basis in a logic $L$ if $\Sigma$ is complete and independent in $L$. In the article, it is proved that in the Gödel–Löb provability logic and in a series of its extensions there exists a countable family of precomplete classes of formulas, there exist formular bases of any finite length, and there is no finite approximability by completeness.

Bibliographie

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

[2] Kuznetsov A. V., “O problemakh tozhdestva i funktsionalnoi polnoty dlya algebraicheskikh sistem”, Trudy Tretego Vsesoyuznogo matematicheskogo s'ezda, t. 2, Moskva, 1956, 145–146

[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”, Matematicheskie issledovaniya, 6:4 (1971), 75–122 | MR | Zbl

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

[6] Kuznetsov A. V., Ratsa M. F., “Kriterii funktsionalnoi polnoty v klassicheskoi logike predikatov pervogo poryadka”, Dokl. AN SSSR, 249:3 (1979), 540–544 | MR | Zbl

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

[8] Maltsev A. I., Algoritmy i rekursivnye funktsii, Nauka, Moskva, 1965 | MR

[9] Maltsev A. I., Iterativnye algebry Posta, Izd-vo NGU, Novosibirsk, 1976 | MR

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

[11] Ratsa M. F., “Netablichnost logiki $S4$ po funktsionalnoi polnote”, Algebra i logika, 21:3 (1982), 283–320 | MR | Zbl

[12] Ratsa M. F., “O funktsionalnoi polnote v modalnoi logike $S5$”, Issledovaniya po neklassicheskim logikam i formalnym sistemam, Nauka, Moskva, 1983, 222–280 | MR

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

[14] Russu A. G., “O moschnosti formulnykh bazisov i otsutstvii finitnoi approksimiruemosti po polnote v propozitsionalnoi logike dokazuemosti”, Izv. Akad. Nauk Respub. Moldova Mat., 1992, no. 2(8), 6–14 | MR | Zbl

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

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

[17] Chërch A., Vvedenie v matematicheskuyu logiku, IL, Moskva, 1960

[18] Yablonskii S. V., “Funktsionalnye postroeniya v $k$-znachnoi logike”, Trudy Matem. in-ta im. V. A. Steklova, 51, 1958, 5–142 | Zbl

[19] Yablonskii S. V., Vvedenie v diskretnuyu matematiku, Nauka, Moskva, 1986 | MR

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

[21] Boolos G. S., Jeffrey R. C., Computability and logic, 1989, Cambridge Univ. Press, Cambridge | MR

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

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

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

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

[26] Post E. L., “Introduction to a general theory of elementary propositions”, Amer. J. Math., 43 (1921), 163–185 | DOI | MR | Zbl

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

[28] Raseva E., Sikorskii R., Matematika metamatematiki, Nauka, Moskva, 1972 | MR

[29] Rosenberg I., “La structure des functions de plusieure variables sur un ensemble finit”, C. R. Acad. Sci., 260 (1965), 2817–2819 | MR

[30] Segerberg K., An essay in classical modal logic, Philosofiska Studier, Uppsala, 1971 | MR

[31] Smorinski C., Self-reference and modal logic., Springer, Berlin, 1985 | MR

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