Методологический семинар ИСИ СО РАН. Заседание от 30.01.2024

Докладчик: д.ф.-м.н. Сергей Павлович Одинцов, Институт математики им. С.Л. Соболева СО РАН

Тема доклада: Верификация, фальсификация, сильное отрицание, FDE.

Цель доклада - проследить, как логики осознали, что верификация и
фальсификация - это несводимые друг к другу понятия, и как данное
обстоятельство дало начало интересному семейству логических формализмов, популярных как у специалистов по искусственному интеллекту, так и у философских логиков. Мы рассмотрим ВНК-интерпретацию интуиционистской логики, которая основана на задачной семантике Колмогорова и ее формализации, известной как реализуемость по Клини.

Неудовлетворительные конструктивные свойства интуиционистской логики привели к появлению модификации семантики реализуемости, предложенной Дэвидом Нельсоном, учеником Клини, и основанной на двух конструктивных процедурах проверки истинности и ложности арифметических суждений. Отрицание системы Нельсона служило для перехода от одной процедуры к другой. Независимо от Нельсона и с совершенно иной мотивацией Н. Белнап предложил логику, в которой фальсифицируемость атомного утверждения совершенно независима от его верифицируемости. В докладе мы проследим связи системы
Белнапа FDE с логикой Нельсона и релевантной логикой R.