Страница 37

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

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

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

  Более того, оказалось (К. Гёдель, 1931), что задача полной и одновременно непротиворечивой формализации даже таких относительно простых математических теорий, как арифметика (теория чисел), в принципе неосуществима, так что в них всегда имеется некоторый «неформализуемый остаток» (см. также Аксиоматическая теория множеств). Наконец, никакая формализация дедуктивных теорий не снимает проблемы их интерпретации, т. е. соотнесения с некоторой описываемой ими и внешней для них реальности (также, быть может, состоящей из объектов высокой степени абстракции), адекватность которого только и может быть в конечном счёте обоснованием истинности теории в целом. Естественно, что в рамках математической логики приобретает всё большее влияние та часть доктрины (альтернативной по отношению к гильбертовской концепции) математического интуиционизма (в значительной мере воспринятой представителями конструктивного направления), согласно которой понятие строгого математического Д. (не говоря уже об общем понятии Д.) вообще не может быть исчерпано никаким «раз навсегда данным» формальным определением.

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

  О некоторых специальных видах и методах Д. см. Доказательство от противного, Косвенное доказательство, Опровержение логическое.