Натуральное исчисление, исчисление естественного вывода, натуральная дедукция, общее название логических исчислений, введённых и изученных в 1934 немецким логиком Г. Генценом (и независимо польским логиком С. Яськовским) с целью формализации процесса логического вывода, как можно более точно воспроизводящей структуру обычных содержательных рассуждений, а также для решения ряда важных задач метаматематики (в том числе для доказательства непротиворечивости арифметики натуральных чисел). Основным объектом Н. и. можно считать отношение (формальной) выводимости, обозначаемое символом , обладающее, по определению, свойством А  (разрешение усилить посылки),  (разрешение опускать одну из совпадающих посылок),  (разрешение переставлять посылки). В различных формулировках Н. и. вид и число структурных правил различны; например, понимая под Д и Г не последовательности, а просто конечные множества (неупорядоченные) формул, можно обойтись без правил перестановки посылок; обычное соглашение, что каждый элемент входит в него лишь один раз, делает ненужным правило сокращения повторяющихся посылок, и т.п. Кроме того, в Н. и. входят логические правила вывода, регламентирующие процедуру введения и удаления (устранения, исключения) символов логических операций и описывающие (как и аксиомы «обычных» логических исчислений; см., например, Логика высказываний) свойства этих операций. Вот правила классического Н. и. высказываний:

  Введение

(та к называемая «теорема о дедукции», см. Дедукция)

(reductio ad absurdum, или приведение к нелепости, см. Доказательство от противного) Удаление

(так называемое доказательство разбором случаев)

(modus ponens, или схема заключения)

(так называемый закон снятия двойного отрицания). (В скобках указана интерпретация некоторых правил в терминах традиционной логики; интерпретация остальных правил — та же, что у соответствующих аксиом обычного исчисления высказываний, перефразировками которых они являются.) Добавление к этому списку соот ветствующих правил введения и удаления для кванторов приводит к Н. и. предикатов. Замена правила -удаления на так называемое правило слабого  («из противоречия следует любое высказывание», см. Противоречия принцип) приводит к интуиционистскому (конструктивному) Н. и. высказываний (а с подходящими изменениями в кванторных правилах — к интуиционистскому Н. и. предикатов; см. Математический интуиционизм, Конструктивное направление).

  Доказательство в Н. и. — это, как обычно, вывод из пустого множества посылок. В формулировках Н. и., подобных приведённой, в которых нет аксиом (к роме, быть может, А  А), источником получения «логических законов», выражаемых формулами, доказуемыми без привлечения каких бы то ни было гипотез (посылок), оказывается правило É-введения. Гибкость аппарата Н. и., близость его к привычным формам содержательных рассуждений и простота получающихся выводов делают его удобным орудием логико-математического исследования. Н. и. полезно и в тех случаях, когда применяются другие системы логики: в качестве источника выводимых (дополнительных) правил вывода, применение которых также значительно упрощает логический аппарат, а также для получения эвристических (предварительных, подлежащих дальнейшему обоснованию) доводов, которые так или иначе должны предшествовать любому формальному доказательству (как источник доказываемых или опровергаемых гипотез).

  Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957, §§ 20, 23; Генцен Г., Исследования логических выводов, пер. с. нем., в кн.: Математическая теория логического вывода, М., 1967; Карри Х. Б., Основания математической логики, пер. с англ., М., 1969. См. также лит. при ст. Правило вывода.

  Ю. А. Гастов.