Числення секвенцій
Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Генріхом Генценом. Після праці Генцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу.
ТермінологіяРедагувати
Числення секвенцій є альтернативною системою формального виводу до аксіоматичних систем описаних у статтях Числення висловлень і Логіка першого порядку. Формули логіки першого порядку для поданої нижче формальної системи мають лише дві логічні зв'яязки і квантор існування. Інші символи логічних зв'язок можна визначити формулами:
- Подібно визначається і квантор загальності:
Загалом при визначенні правил використовуються такі позначення:
- ... (скінченні множини формул)
- ... (формули логіки першого порядку)
- ... (Символ, що показує, що з формул з лівої сторони (антецеденту) виводяться формули з правої сторони (консеквент))
- ... (символ логічного заперечення)
- ... (символ диз'юнкції)
- ... (квантор існування)
Правила виводуРедагувати
Правило антецедентаРедагувати
якщо: .
Правило припущенняРедагувати
якщо:
Перебір варіантівРедагувати
Доведення від супротивногоРедагувати
Диз'юнкція а антецедентіРедагувати
Диз'юнкція в консеквентіРедагувати
Введення квантора істинності в консеквентіРедагувати
Введення квантора істинності в антецедентіРедагувати
, де y не зустрічається у вільному вигляді у формулі .
Рефлексивність рівностіРедагувати
Правило заміни в рівностіРедагувати
Приклади виведенняРедагувати
Приклад 1Редагувати
Покажемо, що
Маємо:
Приклад 2Редагувати
Як і в першому прикладі:
Коректність і повнотаРедагувати
Числення секвенцій є коректним і повним. Тобто всі формули, що можна вивести за його допомогою є логічно значимі і всі логічно значимі формули можна вивести за допомогою числення секвенцій. Це еквівалентно твердженню, що тоді і тільки тоді коли для довільних множини формул і формули .
ДжерелаРедагувати
- Правила виводу // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — С. 507. — 742 с. — 1000 екз. — ББК 87я2. — ISBN 966-531-128-X.
- 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