Определение слова «Натуральное исчисление»

Большая советская энциклопедия:

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

(разрешение усилить посылки),

(разрешение опускать одну из совпадающих посылок),

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

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

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

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

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

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

(«из противоречия следует любое высказывание», см. Противоречия принцип)
приводит к интуиционистскому (конструктивному) Н. и. высказываний (а с подходящими изменениями в кванторных правилах — к интуиционистскому Н. и. предикатов; см. Математический интуиционизм, Конструктивное направление).
Доказательство в Н. и. — это, как обычно, вывод из пустого множества посылок. В формулировках Н. и., подобных приведённой, в которых нет аксиом (кроме, быть может, А А), источником получения «логических законов», выражаемых формулами, доказуемыми без привлечения каких бы то ни было гипотез (посылок), оказывается правило -введения. Гибкость аппарата Н. и., близость его к привычным формам содержательных рассуждений и простота получающихся выводов делают его удобным орудием логико-математического исследования. Н. и. полезно и в тех случаях, когда применяются другие системы логики: в качестве источника выводимых (дополнительных) правил вывода, применение которых также значительно упрощает логический аппарат, а также для получения эвристических (предварительных, подлежащих дальнейшему обоснованию) доводов, которые так или иначе должны предшествовать любому формальному доказательству (как источник доказываемых или опровергаемых гипотез).
Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957, §§ 20, 23; Генцен Г., Исследования логических выводов, пер. с. нем., в кн.: Математическая теория логического вывода, М., 1967; Карри Х. Б., Основания математической логики, пер. с англ., М., 1969. См. также лит. при ст. Правило вывода.
Ю. А. Гастов.

Смотреть другие определения →