Обчислення секвенцій
Обчислення секвенцій(англ. Sequent calculus) [1] - Система формального виведення формул логіки першого порядку (і як окремого випадку логіки висловлювань) запропонована німецьким логіком Герхардом Генценом. [2] Генценом було розроблено кілька еквівалентних варіантів обчислення секвенцій.
Зміст
Концептуальний принцип [ред.]
Обчислення секвенцій є альтернативною системою формального виведення в аксіоматичних системах обчислення висловлювань та логіки першого порядку.
Це формальна система, в якій до алфавіту мови логіки (що включає операції ∨, &, ¬ і квантори ∀ і ∃) доданий символ прямування, що позначається ├, який читається «виводимо» або «доводимо». Правила виведення a├ b (b виводиться з a) застосовуються безпосередньо до формул, а не до таблиць істинності, дозволяючи з істинності одних формул робити висновок про істинність інших формул. Символи a, b у правилі виведення позначають одну або декілька формул; a називається умовою (антецедентом), а b – наслідком (сукцедентом, консеквентом). Якщо за умови чи слідстві формул кілька, всі вони записуються через кому. Цікаві лише такі правила виведення, за допомогою яких на підставі істинності всіх формул, що входять до умови правила виведення, можна за будь-якої інтерпретації зробити висновок про істинність усіх формул, що входять до наслідок правила виведення. Зазвичай такі правила називають багатими.
Висновок у обчисленні секвенцій — це кінцева послідовність секвенцій ∑1, ∑2, …, ∑k така, що для кожного i , 1 ≥ i ≤ k, секвенція ∑i є або аксіомою, або безпосереднім наслідком з попередніх секвенцій за правилами виведення . [3]
Обчислення секвенцій є коректним та повним. Тобто всі формули, які можна вивести з йогодопомогою є логічно значущі та всі логічно значущі формули можна вивести за допомогою обчислення секвенцій.
Правила виведення [ред.]
Нижче представлені правила виведення для LK-обчислення (нім. Klassische Prädikatenlogik - логіки предикатів), запропонованого Генценом в 1934 році.
| Аксіома: | Перетин: [4] |
Структурні правила [ред.]
Послаблення (W) дозволяє додавати довільні елементи до послідовності. Ослаблення антецедента (WL) інтуїтивно зрозуміле, тому що ми завжди можемо обмежити сферу нашого доказу (якщо всі автомобілі мають колеса, то можна впевнено сказати, що всі чорні автомобілі мають колеса); у випадку з сукцедентом (WR), ослаблення припустимо, коли ми можемо припустити альтернативні висновки (якщо всі автомобілі мають колеса, то можна з упевненістю сказати, що всі автомобілі мають колеса або крила).
Скорочення (.С) та перестановка (Р) допустимі, коли ні кратність входження (.С), ні порядок (Р) елементів не належать до питань дослідження послідовностей.
Властивості обчислення [ред.]
Логічні та структурні правила обчислення секвенцій мають низку цікавих властивостей. По-перше, легко встановити, що це правила є оборотними, тобто правила виведення, отримані з вихідних заміною верхньої секвенції (верхніх секвенцій) на нижню, а нижньої на верхню, є похідними правилами. По-друге, всі правила виведення, виключаючи перетин, мають властивість підформуленості, тобто у верхні секвенції входять лише формули, графічнозбігаються з формулами нижньої секвенції, або є підформулами формул, що входять до нижньої секвенції . [5]
Перетин [ ред .
Єдиним правилом, що грає у обчисленні особливу роль, є переріз. Воно порушує зазначені вище властивості. Однак Генценом було доведено, що і в класичній і в інтуїціоністській логіці першого порядку перетин є допустимим правилом: якщо можна побудувати виведення деякої секвенції за допомогою перерізу, то можна побудувати висновок тієї ж секвенції, що не містить перетину. [6] Теорема Генцена про усунення перетину [7] є фундаментальним результатом у логіці і має виключно важливе значення в першу чергу для обґрунтування логіки. Зокрема, з цієї теореми безпосередньо випливає теорема про несуперечність обчислення [5], що спростовує Теореми Геделя про неповноту.
Субструктурні логіки [ред.]
Як варіанти обчислення, можна обмежити або заборонити використання деяких структурних правил. Це дає безліч субструктурних логічних систем (англ. Substructural logic). [8] Вони, як правило, слабші, ніж LK-обчислення (тобто мають менше теорем), і таким чином не перетинаються з класичною семантикою логіки першого порядку. Тим не менш, у них є інші цікаві властивості, які використовуються як додатки в теоретичній інформатиці [9] та штучному інтелекті.