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

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

Натуральные Г. ф. с. содержат правила введения логич. символов и правила удаления символов. Логические аксиомы немногочисленны (обычно одна-две). Рассмотрим, напр., задание классического исчисления предикатов в виде натуральной Г. ф. с. Формулы строят обычным образом с помощью связок Выводимые объекты — односукцедентные секвенции. Аксиомы: .

Правила введения:

Правила удаления:

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

Здесь t — произвольный терм; означает, что переменная b не входит в .

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

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

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

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

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

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

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

Теорема об устранимости сечения позволяет устанавливать разрешимость бескванторных систем: из подформул данной бескванторной ф-лы можно составить лишь конечное число несходных секвенций (секвенции сходны, если они отличаются лишь порядком и повторениями членов в антецеденте и сукцеденте), из которых, в свою очередь, можно составить лишь конечное число «кандидатов» в выводы; данная ф-ла доказуема, если среди этих кандидатов найдется вывод. В действительности, при поиске вывода применяется более эффективный алгоритм поиска «снизу вверх» путем анализа испытуемой на выводимость секвенции S: производятся «контрприменения» правил: над S надписываются секвенции (или пары секвенций), из которых S могла бы получиться однократным применением правила вывода (из-за свойства подформульности и отсутствия кванторов получается конечный список); к каждой из порожденных таким образом секвенций снова применяется тот же прием и т. д. После конечного числа шагов либо получится вывод (на вершинах всех «ветвей» окажутся аксиомы), либо произойдет обрыв процесса (зацикливание) — тогда формула невыводима.

Для кванторных систем эта схема модифицируется: на каждом этапе «анализа» при контрприменениях кванторных правил перебирается лишь конечный список возможных термов; процесс в целом организуется таким образом, что каждый из возможных термов

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

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

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

Лит.: Клини С. К. Математическая логика. Пер. с англ. М., 1973 [библиогр. с. 451—465]; Математическая теория логического вывода. М., 1967; Карри X. Б. Основания математической логики. Пер. с англ. М., 1969 [библиогр. с. 518—547]. Г. Е. Минц.