Секвенцій числення (позднелатінськоє sequentia — послідовність, слідство), секвенциальниє числення, числення способів висновків, модифікації поняття логічного числення, в яких основними об'єктами перетворення є не формули, а т.з. секвенції, тобто вирази вигляду A 1 , ..., A l ® B 1 , ..., Bm, де ® аналогічна знаку виводимості, A 1 , ..., A l і B 1 , ..., Bm — довільні формули; перші — створюючі антецедент секвенції, другі, — її сукцедент. При l, m ³ 1 секвенція A 1 ..., A l ® B 1 ... B m інтерпретується як формула
A 1 &... &A 1 É B 1 Ú...Ú B m .
(& — знак кон'юнкції É — імплікації Ú — диз'юнкції, див.(дивися) Логічні операції ) , секвенція з порожнім антецедентом інтерпретується як істина, а секвенція з порожнім сукцедентом — як брехня (і, отже, секвенція ®, що складається з однієї стрілки, — як протиріччя). Аксіомами (вихідними секвенціями) в С. і. є всі секвенції вигляду З ® З (і лише вони). Правила виводу діляться на т.з. структурні і логічні. Перші кодифікують допустимі зміни «формульного складу» антецедента і сукцеденту, другі — введення в секвенції різних логічних символів. Структурні правила — це «уточнення» (додавання довільної формули до антецеденту або сукцеденту) «скорочення» (викреслювання формул, що повторюються), перестановка довільних формул в антецеденте або сукцеденті, а також «перетин»
(латинськими буквами позначаються довільні формули, грецькими — строчки формул, розділених комами, над межею пишеться посилка правила, під межею — висновок). Логічні правила виводу мають для секвенциального класичного числення висловів наступний вигляд:
; ;
.
Якщо і структурні, і логічні правила виводу обмежити умовою, згідно з якою в сукцеденті кожної секвенції повинно бути не більш за одну формулу, то отримаємо секвенциальноє інтуїционістськоє числення висловів: ця умова виявляється достатньою для невиводимості в С. і. виключеного третього принципу (а також закону зняття подвійного заперечення). Секвенциальноє числення предикатів виходить приєднанням до попередніх правил ще двох пар правил введення кванторів спільності і існування.
Основний результат німецького математика Г. Генцена полягає у встановленні можливості приведення кожного виведення в С. і. до «нормальної форми», що не містить вживань правила перетину і що тим самим представляє в деякому розумінні «прямою» вивід. З багаточисельних додатків цього результату особливо важливі докази несуперечності арифметичних формальних систем, що використовують математичну техніку, що виходить за рамки гильбертовського фінітізма (див. Аксіоматичний метод, Метаматематика ) , і труднощі, що тим самим обходять у відомому сенсі, обумовлені теоремою До. Геделя про неповноту формальної арифметики. Ета ж основна теорема Генцена лежить в основі більшості алгоритмів виводимості для логічних і логіко-математичних числень (див. Дозволи проблема ) , чим і обумовлена виняткова важливість С. і. для досліджень, що інтенсивно розвиваються, в області машинного пошуку логічного виводу, що є важливим прикладом моделювання інтелектуальної діяльності людини.
Літ.: Генцен Р., Дослідження логічних виводів, пер.(переведення) з йому.(німецький), у кн.: Математична теорія логічного виводу, М-код, 1967, с. 9—74; його ж. Несуперечність чистої теорії чисел, там же, с. 77—153; його ж, Новий виклад доказу несуперечності для чистої теорії чисел, там же, с. 154—90; Каррі Х. Би Підстави математичної логіки. пер.(переведення) з англ.(англійський), М., 1969, гл.(глав) 5С, 6b, 7b і 8b; Алгорифм машинного пошуку природного логічного виводу в численні висловів, М. — Л., 1965.
