Проблема машинного доказательства математических теорем

Перейдем к следующей актуальной проблеме философии информатики, а именно проблеме машинного доказательства математических теорем.

Для информатики эта проблема имеет практический характер: можно ли запрограммировать машину таким образом, чтобы та самостоятельно создавала для себя другие программы. Например, в комнате стоят стопки кубиков, помеченных буквами А, Б, В. Причем кубик, А стоит на кубике В. Есть робот, который умеет брать кубики в манипулятор и ставить их на пол или на другие кубики. Наша задача — получить башенку вида «А на Б на В». Конечно, можно составить программу вида: «Снять кубик А, поставить Б на В, поставить, А на Б». Но задача не в этом. Задача в том, чтобы создать для робота программу, для которой в качестве входных данных давался бы только конечный результат — башенка определенного вида, но не непосредственная последовательность действий, и эта программа самостоятельно создала бы подпрограмму «как достичь цели, исходя из текущего положения кубиков». В более широком смысле эта задача рассматривается в русле оценки возможности построения «искусственного интеллекта», которая в философии наиболее остро обсуждается во второй половине XX в.

Для решения этой задачи необходимо заложить в работу робота какие-то принципы математической логики. Наиболее подходящее средство предоставляет ее конструктивное направление^[1], поскольку содержание теорем конструктивизм рассматривает не относительно того, что существует, а относительно того, что может быть сделано^[2]. С точки зрения прикладной компьютерной науки, смыслом обладает то, что можно эксплицитно определить или запрограммировать.

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

Перейдем теперь к философской проблематике, обусловленной развитием упомянутых конструктивных форм.

В рамках проблемы машинного доказательства математических теорем особую важность представляет верификация проводимых вычислений. Например, возможно создать программу, которая будет искать доказательство утверждения исходя из заданных аксиом. И это доказательство будет верным, если сама программа написана корректно. Проблема в том, что корректность программы — сама по себе требует доказательства. Корректность этого доказательства тоже можно пробовать доказать программой… и так далее до бесконечности.

Возникает резонный вопрос: можно ли считать доказанным утверждение, доказательство которого существенно опирается на машинные вычисления? Ответ на этот вопрос зависит от определения онтологического статуса компьютерной программы или созданного конструкта. Например, признавая или не признавая компьютерную программу материальным объектом, мы можем принимать или отрицать «машинные» доказательства математических теорем^[3].

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

Остановившись на проблемах и успехах в конструктивистской части информатики, перейдем к проблемам другой ее части — аналитической.

• [1] Подробнее см. гл. 20 данного учебника о дальнейшей судьбе интуиционизма.
• [2] Этому также способствует многообразие интерпретаций интуиционистской логики. Например, колмогоровская интерпретация рассматривается как исчисление проблем [25, с. 235].
• [3] Так, если саму программу и придаваемое ей значение, в корректности которого никогда нельзя до конца быть уверенным, считать лишь плодом фантазии программиста, то и следствия выполнения этой программы, такие как доказательства математических теорем, мы можем с легкостью отрицать. Однако в современную компьютеризированную эпоху этот вопрос имеет намного больше практических следствий. Можно ли считать предсказания или решения (в том числе судебные), основанные на компьютерных вычислениях, легитимными? Кто ответственен за возможные ошибки?