On some properties of systems, complete with respect to expressibility, of formulas in the Gödel–Löb provability logic

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.