Генцена формальная система

логико-математич. исчисление, служащее для формализации и исследования содержательных доказательств, оперирующих с допущениями (гипотезами). Введены Г. Генценом (G. Gentzen, |2]). Г. ф. с. делят на системы естественного вывода (или натуральные, имитирующие форму обычных математпч. умозаключении и потому особенно подходящие для формализованной записи их) и секвенциальные (или логистические, направленные на анализ возможных доказательств данной формулы, на получение результатов о нормальной форме доказательств и их использование в доказательств теории и в теории доказательства теорем на ЭВМ). Иногда Г. ф. с. отождествляют с системами секвенциального типа; тем не менее натуральные Г. ф. с. могут использовать секвенции, а секвенциальные Г. ф. с. иногда оформляют в виде исчисления формул, а не секвенций; иногда все Г. ф. с. считают натуральными, т. к. все они в той пли иной степени отражают обычные приемы оперирования с логич. связками и допущениями. Натуральные Г. ф. с. содержат правила введения логич. символов и правила удаления символов. Логич. аксиомы немногочисленны (обычно одна - две). Напр., натуральный вариант класснч. исчисления предикатов для языка [img: http://localhost:8080/file/010409-232.jpg] задается аксиомой [img: http://localhost:8080/file/010409-233.jpg], правилам и введения [img: http://localhost:8080/file/010409-234.jpg] где bне входит в [img: http://localhost:8080/file/010409-235.jpg] и [img: http://localhost:8080/file/010409-236.jpg];правилами удаления [img: http://localhost:8080/file/010409-237.jpg] где [img: http://localhost:8080/file/010409-238.jpg] - произвольный терм, и структурными правилами: [img: http://localhost:8080/file/010409-239.jpg] [img: http://localhost:8080/file/010409-240.jpg] (сокращение повторений), [img: http://localhost:8080/file/010409-241.jpg] (перестановка). Секвенция, находящаяся под чертой, наз. заключением правила, а секвенции, находящиеся над чертой,- посылками. Аксиома [img: http://localhost:8080/file/010409-242.jpg] изображает введение допущения [img: http://localhost:8080/file/010409-243.jpg]; правило [img: http://localhost:8080/file/010409-244.jpg] иллюстрирует освобождение от допущения: формула Вверхней секвенции зависит от допущения А, формула [img: http://localhost:8080/file/010409-245.jpg] нижней секвенции уже не зависит от А. Г. ф. с. натурального типа задается иногда в виде исчисления формул (а не секвенций) с неявной записью зависимости от допущений: вывод в таком исчислении - это древовидный граф, в вершинах к-рого могут находиться произвольные формулы (не обязательно аксиомы), а все переходы производятся по правилам вывода. Эти правила получаются вычеркиванием антецедентов из соответствующих правил натуральной системы, описанной с помощью секвенций, причем в случае, когда происходит освобождение от допущений, добавляются соответствующие условия, напр. [img: http://localhost:8080/file/010409-246.jpg] Считается, что вхождение Vформулы в такой вывод зависит от допущения D, если Dне является аксиомой, находится на вершине вывода над V, и в ветви, ведущей от рассматриваемого вхождения Dк V, не происходит освобождения от допущения D. При истолковании такого вывода каждому вхождению формулы Ссопоставляется секвенция [img: http://localhost:8080/file/010409-247.jpg], где Г - полный список допущений, от которых зависит рассматриваемое вхождение формулы С. Связь натуральных Г. ф. с. с обычными (гильбертовскими) вариантами соответствующих систем устанавливается с помощью утверждения: [img: http://localhost:8080/file/010409-248.jpg] выводимо в натуральной системе тогда и только тогда, когда Свыводимо из Г с фиксированными переменными в обычной системе. Натуральные Г. ф. с. в их первоначальной форме плохо приспособлены для поиска вывода путем анализа: при попытке выяснить, по какому правилу из ка-'ких посылок могла получиться данная формула (секвенция), возникает неоднозначность - в принципе это может быть правило введения соответствующей логич. связки или любое из правил удаления. При этом множество возможных посылок в правилах удаления потенциально неограничено (за счет варьирования формулы Ав правиле [img: http://localhost:8080/file/010409-249.jpg]). Поэтому полезно иметь правила, обладающие свойством подформульности: в посылки входят только подформулы заключения, а бесконечность проявляется лишь за счет варьирования вида термов в правилах типа [img: http://localhost:8080/file/010409-250.jpg] В секвенциальных Г. ф. с. либо все правила обладают свойством подформульностн, либо это свойство нарушается лишь для одного правила - правила сечения: [img: http://localhost:8080/file/010409-251.jpg] или другого правила близкого вида, напр, для правила [img: http://localhost:8080/file/010409-252.jpg]. Поэтому Г. ф. с., обладающие свойством подфор-мульности, наз. также свободными от сечения или Г. ф. с. б е з сечения. Пример. Свободный от сечения вариант классич. исчисления предикатов LK. Выводимые объекты - произвольные секвенции, составленные из [img: http://localhost:8080/file/010409-253.jpg] формул. Аксиома [img: http://localhost:8080/file/010409-254.jpg]. Сукцедентные правила: [img: http://localhost:8080/file/010410-1.jpg] где b не входит в [img: http://localhost:8080/file/010410-2.jpg] и [img: http://localhost:8080/file/010410-3.jpg] Антецедентные правила: [img: http://localhost:8080/file/010410-4.jpg] Структурные правила: сечение, перестановка, утончение и сокращение повторений в антецеденте и сукцеденте (см. Секвенция). При сравнении секвенциальных и натуральных Г. ф. с. правилам введения соответствуют сукцедент-ные правила, правилам удаления - антецедентные правила. При моделировании в секвенциальных Г. ф. с. правил удаления используется сечение. Свойство под-формульности для LK обеспечивает основная теорема Генцена (теорема об устранимости сечения): по всякому выводу в LK можно построить вывод (той же секвенции) без сечения. Эта теорема позволяет устанавливать разрешимость бескванторных систем: из подформул данной бескванторной формулы можно составить лишь конечное число несходных секвенций (секвенции сходны, если они отличаются лишь порядком и повторениями членов в антецеденте и сукцеденте), из к-рых, в свою очередь, можно составить лишь конечное число "кандидатов" в выводы; данная формула доказуема, если среди этих кандидатов найдется вывод. Г. ф. с. позволяют отражать содержательные особенности теории с помощью чисто структурных соображений; так, Г. ф. с. конструктивной математики часто отличаются от соответствующих классич. систем лишь использованием односукцедентных секвенций вместо произвольных. В свободных от сечения системах легко доказывается непротиворечивость (т. е. невыводимость пустой секвенции), а также выводимость одного из дизъюнктивных членов выводимой дизъюнкции. Важным обобщением Г. ф. с. являются полуформальные системы, содержащие правила с бесконечным множеством посылок, напр, правило бесконечной индукции ([img: http://localhost:8080/file/010410-5.jpg] -правило): [img: http://localhost:8080/file/010410-6.jpg]