ЕЛИМИНИРАЩА ТЕОРЕМА

ЕЛИМИНИРАЩА ТЕОРЕМА– основната теорема отдоказателствата на теорията. Терминът „теорема за елиминиране“ е въведен от X. Curry като алтернативно име за теоремата за елиминиране на изрязване, която за първи път е формулирана и доказана отG. Genzenпод формата на „Основна теорема“ (Hauptsatz) заизчислението на последователноститена класическата и интуиционистка логика на предикатите в работата „Изследвания в In справка“ (1934). Съгласно тази теорема всяко извеждане в класическото или интуиционистичното секвенционно смятане може да се трансформира в извеждане със същата крайна последователност, която не съдържа приложения на правилото за изрязване.

Концептуално елиминирането на среза е свързано със следната характерна черта на последователните изчисления. Всички правила за извод (с изключение на cut) работят по такъв начин, че всяка формула, използвана в дървото на извода, се оказва подформула на формулата, включена в резултата от извода (крайна последователност). Следователно, вече чрез структурата на формулите на тази последователност, всъщност е възможно да се определи какво трябва да се използва, за да се получи нейното заключение. Наличието на раздел елиминира тази възможност, тъй като когато се прилага това правило, формулите, които се появяват в двете помещения на раздела, изчезват от извеждането.

Доказателството на теоремата за елиминиране се състои в демонстриране на ефективна процедура за трансформиране на произволен първоначален изход (с изрязани приложения) в резултатния изход (без изрязани приложения). Естествено, първоначалните и произтичащите изводи са построени в едно и също смятане и завършват с една и съща секвенция. В класическата версия на доказателството на Генцен ключова роля играе т.нар "главна лема", според която винаги е възможно да се елиминира приложението на правилото от първоначалното заключениесмесване. Тъй като срезът е частен случай на смесване, от основната лема следва, че приложенията на среза са отстраними.

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

Формалното доказателство на основната лема се състои в разглеждане на голям брой отделни случаи и подслучаи. По отношение на съдържанието се основава на пермутацията на правилата за извод в последователния извод. Същността на редукциите е, че едно приложение на смесване се "движи" нагоре по дървото на извеждане - разменя се с предишни приложения на други правила за извод, докато не стане очевидно, че може да бъде премахнато изобщо от извеждането.

Доказателственият метод на Генцен по същество зависи от т.нар свойства на чистотата на променливите от логиката от първи ред на предикатите, от наличието на структурни правила за редуциране и усъвършенстване (добавяне) и от променливостта на правилата за заключение. По-специално, доказателството предполага, че смятането с правилото за изрязване е дедуктивно еквивалентно на смятането с правилото за смесване, което е вярно само при наличието на правилата за редукция и прецизиране. Следователно приложението на този метод е ограничено в областта нанекласическаталогика. Например, в релевантни и парапоследователни логики, изрязването не може да бъде заменено с объркване, а в модалните логики специалните оператори ограничават променливостта на правилата за извод. Допълнителни трудности възникват и при доказването на теоремата за елиминиране за логики от по-високи порядки.

Има различни модификации на доказателствения метод на Генцен. Едно от тях е директно премахване на изрязването (без да се заменя със смес или друго подобно правило). За да направим това, доказваме лема, според която при извеждане без съкращения всички приложения на съкращения могат да бъдат сведени до определена стандартна форма. В логиките с модални оператори могат да се формулират модалните правила за заключване на оригиналната система по такъв начин, че да се осигури променливостта на правилата в по-широк диапазон.

Теоремата за елиминиране има много важно методологично значение за изучаването на логическите системи. Например, Генцен показа, че теоремата за елиминиране на изрязване предоставя прости конструктивни (непривлекателни за семантичните концепции) начини за доказване на последователността на класическите и интуиционистичните логики от първи ред и разрешимостта на техните пропозиционални части. Той също използва своята теорема, за да докаже последователността на аритметиката от първи ред. Всъщност тази теорема се превърна в теоретична основа на ново направление в логическите изследвания - теорията за търсене на логически заключения и автоматизация на логическите доказателства.

1.Гентсен Г.Изследвания на логически заключения. – В кн.: Математическа теория на логическия извод. М., 1967.