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