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

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

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

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

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

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

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

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

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

  якщо:  .

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

  якщо:  

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

 

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

 

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

 

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

 

 

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

 

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

 , де y не зустрічається у вільному вигляді у формулі   .

Рефлексивність рівностіРедагувати

 


Правило заміни в рівностіРедагувати

 

Приклади виведенняРедагувати

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

Покажемо, що

 

Маємо:

 

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

 

Як і в першому прикладі:

 

Коректність і повнотаРедагувати

Числення секвенцій є коректним і повним. Тобто всі формули, що можна вивести за його допомогою є логічно значимі і всі логічно значимі формули можна вивести за допомогою числення секвенцій. Це еквівалентно твердженню, що   тоді і тільки тоді коли   для довільних множини формул   і формули  .

ДжерелаРедагувати

WeblinksРедагувати