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