06.5. Доказательство как вычисление

Еще в XVII в. Г. В. Лейбниц высказал идею представить логическое доказательство как «игру со знаками». Эта «игра» должна осуществлять­ся по простым правилам, напоминающим правила вычисления в матема­тике и принимающим во внимание только внешний вид знаков. Лейбниц верил, что если это удастся, наступит золотой век, когда с помощью новой логики самые сложные и отвлеченные проблемы будут «вычисляться» так же легко, как в математике вычисляется сумма чисел. Эта програм­ма формализовать доказательство и тем самым перестроить логику по образцу математики намного опережала свое время и начала реализовы­ваться только двести лет спустя.

Строя доказательства, мы опираемся на интуитивную логику и посто­янно обращаемся к содержательному значению используемых понятий, их смыслу. Но смысл — трудноуловимая вещь. Нередко он расплывчат и неопределенен, может истолковываться по-разному и меняться в ходе рассуждения. Чтобы сделать доказательство предельно строгим, нужно свести оперирование смыслами, недоступными наблюдению, к действи­ям над вещественными, хорошо обозримыми объектами. Для этого тре­буется выявить все используемые нами принципы интуитивной логики и представить их в виде простых правил преобразования последователь­ностей знаков, записанных на бумаге. Рассуждение превратится при этом в предметные действия над цепочками знаков.

Метод формализации доказательства состоит в построении исчис­ления, в котором содержательным рассуждениям соответствуют чисто формальные преобразования. Они осуществляются на основании сис­темы чисто формальных (принимающих во внимание лишь внешний вид знаков) правил, а не смыслового содержания входящих в рассуждение утверждений. Полная формализация теории имеет место тогда, когда совершенно отвлекаются от содержательного смысла исходных понятий и положений теории и перечисляют все правила логического вывода, ис­пользуемые в доказательствах. Такая формализация включает в себя три момента: обозначение исходных, неопределяемых терминов; перечисле­ние принимаемых без доказательства формул (аксиом); введение правил преобразования этих формул для получения из них новых формул (тео­рем). В формализованной теории доказательство не требует обращения к каким-либо интуитивным представлениям. Оно является последова­тельностью формул, каждая из которых либо есть аксиома, либо полу­чается из аксиом по правилам вывода. Проверка такого доказательства превращается в механическую процедуру и может быть передана вычис­лительной машине.

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

< Предыдущая		Следующая >