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