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.