Документ взят из кэша поисковой машины. Адрес оригинального документа : http://www.mccme.ru/lifr/clkr2012/absyavorskaya.pdf Дата изменения: Wed May 23 17:44:38 2012 Дата индексирования: Tue Oct 2 13:47:27 2012 Кодировка: Windows-1251 Поисковые слова: star

Логика доказательств первого порядка
Т.Л. Яворская

В докладе будет рассказано о первопорядковом расширении логики доказательств

LP

. Логика доказательств первого порядка

F OLP

(С. Артемов,

Т. Яворская, 2011) позволяет построить явную реализацию первопорядковой модальной логики

F OS 4

и, следовательно, интуиционистской логики. Мы

опишем доказуемостную интерпретацию о реализуемости, корректность

F OS 4

в терминах арифметических

выводов с параметрами и некоторые ее обобщения. Совместно с результатом

F OLP

относительно такой интерпретации

позволяет определить точную доказуемостную семантику, удовлетворяющую требованиям Брауэра-Гейтинга-Колмогорова, для нистской логики первого порядка.

F OS 4

и интуицио-

1