НАТУРАЛЬНОЕ ИСЧИСЛЕНИЕ
исчисление
естественного вывода, натуральная дедукция, общее название логич исчислений,
введенных и изученных в 1934 нем логиком Г Генценом (и независимо польск
логиком С Яськовским) с целью формализации процесса логич вывода, как можно
более точно воспроизводящей структуру обычных содержат рассуждений, а также
для решения ряда важных задач метаматематики (в т ч дтя доказательства
непротиворечивости
арифметики
натуральных чисел) Оси объектом H и можно считать отношение (формальной)
выводимости, обозначаемое символом -, обладающее, по определению, свойством
А -, А (здесь А - произвольное высказывание выраженное формулой
H и ) и удовлетворяющее след "структурным" правилам вывода
(здесь
и в дальнейшем в записи правил под горизонтальной чертой помещается выводимость,
получаемая в предположении, что дана выводимость, записанная над чертой,
прописные лат буквы обозначают произвольные формулы а греч буквы - последовательности
формул)
(разрешение усилить посылки),
(разрешение опускать одну из совпадающих
посылок),
(разрешение переставлять посыпки) В различных
формулировках H и вид и число структурных правил различны, напр , понимая
под
и Г не последовательности,
а просто конечные множества (неупорядоченные) формул, можно обойтись без
правил перестановки посылок обычное соглашение, что каждый элемент входит
в него лишь один раз, делает ненужным правило сокращения повторяющихся
посылок, и т д Кроме того, в H и входят логические правила вывода peгламентирующие
процедуру введения и удаления (устранения исключения) символов логич операций
и описывающие (как и аксиомы "обычных" логич исчислений см , напр , огика
высказываний) свойства этих операций Вот правила классического H и.
высказываний
Введение
(т. н. "теорема о дедукции", см. Дедукция)
(reductio ad absurdum, или приведение к
нелепости, см. Доказательство от противного ) Удаление
(т. н. доказательство разбором случаев)
(raodus ponens, или схема заключения)
(т. н. закон снятия двойного отрицания).
(В скобках указана интерпретация нек-рых правил в терминах традиционной
логики; интерпретация остальных правил - та же, что у соответствующих аксиом
обычного исчисления высказываний, перефразировками к-рых они являются.)
Добавление к этому списку соответствующих правил введения и удаления для
кванторов
приводит
к H. и. предикатов. Замена правила ? -удаления на т. н. правило слабого
?-удаления (Г|-А;Г|-?А)/Г|-В , ("из противоречия следует любое высказывание",
см. Противоречия принцип) приводит к интуиционистскому (конструктивному)
H. и. высказываний (а с подходящими изменениями в кванторных правилах -
к интуиционистскому H. и. предикатов; см. Математический интуиционизм,
Конструктивное направление).
Доказательство в H. и.- это, как
обычно, вывод из пустого множества посылок. В формулировках H. и., подобных
приведённой, в к-рых нет аксиом (кроме, быть может, А |- А), источником
получения "логических законов", выражаемых формулами, доказуемыми без привлечения
каких бы то ни было гипотез (посылок), оказывается правило U-введения.
Гибкость аппарата H. и., близость его к привычным формам содержательных
рассуждений и простота получающихся выводов делают его удобным орудием
логико-математич. исследования. H. и. полезно и в тех случаях, когда применяются
другие системы логики: в качестве источника выводимых (дополнительных)
правил вывода, применение к-рых также значительно упрощает ло-гич. аппарат,
а также для получения эвристических (предварительных, подлежащих дальнейшему
обоснованию) доводов, к-рые так или иначе должны предшествовать любому
формальному доказательству (как источник доказываемых или опровергаемых
гипотез).
Лит.: К л и н и С. К., Введение
в метаматематику, пер. с англ., M., 1957, §§ 20, 23; Г е н ц е н Г., Исследования
логических выводов, пер. с нем., в кн.: Математическая теория логического
вывода, M., 1967; К а рр и X. Б., Основания математической логики, пер.
с англ., M., 1969. См. также лит. при ст. Правило вывода. Ю. А. Гастев.
А Б В Г Д Е Ё Ж З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Ъ Ы Ь Э Ю Я