Відкрити головне меню

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

Зміст

ТермінологіяРедагувати

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

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

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

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

Правила виводуРедагувати

Правило антецедентаРедагувати

  якщо:  .

Правило припущенняРедагувати

  якщо:  

Перебір варіантівРедагувати

 

Доведення від супротивногоРедагувати

 

Диз'юнкція а антецедентіРедагувати

 

Диз'юнкція в консеквентіРедагувати

 

 

Введення квантора істинності в консеквентіРедагувати

 

Введення квантора істинності в антецедентіРедагувати

 , де 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Редагувати