Числення секвенцій

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Генріхом Генценом. Після праці Генцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу.

Термінологія[ред.ред. код]

Числення секвенцій є альтернативною системою формального виводу до аксіоматичних систем описаних у статтях Числення висловлень і Логіка першого порядку. Формули логіки першого порядку для поданої нижче формальної системи мають лише дві логічні зв'яязки і квантор існування. Інші символи логічних зв'язок можна визначити формулами:

  • Подібно визначається і квантор загальності:

Загалом при визначенні правил використовуються такі позначення:

  • ... (скінченні множини формул)
  • ... (формули логіки першого порядку)
  • ... (Символ, що показує, що з формул з лівої сторони (антецеденту) виводяться формули з правої сторони (консеквент))
  • ... (символ логічного заперечення)
  • ... (символ диз'юнкції)
  • ... (квантор існування)

Правила виводу[ред.ред. код]

Правило антецедента[ред.ред. код]

якщо: .

Правило припущення[ред.ред. код]

якщо:

Перебір варіантів[ред.ред. код]

Доведення від супротивного[ред.ред. код]

Диз'юнкція а антецеденті[ред.ред. код]

Диз'юнкція в консеквенті[ред.ред. код]

Введення квантора істинності в консеквенті[ред.ред. код]

Введення квантора істинності в антецеденті[ред.ред. код]

, де 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[ред.ред. код]