Натуральне числення, числення природного виводу, натуральна дедукція, загальна назва логічних числень, введених і вивчених в 1934 німецьким логіком Г. Генценом (і незалежно польським логіком С. Яськовським) з метою формалізації процесу логічного виводу, як можна точніше відтворюючою структуру звичайних змістовних міркувань, а також для вирішення ряду важливих завдань метаматематики (у тому числі для доказу несуперечності арифметики натуральних чисел). Основним об'єктом Н. і. можна рахувати відношення (формальною) виводимості, що позначається символом, володіє, за визначенням, властивістю А, (дозвіл опускати одну із співпадаючих посилок), (дозвіл переставляти посилки). У різних формулюваннях Н. і. вигляд і число структурних правил різні; наприклад, розуміючи під Д і Г не послідовності, а просто кінцеву безліч (неврегульовані) формул, можна обійтися без правил перестановки посилок; звичайна угода, що кожен елемент входить в нього лише один раз, робить непотрібним правило скорочення посилок, що повторюються, і т.п. Крім того, в Н. і. входять логічні правила виводу, що регламентують процедуру введення і видалення (усунення виключення) символів логічних операцій і властивості цих операцій, що описують (як і аксіоми «звичайних» логічних числень; див.(дивися), наприклад, Логіка висловів ). Ось правила класичного Н. і. висловів:
Введення
(так звана «теорема про дедукцію», див.(дивися) Дедукція )
(reductio ad absurdum, або приведення до безглуздості, див.(дивися) Доказ від осоружного ) Видалення
(так званий доказ розбором випадків)
(modus ponens, або схема висновку)
(так званий закон зняття подвійного заперечення). (У дужках вказана інтерпретація деяких правил в термінах традиційної логіки; інтерпретація останніх правил — та ж, що у відповідних аксіом звичайного числення висловів, перефразовуваннями яких вони є.) Додавання до цього списку відповідних правил введення і видалення для кванторів приводить до Н. і. предикатів. Заміна правила -удаленія на так зване правило слабкого («з протиріччя виходить будь-який вислів», див.(дивися) Протиріччя принцип ) приводить до інтуїционістському (конструктивному) Н. і. висловів (а з відповідними змінами в правилах кванторів — до інтуїционістському Н. і. предикатів; див.(дивися) Математичний інтуїционізм, Конструктивний напрям ).
Доказ в Н. і. — це, як завжди, вивід з порожньої безлічі посилок. У формулюваннях Н. і., подібних приведеною, в яких немає аксіом (окрім, мабуть, А А), джерелом здобуття «логічних законів», що виражаються формулами, доказовими без залучення яких би то не було гіпотез (посилок), виявляється правило É-введения. Гнучкість апарату Н. і., близькість його до звичних форм змістовних міркувань і простота виводів, що виходять, роблять його зручним знаряддям логіко-математичного дослідження. Н. і. корисно і в тих випадках, коли застосовуються інші системи логіки: як джерело правил виводу, що виводяться (додаткових), вживання яких також значно спрощує логічний апарат, а також для здобуття евристичних (попередніх, підлягаючих подальшому обгрунтуванню) аргументів, які так чи інакше повинні передувати будь-якому формальному доказу (як джерело доводжуваних або заперечуваних гіпотез).
Літ.: Кліні С. До., Введення у метаматематику, пер.(переведення) з англ.(англійський), М., 1957 §§ 20, 23; Генцен Р., Дослідження логічних виводів, пер.(переведення) с. йому.(німецький), у кн.: Математична теорія логічного виводу, М., 1967; Каррі Х. Би., Підстави математичної логіки, пер.(переведення) з англ.(англійський), М., 1969. Див. також літ.(літературний) при ст. Правило виведення .
