Поиск в словарях
Искать во всех

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

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

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

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

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

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

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

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

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

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

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

Рейтинг статьи:
Комментарии:

Вопрос-ответ:

Что такое генцена формальная система
Значение слова генцена формальная система
Что означает генцена формальная система
Толкование слова генцена формальная система
Определение термина генцена формальная система
gencena formalnaya sistema это
Ссылка для сайта или блога:
Ссылка для форума (bb-код):