Игошин Математическая логика и теория алгоритмов (1019110), страница 77
Текст из файла (страница 77)
Затем логические принципы, употреблявшиеся в теории для получения новых фактов, формализуются в виде аксиом и чисто формальных правил вывода, позволяющих выводить новые формулы языка й из аксиом и уже выведенных формул. Таким образом возникает формальная аксиоматическая теория (или, иначе, формальная система, исчисление Т*,, точно описывающая некоторый интересующий нас фрагмент содержательной теории Ть Существенно при этом, что формулировка Т," не требует исчерпывающего проникновения в, быть 308 может, весьма сложную семантику теории Ть Исчисление Т, строится по простым законам как чисто знаковая система, и для понимания устройства этой знаковой системы нет необходимости вникать в смысл выводимых в ней формул. Такой подход открывает возможность строго математически сформулировать интересуюшие нас проблемы, относящиеся к выводимости некоторых формул в Т;.
Кроме того, он дает возможность исследовать формальную теорию Т," средствами некоторой содержательной теории Ть В этой ситуации Т, *называется лредметнойтеорией, а Т, — ее метатеорией. С точки зрения оснований математики важно, чтобы Т, была в некотором отношении более надежной теорией, чем Т„так что исследование Т; средствами теории Т, можно было бы действительно рассматривать как разъяснение и обоснование неясных деталей семантики Т, с помощью более убедительной теории Тъ Если же нас интересует не столько вопрос об интуитивной ясности Т„сколько просто факт о выводимости или невыводимости некоторых формул в Т,*, то Т; может исследоваться средствами любой исторически сложившийся и убедительной для исследователя математической теории Тп Один из важнейших вопросов о теории Т,* есть вопрос о ее формальной непротиворечивости, который состоит в выяснении того, существует ли в языке й такая формула Г, что сама Г и ее отрицание — Г являются теоремами теории Т, "(что равносильно выяснению вопроса о том, всякая ли формула языка й является теоремой теории Т;).
Метаматематический метод доказательства непротиворечивости, предложенный в начале ХХ в. Гильбертом, состоит в том, что утверждение о непротиворечивости формальной системы Т,* рассматривается как высказывание о возможных в этой системе доказательствах. Само же это высказывание уже принадлежит метатеории Т„которая и исследует это утверждение. Такой подход сводит вопрос о непротиворечивости Т,* к вопросу непротиворечивости другой теории Т,. При этом говорят, что Т, *непротиворечива относительно Т,. Большое значение имеет вторая теорема Геделя, которая утверждает, что непротиворечивость формальной теории, содержащей формальную арифметику, невозможно доказать с помощью средств самой рассматриваемой теории (при условии, что эта теория действительно не- противоречива).
Примером применения метаматематического метода может служить доказательство Г. Генцена непротиворечивости формальной арифметики, полученное им в 1936 г. и использующее трансфинитную индукцию — средство, выходящее за рамки формальной арифметики. Существует и другой путь доказательства непротиворечивости формальной системы, идущий через понятие интерпретации и модели. Формальная система называется содержательно (или се- 309 мантически) непротиворечивой, если существует модель, в ко торой истинны все теоремы этой системы. Без труда устанавлива ется, что если формальная система содержательно непротиворечива, то она формально непротиворечива.
Для формальных систем, основанных на классическом исчислении предикатов 1-го порядка, справедливо и обратное утверждение (теорема Геделя о модели): всякая непротиворечивая формальная теория имеет модель. Таким образом, другой способ доказательства непротиворечивости формальной теории состоит в построении ее модели. Но и этот метод является относительным: он устанавливает непротиворечивость одной формальной системы относительно другой, в терминах которой построена модель первой. Можно, далее, исследовать аналогичным образом и метатеорию Ть построив формальную систему Т,* и изучая уже Т2' средствами следующей содержательной теории Т„ которая будет метатеорией по отношению к теории Т, и метаметатеорией по отношению к теории Ть О границах аксиоматического метода, метода формализации и логики.
Насколько универсален и насколько всемогущ аксиоматический метод и его наивысшее математическое выражение — формализация? Прежде всего, границы методу формализации были поставлены двумя выдающимися теоремами К. Геделя, доказанными им в 1931 г.
Первая из них утверждает, что для всякой непротиворечивой формальной системы, содержащей аксиомы формальной арифметики, можно дать явное описание замкнутой формулы г", такой, что ни сама эта формула, ни ее отрицание г" не выводимы в этой формальной системе. Вторая теорема утверждает, что при выполнении некоторых естественных условий в качестве г можно взять утверждение о непротиворечивости данной формальной системы, т.е. в непротиворечивой формальной системе, включающей формальную арифметику, содержится формула, выражающая ее непротиворечивость, и что эта формула недоказуема в этой системе.
Доказательство этих утверждений ознаменовало собой строгое математическое установление того факта, что гильбертовская программа формализации математики не может быть реализована в том виде и в том объеме, в каких ее мыслил Гильберт. Эти теоремы Геделя фактически означали, что истинное утверждение не всегда может быть доказано. Эти логические теоремы по существу разрушали восходящее к Лейбницу и Декарту мнение, будто всякое истинное утверждение подвластно обоснованию методами математического доказательства. Но оставалась надежда, что выводимость ненамного меньше истинности, что недоказуемыми являются лишь экзотические формулы геделевского типа, в которых зашифрованы утверждения, относящиеся к самим этим формулам.
Однако результаты, полученные А.Тарским в 1936 г., 310 окончательно разрушили и эту последнюю надежду (см. более подробно об этом в Заключении). Конечно, эти результаты, показывающие, что расстояние от доказуемости (выводимости) до истинности столь велико, могут служить солидным основанием для значительной доли пессимизма в оценке роли логики (и в частности, математической логики) в процессе познания окружающего мира и истины. Некоторые определенные философы истолковывают эти результаты как полное отрицание роли логики в процессе познания, считая, что она нужна лишь для придания уже полученным результатам общепонятной и убедительной формы, а сам механизм получения этих результатов совершенно иной. Не следует истолковывать эти результаты и как полный крах формального подхода к математическим теориям. Эти результаты несомненно означают, что первоначальная «максималистская» гильбертовская программа финитистского подхода к обоснованию математики не может быть реализована в полном объеме: нельзя построить математику как некоторую фиксированную совокупность средств, которые можно было бы объявить единственно законными, и с их помощью строить метатеории любых теорий.
Невозможность полной формализации содержательно определенных математических теорий — это не недостаток подхода или концепции, а объективный факт, неустранимый никакой концепцией, «суровая правда» об устройстве мира, изучаемого этой теорией. Невозможность адекватной формализации теории означает, что надо либо искать формализуемые ею фрагменты, либо строить какую-то более сильную формальную теорию, которая, правда, снова будет неполна, но, быть может, будет содержать всю исходную теорию. Рассматриваемые выдающиеся результаты Геделя и Тарского демонстрируют не только слабость математической логики в процессах познания, но и ее силу, еще раз являя уникальность этой науки.
Она единственная из всех наук своими собственными строгими методами устанавливает границы своей применимости. Фактически средствами математической логики устанавливаются границы применимости математики. Наука с такими уникальными возможностями не может быть бесполезна для дела познания окружающего мира, и, думается, что ее будущие результаты заставят еще не раз как математиков, так и философов обратиться к их интерпретации.
Глава У11 ЭЛЕМЕНТЫ ТЕОРИИ АЛГОРИТМОВ В предыдущих главах неоднократно использовались термины, «алгоритм», «эффективная процедура». Настоящая глава посвящается уточнению и изучению этого понятия.. В' в 31 более детальке обсуждается понятие алгоритма ны интуитивной основе и: устанавливается необходимость его утачнания, в 32 посвящен изучению одного из возможных угочиений. ёанятия алгоритма — ма шинам Тьюринга, в В 33 и, В 34 дан обзор других возможных, уточнений понятия алгоритма — рекурсивных функций и нормальных алгоритмов Маркова.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
