Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Ґергардом Ґенценом. Після праці Ґенцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу.
Термінологія
Числення секвенцій є альтернативною системою формального виводу до аксіоматичних систем описаних у статтях Числення висловлень і Логіка першого порядку. Формули логіки першого порядку для поданої нижче формальної системи мають лише дві логічні зв'яязки і квантор існування. Інші символи логічних зв'язок можна визначити формулами:
Подібно визначається і квантор загальності:
Загалом при визначенні правил використовуються такі позначення:
... (скінченні множини формул) ... (формули логіки першого порядку) ... (Символ, що показує, що з формул з лівої сторони (антецеденту) виводяться формули з правої сторони (консеквент)) ... (символ логічного заперечення) ... (символ диз'юнкції) ... (квантор існування)
Правила виводу
Правило антецедента
якщо: .
Правило припущення
якщо:
Перебір варіантів
Доведення від супротивного
Диз'юнкція а антецеденті
Диз'юнкція в консеквенті
Введення квантора істинності в консеквенті
Введення квантора істинності в антецеденті
, де y не зустрічається у вільному вигляді у формулі .
Рефлексивність рівності
Правило заміни в рівності
Приклади виведення
Приклад 1
Покажемо, що
Маємо:
Приклад 2
Як і в першому прикладі:
Коректність і повнота
Числення секвенцій є коректним і повним. Тобто всі формули, що можна вивести за його допомогою є логічно значимі і всі логічно значимі формули можна вивести за допомогою числення секвенцій. Це еквівалентно твердженню, що тоді і тільки тоді коли для довільних множини формул і формули .
Див. також Числення конструкцій
Джерела Правила виводу // Ebbinghaus H.-D., Flum J., Thomas W.: Mathematical logic. New York: Springer-Verlag, 1984. Richter, M. M.: Logikkalküle. Stuttgart: Teubner Verlag, 1978.
Weblinks Sequent Calculus by Alex Sakharov MathWorld