ЗЛІЧЕННЯ СЕКВЕНЦІЙ

- одна з основних форм подання логічних систем, що застосовується в логіці поряд з аксіоматичними системами (гільбертівського типу) і системами натурального (природного) висновку. Термін "секвенція" походить від слова sequent (послідовність). Він введений у логіку П.Герцем (1929) і запозиченийГ.Генценом, який вперше сформулював у формі обчислення секвенцій класичну та інтуїціоністськулогіку предикатівпершого порядку.

Секвенція – це формальний запис відношення логічної виведеності виду F→Θ, де Г і Θ – послідовності (можливо порожні) розділених комами формул. Замість стрілки можна використовувати «⊢» або будь-який інший знак логічного виведення. Ліву частину секвенції називають антецедентом, а праву сукцедентом. Змістовно у вихідному генценовском варіанті секвенція означає, що з кон'юнкції формул, що входять до її антецедента, логічно виводиться диз'юнкція формул, що входять до її сукцеденту. Напр.: А1, . Аn, → В1, . Вm означає А1& . & & Аn ⊢В1∨. ∨Bm; →В1, . Bm означає ⊢ В1,∨. ∨Bm; A1, . Аn, → означає ⊢ (Α1& . & &An); a секвенція, обидві частини якої порожні, може інтерпретуватися як логічне протиріччя.

Обчислення секвенцій і двох основних компонентів: основний секвенції і правил укладання (іноді їх називають правилами виведення). Основна секвенція у початковому генценовском варіанті – це секвенція виду А→А, де А– формула, але можуть застосовуватися основні секвенції та іншого виду. Правила укладання поділяються на два типи: логічні та структурні. Логічні правила укладання у свою чергу поділяються на правила введення логічного знака до антецеденту та правилвведення логічного знака до сукцеденту секвенції. За логічним правилом з формул, що входять до його посилки (бічних формул), у висновку за допомогою введення логічного знака виходить складніша формула (головна формула). Таким чином, логічні правила дозволяють будувати складні формули більш простих. Число логічних правил у обчисленні секвенцій визначається числом логічних констант, що використовуються в даному обчисленні. Структурні правила (перестановка, скорочення та витончення) впливають не так на структуру окремих формул, але в структуру секвенцій. В результаті застосування цих правил входження формул до антецеденту або сукцеденту секвенції переставляються, скорочуються або додаються. Логічні та структурні правила укладання для класичної та інтуїціоністської логік симетричні в тому сенсі, що кожному антецедентному (сукцедентному) правилу відповідає точно одне сукцедентне (антецедентне) правило.

Особливу роль обчисленні секвенцій грає правило, зване «перетином»:

Це єдине правило, у результаті застосування якого формула перерізу (у разі А) викреслюється з висновку. Всі інші правила зберігають так звану властивість підформульності висновку: всі формули, що входять до посилки конкретного правила, є підформулами деяких формул, що входять до висновку цього правила. Висновок у обчисленні секвенцій має форму дерева секвенцій, побудова якого починається з основної секвенції (основних секвенцій) і продовжується за правилами укладання. Секвенція вважається виведеною у обчисленні секвенцій, якщо можна побудувати висновок, у якому вона є останньою (кінцевою) секвенцією. Строго кажучи, дерева в обчисленні секвенцій є не висновками у стандартному сенсі терміна «логічний висновок», а метаконструкціями, припобудові яких виконуються логічні переходи від одних записів про виведеннядоіншим. Інтерпретація секвенцій у своїй може бути різною, що відкриває широкі змогу дослідження загальних властивостей формальних логічних доказів.

З обчисленням секвенцій пов'язаний отриманий Г. Генценом фундаментальний результат сучасної логіки - теорема про усунення перерізу, або елімінаційна теорема. У доказі цієї теореми Г. Генцен замінює переріз правилом змішування:

де Δ* і Θ* не містять формули А, і показує, що з будь-якого висновку в обчисленні секвенцій класичної та інтуїціоністської першопорядкової логіки можна усунути застосування цього правила.

Існує безліч модифікацій початкового генценівського варіанта обчислення секвенцій для класичної та некласичної логік. Методологічно ці модифікації зводяться до того, що змінюється форма або число основних секвенцій, форма або число правил укладання або вводяться обмеження на застосування конкретних правил укладання при побудові дерева виведення. Іноді змінюється саме поняття секвенції та використовуються такі об'єкти, як надсеквенції, кортежі секвенцій, структури і т.д. Досить прозорий і ефективний підхід до формулювання обчислення, у якому правилам укладання надається «глобальний» характер – їх застосування залежить лише від виду посилок, а й стану висновків цих посилок. Такі правила зокрема розширюють можливості доказу теореми про усунення перерізу для некласичних логік.

Обчислення секвенцій тісно пов'язані з табличними уявленнями логічних систем та забезпечують природний перехід між синтаксичним та семантичним рівнями аналізу некласичних логік. Вони є зручним апаратом дослідженнякількісних та якісних характеристик логічних висновків та процедур пошуку логічних доказів.

1. Математична теорія логічного висновку. М., 1969.