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

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

Γ ⊢ A

B, Γ ⊢ A

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

B, B, Γ ⊢ A

B, Γ ⊢ A

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

Δ, B, C, Γ ⊢ A

Δ, C, B, Γ ⊢ A

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

&
Δ ⊢ A; Γ ⊢ B

Δ,Γ ⊢ A&B




Γ ⊢ A

Γ ⊢ A∨B
;
Γ ⊢ B

Γ ⊢ A∨B





Γ,A ⊢ B

Γ ⊢ A⊃B


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

¬

Δ, A ⊢ B; Γ, A ⊢ ¬B

Δ, Γ ⊢ ¬A


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

&

Γ ⊢ A&B

Γ ⊢ A
;
Γ ⊢ A&B

Γ ⊢ B




Δ ⊢ A∨B; Γ, A ⊢ C; Γ, B ⊢ C


Δ, Γ ⊢ C

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


Δ ⊢ A; Γ ⊢ A⊃B


Δ, Γ ⊢ B

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

¬
Γ ⊢ ¬¬A


Γ ⊢ A

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

¬
Γ ⊢ A; Γ ⊢ ¬A


Γ ⊢ B

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

Натуральная заработная плата    Натуральное исчисление    Натуральное обязательство