FPM 1997, ТОМ 3, ВЫПУСК 4, СТР. 1173-1197

ФУНДАМЕНТАЛЬНАЯ И ПРИКЛАДНАЯ МАТЕМАТИКА
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