ЕЛІМІНАЦІЙНА ТЕОРЕМА це що таке ЕЛІМІНАЦІЙНА ТЕОРЕМА визначення
ЕЛІМІНАЦІЙНА ТЕОРЕМА
фундаментальна теорема доказів теорії Термін «елімінаційна теорема» введено X. Каррі як альтернативну назву теореми про усунення перерізу, яка вперше була сформульована і доведена Г. Генценом у вигляді «Основної теореми» (Hauptsatz) для обчислення секвенцій класичної та інтуїціоністської логіки предикатів у роботі «І. »(1934). Відповідно до цієї теореми, будь-який висновок у класичному чи інтуїціоністському обчисленні секвенцій можна перетворити на вьюод з тією ж кінцевою секвенцією, що не містить застосування правила перерізу. Ідейно усунення перерізу пов'язане з наступною характерною рисою секвенційних обчислень. Усі правила виведення (крім перерізу) діють так, що будь-яка формула, використана в дереві виведення, виявляється підформулою формули, що входить до результату виведення (кінцеву секвенцію). Тому вже за структурою формул цієї секвенції, фактично, можна визначити, що необхідно використовувати для отримання її висновку. Наявність перерізу ліквідує таку можливість, тому що при застосуваннях цього правила з виведення зникають формули, що входять в обидві посилки перерізу. Доказ елімінаційної теореми полягає в демонстрації ефективної процедури перетворення довільного вихідного висновку (із застосуванням перерізу) на результуючий висновок (без застосування перерізу). Природно, вихідний і результуючий висновки будуються в тому самому обчисленні і закінчуються однією і тією ж секвенцією. У класичному варіанті докази Генцена ключову роль відіграє т. Неосновна лема », згідно з якою з вихідного висновку завжди можна усунути застосування правила змішування. Оскільки перетин є окремим випадком змішування, з основної леми випливає, щозастосування перерізу усунути.
Основна лема доводиться зворотної індукцією за трьома параметрами: числу застосувань правила змішування у вихідному висновку, ступеня та рангу змішування. Ідея доказу полягає в тому, щоб показати усунення змішування з тієї частини дерева вихідного висновку, яка закінчується єдиним застосуванням цього правила. Якщо таке можливо, то всі застосування змішування усуваються послідовно, починаючи з самого верхнього. Структура доказу визначається кінцевим числом редукцій (кроків перетворень вихідного висновку, що закінчується єдиним застосуванням змішування), у ході яких зменшується або ступінь, або ранг змішування і в результаті виходить висновок без змішувань.
Формальний доказ основної леми складається з розгляду великої кількості окремих випадків та підвипадків. Змістовно воно базується на перестановочності правил ув'язнення у секвенційному висновку. Суть редукцій у тому, що єдине застосування змішування «переміщається» вгору по дереву виводу — переставляється з попередніми застосуваннями інших правил ув'язнення доти, доки стає очевидним, що його можна видалити з висновку.
Метод доказу Генцена суттєво залежить від т. в. властивості чистоти змінних першопорядкової логіки предикатів, від структурних правил скорочення і уточнення (додання) і зажадав від перестановочності правил укладання. Зокрема, у доказі передбачається, що літочислення з правилом перерізу дедуктивно еквівалентно літочисленню з правилом змішування, що правильне лише за наявності правил скорочення та витончення. Тому застосування цього методу обмежено у сфері некласичних логік. Напр., в релевантній та паранесуперечливій логіках перетин не можна замінити змішуванням, а в модальнихУ логіках спеціальні оператори обмежують перестановочність правил укладання. Додаткові проблеми виникають і при доказі елімінаційної теореми для логік вищих порядків.
Існують різні модифікації методу доказу Генцена. Одна з них полягає в тому, щоб усувати безпосередньо перетин (не замінюючи його змішуванням чи іншим подібним правилом). Для цього доводиться лема, згідно з якою у виведенні без перерізів застосування скорочень можна привести до певного стандартного вигляду. У логіках з модальними операторами можна сформулювати модальні правила укладання вихідної системи те щоб забезпечити перестановочність правил у ширших межах.
Елімінаційна теорема має дуже важливе методологічне значення для вивчення логічних систем. Напр., Генцен показав, що теорема про усунення перерізу забезпечує прості конструктивні (що не апелюють до семантичних понять) способи доказу несуперечності класичної та інтуїціоністської першопорядкових логік та розв'язності їх пропозиційних частин. Він використав свою теорему і для доказу несуперечності першопорядкової арифметики. Фактично ця теорема стала теоретичною основою нового напряму логічних досліджень - теорії пошуку логічних висновків та автоматизації логічних доказів.
Генцен Г. Дослідження логічних висновків. - У кн.: Математична теорія логічного висновку. М., 1967.