ФУНДАМЕНТАЛЬНАЯ И ПРИКЛАДНАЯ МАТЕМАТИКА
1997, ТОМ 3, ВЫПУСК 4, СТР. 1173-1197

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

Т. Л. Сидон

Аннотация

Посмотреть как HTML    Посмотреть как рисунок    Посмотреть в формате LaTeX

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

Постскрипт статьи (84 Kb)

Главная страница Содержание журнала Новости Поиск

URL страницы: http://mech.math.msu.su/~fpm/rus/97/974/97418t.htm
Изменения вносились 27 января 2000