О корректности, полноте и разрешимости

Если F выводится из G с использованием правил вывода, вводимых ниже, тогда каждая интерпретация, при которой G истинно, делает F также истинным ^*; в этом смысле правила вывода ``корректны''. ^* Наоборот, если каждая интерпретация, при которой G истинно, делает истинным F, тогда можно вывести F из G ^*; в этом смысле набор правил вывода ``полный''. Взятые вместе теоремы корректности и полноты устанавливают эквивалентность семантического и дедуктивного определения логического следования. Теоремы корректности и полноты известны не только для логики высказываний, но также для логики предикатов (часть 3) и для некоторых других логических систем.

Свойство корректности безусловно должно выполняться, если мы хотим, чтобы логическая система имела какой-либо смысл. Действительно, какой смысл в выводе, который может вывести ложные утверждения ? В ``идеальной'' логической системе должны выполняться и теорема корректности и теорема полноты. Однако, как мы увидим, далеко не всегда можно построить такую логическую систему. Это говорит об ограниченности возможностей логического вывода.

Ещё одним важным свойством исчисления является разрешимость. Разрешимость – это возможность определить (для произвольной формулы), выводима или нет эта формула из множества аксиом. Свойством разрешимости обладает исчисление высказываний, но не обладает исчисление предикатов.