Натуральное исчисление

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

        

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

         Введение

        

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

        

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

        

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

        

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

        

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

         Доказательство в Н. и. — это, как обычно, вывод из пустого множества посылок. В формулировках Н. и., подобных приведённой, в которых нет аксиом (кроме, быть может, А

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

         Ю. А. Гастов.