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