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