Akademik

(исчисление естественного в ы в о д а) – общее название логич. исчислений [введенных и впервые описанных нем. логиком и математиком Г. Генценом (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 ].