Akademik

    ЭЛИМИНАЦИОННАЯ ТЕОРЕМА — фундаментальная теорема доказательств теории. Термин “элиминационная теорема” введен X. Карри в качестве альтернативного названия теоремы об устранении сечения, которая впервые была сформулирована и доказана Г. Генценом в виде “Основной теоремы” (Hauptsatz) для исчисления секвенций классической и интуиционистской логики предикатов в работе “Исследования логических выводов” (1934). Согласно этой теореме, любой вывод в классическом или интуиционистском исчислении секвенций можно преобразовать в вьюод с той же конечной секвенцией, не содержащий применений правила сечения. Идейно устранение сечения связано со следующей характерной особенностью секвенциальных исчислений. Все правила вывода (кроме сечения) действуют так, что любая формула, использованная в дереве вывода, оказывается подформулой формулы, входящей в результат вывода (конечную секвенцию). Поэтому уже по структуре формул данной секвенции, фактически, можно определить, что необходимо использовать для получения ее вывода. Наличие сечения ликвидирует такую возможность, т. к. при применениях этого правила из вывода исчезают формулы, входящие в обе посылки сечения. Доказательство элиминационной теоремы заключается в демонстрации эффективной процедуры преобразования произвольного исходного вывода (с применениями сечения) в результирующий вывод (без применений сечения). Естественно, исходный и результирующий выводы строятся в одном и том же исчислении и заканчиваются одной и той же секвенцией. В классическом варианте доказательства Генцена ключевую роль играет т. неосновная лемма”, согласно которой из исходного вывода всегда можно устранить применения правила смешения. Поскольку сечение является частным случаем смешения, из основной леммы следует, что применения сечения устранимы.

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

    Формальное доказательство основной леммы состоит из рассмотрения большого числа отдельных случаев и подслучаев. Содержательно оно базируется на перестановочности правил заключения в секвенциальном выводе. Суть редукций в том, что единственное применение смешения “перемещается” вверх по дереву вывода — переставляется с предшествующими применениями других правил заключения до тех пор, пока не становится очевидным, что его вообще можно удалить из вывода.

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

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

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

    Лит.: Генцен Г. Исследования логических выводов.— В кн.: Математическая теория логического вывода. М., 1967.

    П. И. Быстрое