О некоторых свойствах полных по выразимости систем формул в логике доказуемости Геделя–Леба

Хорошо известны идеи о погружении интуиционистской логики в модальную логику с целью последующей интерпретации модальности доказуемо как выводимость в арифметике Пеано, а также возникающие при этом трудности. Р. М. Соловей и А. В. Кузнецов ввели в рассмотрение логику доказуемости Геделя–Леба, формулы которой построены из пропозициональных переменных с помощью связок $\&$, $\vee$, $\supset$, $\neg$ и $\Delta$ (геделизированная доказуемость). Логика эта определена классическим исчислением высказываний, обогащенным тремя $\Delta$-аксиомами
$$ \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, $$
а также правилом усиления (правило Геделя). Формула называется (функционально) выразимой в логике $L$ через систему формул $\Sigma$, если ее можно получить из $\Sigma$ и переменных посредством ослабленного правила подстановки и правила замены эквивалентным в $L$. Понятия полноты и предполноты (по выразимости) в логике определяются традиционным образом. Система $\Sigma$ называется формульным базисом в логике $L$, если $\Sigma$ полна и независима в $L$. В статье доказано, что в логике доказуемости Геделя–Леба и ряде ее расширений существует счетное семейство предполных классов формул, существуют формульные базисы любой конечной длины и отсутствует финитная аппроксимируемость по полноте.