НАТУРАЛЬНОЕ ИСЧИСЛЕНИЕ
НАТУРАЛЬНОЕ ИСЧИСЛЕНИЕ, исчисление естественного вывода, натуральная дедукция, общее название логич исчислений, введенных и изученных в 1934 нем логиком Г Генценом (и независимо польск логиком С Яськовским) с целью формализации процесса логич вывода, как можно более точно воспроизводящей структуру обычных содержат рассуждений, а также для решения ряда важных задач метаматематики (в т ч дтя доказательства непротиворечивости арифметики натуральных чисел) Оси объектом H и можно считать отношение (формальной) выводимости, обозначаемое символом -, обладающее, по определению, свойством А -, А (здесь А - произвольное высказывание выраженное формулой H и ) и удовлетворяющее след "структурным" правилам вывода (здесь и в дальнейшем в записи правил под горизонтальной чертой помещается выводимость, получаемая в предположении, что дана выводимость, записанная над чертой, прописные лат буквы обозначают произвольные формулы а греч буквы - последовательности формул)
(разрешение усилить посылки),
(разрешение опускать одну из совпадающих посылок),
(разрешение переставлять посыпки) В различных
формулировках H и вид и число структурных правил различны, напр , понимая
под 
Введение
(т. н. "теорема о дедукции", см. Дедукция)
(reductio ad absurdum, или приведение к нелепости, см. Доказательство от противного ) Удаление
(т. н. доказательство разбором случаев)
(raodus ponens, или схема заключения)
(т. н. закон снятия двойного отрицания). (В скобках указана интерпретация нек-рых правил в терминах традиционной логики; интерпретация остальных правил - та же, что у соответствующих аксиом обычного исчисления высказываний, перефразировками к-рых они являются.) Добавление к этому списку соответствующих правил введения и удаления для кванторов приводит к H. и. предикатов. Замена правила ? -удаления на т. н. правило слабого ?-удаления (Г|-А;Г|-?А)/Г|-В , ("из противоречия следует любое высказывание", см. Противоречия принцип) приводит к интуиционистскому (конструктивному) H. и. высказываний (а с подходящими изменениями в кванторных правилах - к интуиционистскому H. и. предикатов; см. Математический интуиционизм, Конструктивное направление).
Доказательство в H. и.- это, как обычно, вывод из пустого множества посылок. В формулировках H. и., подобных приведённой, в к-рых нет аксиом (кроме, быть может, А |- А), источником получения "логических законов", выражаемых формулами, доказуемыми без привлечения каких бы то ни было гипотез (посылок), оказывается правило U-введения. Гибкость аппарата H. и., близость его к привычным формам содержательных рассуждений и простота получающихся выводов делают его удобным орудием логико-математич. исследования. H. и. полезно и в тех случаях, когда применяются другие системы логики: в качестве источника выводимых (дополнительных) правил вывода, применение к-рых также значительно упрощает ло-гич. аппарат, а также для получения эвристических (предварительных, подлежащих дальнейшему обоснованию) доводов, к-рые так или иначе должны предшествовать любому формальному доказательству (как источник доказываемых или опровергаемых гипотез).
Лит.: К л и н и С. К., Введение в метаматематику, пер. с англ., M., 1957, §§ 20, 23; Г е н ц е н Г., Исследования логических выводов, пер. с нем., в кн.: Математическая теория логического вывода, M., 1967; К а рр и X. Б., Основания математической логики, пер. с англ., M., 1969. См. также лит. при ст. Правило вывода. Ю. А. Гастев.
Смотреть больше слов в «Большой советской энциклопедии»
Смотреть что такое НАТУРАЛЬНОЕ ИСЧИСЛЕНИЕ в других словарях:
НАТУРАЛЬНОЕ ИСЧИСЛЕНИЕ
исчисление естественного вывода, натуральная дедукция, общее название логических исчислений, введённых и изученных в 1934 немецким логиком Г. Г... смотреть
НАТУРАЛЬНОЕ ИСЧИСЛЕНИЕ
НАТУРА́ЛЬНОЕ ИСЧИСЛЕ́НИЕ (исчисление естественного в ы в о д а) – общее название логич. исчислений [введенных и впервые описанных нем. логиком и мат... смотреть
НАТУРАЛЬНОЕ ИСЧИСЛЕНИЕ
исчисление естественного в ы в о д а) – общее название логич. исчислений [введенных и впервые описанных нем. логиком и математиком Г. Генценом (1934) и польским логиком С. Яськовским (1934) с целью формализации процесса логич. вывода ], более близких к обычным содержательным методам рассуждений, чем различные аксиоматич. формулировки логики высказываний и предикатов исчисления. В соответствии с общепринятыми способами рассуждений, в Н. и. допускается не только вывод истинных предложений из и с т и н н ы х посылок, но и вывод следствий из гипотез. В то время как теоремы аксиоматич. систем логики высказываний и предикатов являются результатом последовательного применения правил вывода к нек-рым исходным истинным формулам (аксиомам), в Н. и. никакие формулы заранее не предполагаются истинными – в Н. и. нет аксиом, а есть лишь правила вывода. Иначе говоря, осн. объектом рассмотрения в Н. и. является отношение выводимости одних предложений (формул) из других. Предложение Н. и., выведенное (по правилам вывода) из к.-л. совокупности формул (посылок, гипотез), будет (как и в обычных исчислениях высказываний и предикатов) теоремой лишь в том случае, если все посылки сами являются теоремами, или же – и этот случай наиболее интересен – когда формула выведена из п у с т о й совокупности посылок, т.е. для установления ее истинности не требуется принятия к.-л. исходных предпосылок. Такие доказуемые в Н. и. формулы естественно считать выражением "логических истин", или законов логики (см. Логическая истинность). Поскольку, однако, ни один из таких законов логики в Н. и. заранее не постулируется, в числе средств Н. и. должно быть правило, позволяющее перейти от в ы в о д а (из гипотез) к д о к а з а т е л ь с т в у, т.е. выводу из пустой совокупности посылок (напр., путем последовательного уменьшения числа посылок). Таким средством получения теорем в Н. и. оказывается т.н. правило введения импликации, согласно к-рому, если предложение (формула) В может быть выведено из предложения (формулы) А по правилам вывода Н. и., то импликация А?В считается доказанной. Правила вывода Н. и. подразделяются на правила в в е д е н и я и у д а л е н и я (или исключения) логич. символов: конъюнкции (&), дизъюнкции (/) импликации (?) и отрицания (). При записи каждого правила вывода над горизонтальной чертой пишутся одна или более посылок (гипотез), каждая из к-рых является либо формулой Н. и. (формулы Н. и. определяются как в обычных исчислениях высказываний и предикатов), либо констатацией факта следования (т. е. выводимости по правилам вывода Н. и.) к.-л. формулы В из формулы А, что обозначается через АВ [соответственно В, где левее знака стоит "пустое множество" формул, означает, согласно сказанному выше, что В доказано в Н. и.; по определению также AA (иногда эта "тривиальная" выводимость принимается в качестве единств. аксиомы Н. и.) ]. Под чертой пишется заключение, полученное из этих гипотез. Классич. Н. и. высказываний может быть, напр., описано при помощи след. логич. правил вывода (здесь А, В и С – формулы, а Г и ? – произвольные конечные, возможно пустые, списки формул): Кроме того, в Н. и. используются т.н. структурные правила вывода, определяющие отношение выводимости: Правила (I) – (III) выражают соответственно сохранение выводимости при усилении посылок, опускании одной из совпадающих посылок, перестановки посылок; правило (IV) ("сечение") есть аналог т.н. правила цепного заключения, согласно которому посылки, вытекающие из других посылок, можно опускать. Н. и. высказываний (а также предикатов) эквивалентно обычному исчислению высказывании (соотв., предикатов) в том смысле, что правила вывода Н. и. являются выводимыми (или постулированными) правилами обычных исчислений, а аксиомы (следовательно, и теоремы) исчислений высказываний и предикатов могут быть доказаны в Н. и. Правило ?-введения Н. и. есть не что иное, как теорема о дедукции "обычных" исчислений. Правило ?-удаления соответствует т.н. правилу зачеркивания, или схеме заключения (modus ponens). Правило /-удаления выражает т.н. доказательство разбором случаев, а правило -введения – т.н. reductio ad absurdum (метод доказательства п р и в е д е н и е м к н е л е п о с т и – см. Доказательство от противного). Содержательная интерпретация остальных правил вывода Н. и., отличающихся от аксиом исчисления высказываний по существу лишь заменой знака импликации на знак выводимости или горизонтальную черту, ясна непосредственно из их внешнего вида. Замена правила -удаления (законад в о й н о г о о т р и ц а н и я классич. логики) на т.н. правило слабого -удаления: A, A / B ("из противоречия выводимо все, что угодно") приводит к и н т у и ц и о н и с т с к о м у (или конструктивному) варианту Н. и. высказываний (см. Интуиционистская логика, Конструктивная логика), а исключение этого правила без всякой замены – к минимальной логике. Здесь Г (х) – список формул Н. и. предикатов, а переменная х, предикат А (х), формула С и терм. t Н. и. предикатов может быть задано независимо от Н. и. высказываний или же – присоединением к правилам вывода последнего нек-рых др. правил, напр. таких: подчинены обычным для исчисления предикатов условиям. Богатый арсенал постулированных правил [среди к-рых, как было сказано, есть, напр., правило, соответствующее дедукционной (мета)теореме, доказательство к-рой в обычных исчислениях, при всей принципиальной простоте, достаточно громоздко ] и возможность вывода из гипотез (с их последующим исключением при помощи правила ?-введения) способствует тому, что пользование Н. и. значительно сокращает и упрощает выводы по сравнению с обычными аксиоматич. системами логики с их зачастую весьма утомительными процедурами вывода из аксиом даже таких простейших "законов логики", как, напр., эквиваленция АНАТУРА?ЛЬНОЕ ИСЧИСЛЕ?НИЕА [формула: АНАТУРА?ЛЬНОЕ ИСЧИСЛЕ?НИЕВ, по определению, есть сокращение для (А?В)&(B?A) ]; в Н. и. эта эквиваленция получается сразу при помощи правил ?-введения и &-введения. Но и в тех случаях, когда при исследовании применяется к.-л. др. логич. система, Н. и. очень удобно для эвристических целей. Формальный аппарат Н. и. близок к введенному также Генценом (в тех же работах, хотя и совсем для др. целей) секвенций исчислению. Близкая к Н. и. техника вывода используется в т.н. семантических таблицах голл. математика Э. Бета. Разл. системы Н. и. разрабатывались также Куайном (1950), нем. математиком К. Шютте (1950) и др. Лит.: Гильберт Д. и Аккерман В., Основы теоретич. логики, пер. с нем., М., 1947; Клини С. К., Введение в метаматематику, пер. с англ., М., 1957, § 20, 23 (термины "Н. и." и "естественный вывод" не используются); Гудстейн Р. Л., Математич. логика, пер. с англ., М., 1961, гл. 1, 2; Gentzen G., Untersuchungen ?ber das logische Schliessen, [Tl ] 1–2, "Math. Zeitschrift", 1934, Bd 39, S. 176–210, 405–31; Ja?k?wskis S., On the rules of suppositions in formal logic (в серии: Studia Logica, 1), Warsz., 1934; Quine W., On natural deduction, "J. Symbolic Logic", 1950, v. 15, No 2, p. 93–102; Beth E. W., Formal methods, Dordrecht–N. Y., [1962 ]; Сurrу H. В., Foundations of mathematical logic, ?. ?., [1963 ]. Ю. Гастев. Москва. ... смотреть