Математическая энциклопедия - генцена формальная система

логико-математич. исчисление, служащее для формализации и исследования содержательных доказательств, оперирующих с допущениями (гипотезами). Введены Г. Генценом (G. Gentzen, |2]). Г. ф. с. делят на системы естественного вывода (или натуральные, имитирующие форму обычных математпч. умозаключении и потому особенно подходящие для формализованной записи их) и секвенциальные (или логистические, направленные на анализ возможных доказательств данной формулы, на получение результатов о нормальной форме доказательств и их использование в доказательств теории и в теории доказательства теорем на ЭВМ). Иногда Г. ф. с. отождествляют с системами секвенциального типа; тем не менее натуральные Г. ф. с. могут использовать секвенции, а секвенциальные Г. ф. с. иногда оформляют в виде исчисления формул, а не секвенций; иногда все Г. ф. с. считают натуральными, т. к. все они в той пли иной степени отражают обычные приемы оперирования с логич. связками и допущениями.

Натуральные Г. ф. с. содержат правила введения логич. символов и правила удаления символов. Логич. аксиомы немногочисленны (обычно одна две). Напр., натуральный вариант класснч. исчисления предикатов для языка задается аксиомой , правилам и введения

где bне входит в и ;правилами удаления

где произвольный терм, и структурными правилами:

(сокращение повторений), (перестановка).

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

Считается, что вхождение Vформулы в такой вывод зависит от допущения D, если Dне является аксиомой, находится на вершине вывода над V, и в ветви, ведущей от рассматриваемого вхождения Dк V, не происходит освобождения от допущения D. При истолковании такого вывода каждому вхождению формулы Ссопоставляется секвенция , где Г полный список допущений, от которых зависит рассматриваемое вхождение формулы С. Связь натуральных Г. ф. с. с обычными (гильбертовскими) вариантами соответствующих систем устанавливается с помощью утверждения: выводимо в натуральной системе тогда и только тогда, когда Свыводимо из Г с фиксированными переменными в обычной системе.

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

или другого правила близкого вида, напр, для правила . Поэтому Г. ф. с., обладающие свойством подфор-мульности, наз. также свободными от сечения или Г. ф. с. б е з сечения.