аксиоматизация геометрии, однако в современной математике почти все математические теории строятся на аксиоматической основе. В математической логике описывается специальный язык формул, позволяющий любое предложение математической теории записать в виде вполне определенной формулы.
Пользуясь терминологией, введенной выше при рассмотрении ассоциативных исчислений, можно сказать, что всякая такая формула представляет собой слово в некоторое специальном алфавите, содержащем наряду с употребительными в математике знаками вроде букв, скобок и т.д., еще и другие специальные знаки, изображающие логические операции, например отрицание, дизъюнкция и т. д. Однако главная аналогия с ассоциативными исчислениями заключается в том, что сам процесс логического вывода из какой-нибудь посылки R следствия S может быть описан в виде процесса формальных преобразований слов, очень сходных с допустимыми подстановками в ассоциативном исчислении. Это позволяет говорить о логическом исчислении, о котором указана система допустимых преобразований, изображающих элементарные акты логического умозаключения, из которых складывается любой сколь угодно сложный формально-логический вывод. Примером такого допустимого преобразования является вычеркивание в формуле двух рядом стоящих знаков отрицания; скажем, «ненекрасивый» может быть преобразовано в «красивый».
Вопрос о логической выводимости предложения S из посылки R в оказанном логическом исчислении становится вопросом о существовании дедуктивной цепочки, ведущей от слова, изображающего посылку R, к слову, изображающему предложение S. Проблему распознавания выводимости можно теперь сформулировать так.
Для любых двух слов (формул) R и S в логическом исчислении узнать, существует дедуктивнаяцепочка, ведущая отR к S, или нет.
Решение понимается в смысле алгоритма, дающего ответ на любой из вопросов такого типа (любые R и S).
Нетрудно теперь сообразить, что создание такого алгоритма позволило бы получить общий разрешающий метод для автоматического решения самых разнообразных задач из всех математических теорий, которые построены аксиоматически. Действительно, справедливость какого-нибудь утверждения S (например, формулировка какой-нибудь теоремы) в такой теории понимается как его логическая выводимость из системы аксиом, взятой в качестве посылки R. Но тогда, применяя алгоритм распознавания выводимости, можно было бы установить, справедливо ли это утверждение S в рассматриваемой теории или нет. Более чего, в случае утвердительного ответа можно было бы эффективно найти в логическом исчислении соответствующую дедуктивную цепочку, а по ней восстановить цепь умозаключений, составляющих доказательство рассматриваемого утверждения. Фактически, предполагаемый алгоритм решил бы единым эффективным методом почти все сформулированные и еще не решенные до сегодняшнего дня математические проблемы. Это обстоятельство делает понятным не только заманчивость построения такого «всеобщего алгоритма», а значит, и построения соответствующей «всемогущей машины», но и трудности такого построения.
И действительно, несмотря на долгие и упорные усилия многих крупных
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.