Чи́слення секве́нцій — система формального виведення формул логіки першого порядку (і як часткового випадку логіки висловлень) запропонована німецьким логіком Ґергардом Ґенценом. Після праці Ґенцена розроблено кілька варіантів числення секвенцій, що є еквівалентними між собою і альтернативою аксіоматичному підходу.
Числення секвенцій є альтернативною системою формального виводу до аксіоматичних систем описаних у статтях Числення висловлень і Логіка першого порядку. Формули логіки першого порядку для поданої нижче формальної системи мають лише дві логічні зв'яязки
і квантор існування. Інші символи логічних зв'язок можна визначити формулами:
![{\displaystyle (\varphi \wedge \psi ):\Leftrightarrow \neg (\neg \varphi \vee \neg \psi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1f3027d3b7190c599eb810d0f7039ef0092ed86b)
![{\displaystyle (\varphi \rightarrow \psi ):\Leftrightarrow (\neg \varphi \vee \psi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4f9dae66f18784cf9186442108ce7e2ad36c17ed)
![{\displaystyle (\varphi \leftrightarrow \psi ):\Leftrightarrow \neg (\neg (\neg \varphi \vee \psi )\vee \neg (\neg \psi \vee \varphi ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8ef6557f5f492ce921f284d2cd184580ffd16d3c)
- Подібно визначається і квантор загальності:
![{\displaystyle \forall x\varphi :\Leftrightarrow \neg \exists x\neg \varphi }](https://wikimedia.org/api/rest_v1/media/math/render/svg/200ebb361b0be7a7bc6cb0a40b67dd82bc1015b1)
Загалом при визначенні правил використовуються такі позначення:
... (скінченні множини формул)
... (формули логіки першого порядку)
... (Символ, що показує, що з формул з лівої сторони (антецеденту) виводяться формули з правої сторони (консеквент))
... (символ логічного заперечення)
... (символ диз'юнкції)
... (квантор існування)
якщо:
.
якщо:
, де y не зустрічається у вільному вигляді у формулі
.
Покажемо, що
Маємо:
Як і в першому прикладі:
Числення секвенцій є коректним і повним. Тобто всі формули, що можна вивести за його допомогою є логічно значимі і всі логічно значимі формули можна вивести за допомогою числення секвенцій. Це еквівалентно твердженню, що
тоді і тільки тоді коли
для довільних множини формул
і формули
.