ГЕНЦЕНА ФОРМАЛЬНАЯ СИСТЕМА

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

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

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

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

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

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

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

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

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

Пример. Свободный от сечения вариант классич. исчисления предикатов LK. Выводимые объекты - произвольные секвенции, составленные из формул. Аксиома .

Сукцедентные правила:

где b не входит в и

Антецедентные правила:

Структурные правила: сечение, перестановка, утончение и сокращение повторений в антецеденте и сукцеденте (см. Секвенция).

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

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

Важным обобщением Г. ф. с. являются полуформальные системы, содержащие правила с бесконечным множеством посылок, напр, правило бесконечной индукции ( -правило):

Лит.:[1]Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [2] Генцен Г., в кн.: Математическая теория логического вывода, Сб. переводов, М., 1967, с. а-76; [3] Карри X. Б., Основания математической логики, пер. с англ., М., 1969; [4] Рrawitz D., Ideas and results in proof theory, в кн.: Proc. 2 Scand. logic symposium, Amst.- L., 1971.

Г. Е. Минц.