ГЕНЦЕНА ФОРМАЛЬНАЯ СИСТЕМА это:

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

логико-математич. исчисление, служащее для формализации и исследования содержательных доказательств, оперирующих с допущениями (гипотезами). Введены Г. Генценом (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.

Г. Е. Минц.


Математическая энциклопедия. — М.: Советская энциклопедия. . 1977—1985.

Смотреть что такое "ГЕНЦЕНА ФОРМАЛЬНАЯ СИСТЕМА" в других словарях:

  • ГЕЙТИНГА ФОРМАЛЬНАЯ СИСТЕМА — Гейтипга исчисление, название трех формальных систем конструктивной логики, предложенных А. Рейтингом [1]. Первая из них гейтинговское, или интуиционистское, исчисление высказываний формализация принципов конструктивной логики высказываний;… …   Математическая энциклопедия

  • АРИФМЕТИКА ФОРМАЛЬНАЯ — арифметическое исчисление, логико математич. исчисление, формализующее элементарную теорию чисел. Язык наиболее употребительного варианта А. ф. содержит константу 0, числовые переменные, символ равенства, функциональные символы (прибавление 1) и… …   Математическая энциклопедия

  • НЕПРОТИВОРЕЧИВОСТЬ — свойство формальной системы, состоящее в том, что не каждая формула этой системы доказуема в ней. Формальные системы, обладающие этим свойством, наз. непротиворечивым и, или формально непротиворечивым и. В противном случае формальная система наз …   Математическая энциклопедия

  • КОНСТРУКТИВНАЯ ЛОГИКА — раздел математической логики, изучающий рассуждения о конструктивных объектах и конструкциях. При таком понимании К. л. шире, чем логика конструктивной математики. Самое заметное отличие от традиционной (классической) логики состоит в отсутствии… …   Математическая энциклопедия

  • ГЁДЕЛЯ ТЕОРЕМА О ПОЛНОТЕ — утверждение о полноте классического исчисления предикатов: всякая предикатная формула, истинная на всех моделях, выводима (по формальным правилам классич. исчисления предикатов). Г. т. о п. показывает, что множество выводимых формул этого… …   Математическая энциклопедия

  • ДОПУСТИМОЕ ПРАВИЛО — вывода правило, добавление к рого в исчисление не меняет объема выводимых в этом исчислении слов. Введение в исчисление Д. п. является мощным и часто применяемым средством сокращения выводов, во многих случаях полезно для совершенствования… …   Математическая энциклопедия

  • ЕСТЕСТВЕННЫЙ ЛОГИЧЕСКИЙ ВЫВОД — формальный вывод, по возмвжности приближенный к содержательному рассуждению, привычному для математика и логика. Критерии естественности и качества вывода не уточняются полностью, но обычно имеются в виду выводы, осуществляемые по… …   Математическая энциклопедия

  • ПОДФОРМУЛЬНОСТИ СВОЙСТВО — свойство нек рых логических исчислений и логико математических исчислений, заключающееся в том, что посылки каждого правила исчисления состоят из подформул заключения. П. с. позволяет организовать поиск вывода снизу вверх (см. Генцена формальная… …   Математическая энциклопедия

  • СЕМИОТИКА — (от греч. semeiot знак) общая теория знаковых систем, изучающая свойства знаковых комплексов самой различной природы. К таким системам относятся естественные языки, письменные и устные, разнообразные искусственные языки, начиная с формализованных …   Философская энциклопедия


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»