Большая Советская Энциклопедия (цитаты)

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

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

  Введение



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



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



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



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



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

  Доказательство в Н — это, как обычно, вывод из пустого множества посылок. В формулировках Н, подобных приведенной, в которых нет аксиом (кроме, быть может, А  А), источником получения "логических законов", выражаемых формулами, доказуемыми без привлечения каких бы то ни было гипотез (посылок), оказывается правило É-введения. Гибкость аппарата Н, близость его к привычным формам содержательных рассуждений и простота получающихся выводов делают его удобным орудием логико-математического исследования. Н полезно и в тех случаях, когда применяются другие системы логики: в качестве источника выводимых (дополнительных) правил вывода, применение которых также значительно упрощает логический аппарат, а также для получения эвристических (предварительных, подлежащих дальнейшему обоснованию) доводов, которые так или иначе должны предшествовать любому формальному доказательству (как источник доказываемых или опровергаемых гипотез).

  Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957, §§ 20, 23; Генцен Г., Исследования логических выводов, пер. с. нем., в кн.: Математическая теория логического вывода, М., 1967; Карри Х. Б., Основания математической логики, пер. с англ., М., 1969. См. также лит. при ст. Правило вывода.

  Ю. А. Гастов.


Для поиска, наберите искомое слово (или его часть) в поле поиска


Новости 25.06.2022 08:21:55