Логика доказуемости с операциями над доказательствами

Найдена естественная аксиоматизация пропозициональной логики с модальным оператором формальной доказуемости (Соловей, [5]) и помеченными модальностями для индивидуальных доказательств с операциями над ними (Артемов, [2]). При этом возникает необходимость ввести в язык две новые операции. Полученная система $\mathcal{MLP}$ естественно включает в себя как логику доказуемости Соловея GL, так и операторную логику доказательств Артемова $\mathcal{LP}$. Доказана разрешимость, арифметическая и функциональная полнота конечных расширений базисного фрагмента системы $\mathcal{MLP}$.