Исчисление секвенций

Непосредственно использовать выводы в исчислении предикатов для установления логических законов крайне неудобно. Выводы даже простых формул получаются очень громоздкими и не похожи на обычные способы рассуждения, употребляемые математиками. Поэтому практически выводимость формул и секвенций устанавливается с помощью специально подобранных допустимых вспомогательных правил вывода, относящихся непосредственно к секвенциям. С их помощью можно установить выводимость секвенции, не строя для нее вывод в исчислении предикатов. Такие правила близко соответствуют обычной практике математического рассуждения, что облегчает доказательство выводимости. Набор этих правил называется техникой естественного вывода.

Ключевым фактом здесь является теорема о дедукции: если Г, А├ В, то Г├А®В. Этот факт записывается в виде вспомогательного правила вывода:

Доказательство общезначимости секвенций в исчислении предикатов, как и в исчислении высказываний, строится с использованием схемы аксиом и правил вывода. Изучение системы исчисления секвенций, названной естественной дедуктивной системой (Logische Kalkul), было начато Г. Генценом в 1934 году. В этой системе логические аксиомы формализованы, а преобразования формул не выполняются. Вместо этого используется большое число правил вывода, которые представляют собой стройную систему, подходящую для проведения обратного вывода.

Название «естественная дедуктивная система» введено для того, чтобы отличить ее от системы выводов на основе резолюций. Это основная система выводов в логике предикатов, в которой функционируют как единое целое группы правил вывода и логические аксиомы. В системе с малым числом правил вывода обычно имеется большое число логических аксиом, и наоборот. Рассмотрим систему исчисления секвенций.

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

Как и в исчислении высказываний, мы будем рассматривать кроме формул выражения вида, Г |- A, называемые секвенциями где |- - символ секвенции, Г - последовательность формул, которая может быть пустой, A - формула.