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

Противопоставление содержательных и формальных аспектов понятия «Д.» проявляется прежде всего в различии широкого и узкого понимания этого термина.

Д. в широком смысле — это любая процедура установления истинности какого-либо суждения (называется тезисом, или заключением, данного Д.): как при помощи некоторых логических рассуждений, так и посредством чувственного восприятия некоторых физических предметов и явлений, а также ссылок (указаний или упоминаний) на такие восприятия. Именно такой характер имеют Д. в юридической практике, где термин «Д.» применяют к такого рода единичным указаниями даже для наименования самих указываемых предметов — отсюда выражения «предъявить Д. (улику)», «вещественное Д.». Таковы и обоснования большей части утверждений гуманитарных наук, а в ещё более отчётливой форме — эмпирические (опытные: экспериментальные или основанные на данных наблюдений) Д. в естественных науках. Хотя все такие Д. (если не считать Д. некоторых единичных фактов, сводящихся к непосредственному умозаключению из однократного «предъявления улики») включают в качестве составных частей дедуктивные фрагменты — умозаключения , связывающие ссылки на опыт с доказываемым (и промежуточными) тезисом, тем не менее все эти Д. можно считать индуктивными: в них имеет место переход от частных посылок к общим заключениям ( индукция ), совершаемый (чаще всего в неявной форме) по правилам индуктивной логики.

Д. в узком смысле слова, характерные для дедуктивных наук (логики, математики и построенных по их образцу и на их основе разделов теоретической физики и теоретической кибернетики), представляют собой цепочки умозаключений (правильных), ведущих от истинных посылок (исходных для данного Д. суждений) к доказываемым (заключительным) тезисам. Посылки Д. также именуются его основаниями, или аргументами, или доводами; термины эти, однако, не менее часто применяются для обозначения промежуточных переходов от посылок к заключению или всякого рода пояснений (комментариев), сопровождающих такие переходы в подобных Д. Истинность посылок не должна обосновываться в самом Д., а должна каким-либо образом устанавливаться заранее. Последовательное развитие этой традиционной (идущей от Аристотеля) концепции Д., связанное с аксиоматическим методом , потребовало (в конце 19 в.) существенного её уточнения и даже пересмотра. Если принятие аксиом в качестве истинных предложений ещё согласовывалось с классическими представлениями (достаточно было, казалось, потребовать их эмпирического обоснования), то открытие возможности построения различных аксиоматических систем (например, неевклидовых геометрий), пригодных, по крайней мере в принципе, для описания одной и той же физической реальности, заставило отбросить представление об аксиомах и как об «истинах самоочевидных», и как об эмпирических истинах. Такое представление (идущее ещё от греческой науки) противоречило, как оказалось, возможности принимать в качестве аксиом различных конкретных геометрических систем (но, конечно, не одной и той же системы) утверждения, являющиеся отрицаниями друг друга, и открывшейся в связи с этим возможности класть в основу научных теорий (а тем самым — и в качестве посылок Д.) предложения, вопрос об истинности которых не только не предопределён с самого начала, но может даже и не ставиться. Иначе говоря, обнаружилась относительность противопоставления понятий вывода (из гипотез ) и Д. — ведь аксиомы (независимо от их гипотетической «истинности» или «ложности») это и есть гипотезы, на которых основывается Д.

Но этот пересмотр понятия Д., произведённый на рубеже 19 и 20 вв. Д. Гильбертом , не был до конца последовательным. В связи с обострившимися проблемами непротиворечивости научных теорий (уверенность в которой уже не могла больше базироваться на уверенности в истинности исходных положений теории), Гильберт выдвинул программу формализации Д. дедуктивных теорий, предполагающую не только явное указание всех исходных понятий и исходных предложений (аксиом) каждой данной теории, но и такое же явное указание всех используемых в выводах (в частности, в Д.) этой теории логических средств. При такой постановке вопроса проблема убедительности (правильности) Д. получает (впервые!) совершенно объективный характер. Д. (точнее, формальное Д.) рассматривается просто как «строчка формул», каждая из которых есть либо аксиома (т. е. принадлежит к некоторому заранее выделенному списку «отмеченных» формул), либо непосредственно следует по одному из правил вывода (также точно перечисленных) из предыдущих формул строчки. Заключение данного Д. — это просто его последняя формула (в частности, Д. любой аксиомы состоит всего из одной формулы — из неё самой). При такой трактовке рассматриваемая научная теория перестаёт быть теорией в привычном смысле: она оказывается представленной в виде исчисления , или формальной системы , состоящей из формул, получающихся из формул некоторого исходного запаса (аксиом) посредством чисто «механического» применения правил вывода (применение которых, равно как и проверка правильности этого применения, не предполагает никакого «содержательного» их понимания). Формула, для которой существует формальное Д., называется доказуемой формулой, или формальной теоремой.

Т. о., реализация этой части гильбертовской программы позволила осуществить идеал, выдвинутый ещё Г. В. Лейбницем : «заменить рассуждение вычислением». Для проверки того обстоятельства, является ли данная строчка формул Д., существует простой, единообразный и притом чисто механический метод — алгоритм . Для выяснения того, является ли произвольная данная формула теоремой, такой алгоритм возможен лишь для немногих, относительно простых формальных теорий, но это обстоятельство не исключает возможности машинного поиска вывода (поиска Д.) для многих важных классов формул, и разработка таких машинных алгоритмов вывода является одним из перспективных направлений математической логики, теории алгоритмов и теоретической кибернетики.

Представление Д. в виде строчек (линейных последовательностей) формул — не единственно возможное; часто бывает удобнее определять формальные Д. как «деревья» формул, «ветвями» которых служат посылки применений правил вывода. Такая форма Д. оказалась, в частности, удобной для предпринятых в рамках гильбертовской теории доказательств немецким математиком Г. Генценом (1934) исследований логических выводов; в предложенных им модификациях логических исчислений в виде так называемых исчислений «естественного вывода» формальные логические средства ближе по своей структуре к обычным (содержательным) методам умозаключений, нежели в первоначальной гильбертовской схеме. Аксиом в этих исчислениях нет (или совсем мало), но введены дополнительные правила вывода, так что в результате общий «запас теорем», выводимых новыми и прежними средствами, оказывается одним и тем же. Т. о., различие между формальными аксиомами и содержательными правилами оказывается также относительным.