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/97418h.htm
Изменения вносились 27 января 2000