Если F выводится из G с использованием правил вывода,
вводимых ниже, тогда каждая интерпретация, при которой G истинно,
делает F также истинным; в этом смысле правила вывода "корректны".
Наоборот,
если каждая интерпретация, при которой G истинно,
делает истинным F, тогда можно вывести F из G
;
в этом смысле набор правил вывода
"полный". Взятые вместе теоремы корректности и полноты устанавливают
эквивалентность семантического и дедуктивного определения логического
следования. Теоремы корректности и полноты известны не только для логики
высказываний, но также для логики предикатов (часть 3) и для
некоторых других логических систем.
Свойство корректности безусловно должно выполняться, если мы хотим, чтобы
логическая система имела какой-либо смысл. Действительно, какой смысл в
выводе, который может вывести ложные утверждения ?
В "идеальной" логической системе должны выполняться и теорема корректности
и теорема полноты. Однако, как мы увидим, далеко не всегда можно построить
такую логическую систему. Это говорит об ограниченности возможностей
логического вывода.
Ещё одним важным свойством исчисления является
разрешимость.
Разрешимость – это возможность определить (для произвольной формулы),
выводима или нет эта формула из множества аксиом.
Свойством разрешимости обладает исчисление высказываний, но не обладает
исчисление предикатов.
Назад
|