|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
Погружение модального λ-исчисления в логику доказательствстатья
Статья опубликована в журнале из списка RSCI Web of Science
Статья опубликована в журнале из перечня ВАК- Автор: Артемов С.Н.
- Журнал: Труды Математического института им.В.А.Стеклова РАН
- Том: 242
- Год издания: 2003
- Издательство: МИАН
- Местоположение издательства: Москва
- Первая страница: 44
- Последняя страница: 58
- Аннотация: Система логики доказательств LP, введенная автором, восходит к доказуемостному исчислению Гёделя, известному также под именем модальной логики S4, которому была посвящена монография П. С. Новикова “Конструктивная математическая логика с точки зрения классической” LP дает точный математический ответ на вопрос о доказуемостной семантике S4, поставленный Гёделем. В настоящей работе проводится сравнение выразительной силы LP, типового λ-исчисления и модального λ-исчисления. Показано, что малый (а именно хорновский) фрагмент LP достаточен для естественного погружения типового λ-исчисления. Показано, что сама LP моделирует модальное λ-исчисление.
- Добавил в систему: Золин Евгений Евгеньевич