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

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