Доказуемое и недоказуемое - Манин Ю.И.
Скачать (прямая ссылка):
Тем не менее в системах Рассела—Уайтхеда, Куайна и других авторов формализация языка свойств в «теориях типов» использовалась именно для обоснования теории множеств. Прагматическая цель состояла в таком ограничении универсума и языковых средств, чтобы сделать невозможным появление парадоксов расселовского типа.
«Реальностью» для теории типов является универсум, состоящий из индивидуумов (нулевого типа), их свойств (первого типа), свойств их свойств (второго типа) и т. д. до бесконечности. Парадокс Рассела не воспроизводим, ибо свойство «быть свойством, не обладающим самим собой» универсуму не принадлежит. В этом универсуме, однако, интерпретировать классическую математику неудобно уже на уровне языка и почти невозможно на уровне аксиом существования: постулируемая Расселом специфическая «аксиома сводимости» не удовлетворяла его самого. Варианты теории типов связывают, с «логицистическим» тезисом, согласно которому математика сводима к логике, по историческим и интуитивным причинам, сам этот тезис едва ли обладает четким содержанием (см. Клини [3]).
В интуиционистской математике место как «множества», так и «свойства» примерно занимает выражение «закон образования», однако, принципиальная установка интуиционизма на несущественность «внешнего смысла» их текстов, в частности неадекватность любой из формализации, мешает вести это сопоставление слишком далеко.
Для Брауэра и его школы интуиционизма предметом первоначальной интуиции является ряд целых чисел 0, 1, 2, 3..., при этом рассматриваемый не как завершенный, но как становящийся посредством закона перехода от п к л+1. Соответственно индукция принимается как основной прообраз всех конструкций, допустимых в математике. Сами по себе конструкции должны осуществляться финитными средствами над финитными объектами, и существование математического объекта понимается как возможность построить его. Это исключает доказательства существования «от противного», не сопровождаемые предъявлением соответст-
11*
155
вующега объекта в случае, когда он должен выбираться из потенциально бесконечного множества. Это — известный принцип неприменимости закона исключенного третьего в бесконечных областях.
Континуум Брауэра представляет собой с трудом эксплицируемую в классических терминах «среду свободного становления»,, скажем, десятичных дробей, не актуально, а лишь потенциально бесконечных, причем, однако, выбор последовательных десятичных знаков не подчинен никакому закону.
Кронекер был первым проповедником ограничений, которые подобная точка зрения налагает на математику, и одним из самых влиятельных противников Кантора. Брауэр и его последователи приложили много усилий к тому, чтобы прояснить контуры интуиционистской математики и логики, оазвивая ее положительные принципы. Однако они, в частности Гейтинг, постоянно подчеркивали примат внутренней интерпретации математических текстов н ограниченные возможности передачи ее в однозначно понимаемых аксиоматических теориях. С этих философских позиций отсутствие готовности принять внутреннюю интерпретацию теории множеств в духе Кантора может показаться необъяснимым: многие математики признают внутреннюю интерпретацию теории множеств в полном объеме. Для объяснения интукционисты привлекают психологические аргументы в пользу примата идеи расчлененности, прерывности и, стало быть, потенциальной счетности в качестве единственно законного типа бесконечности. Интуиционистам не дужды и апелляции к «реалистическому» смыслу математики, в одной из статей Брауэр утверждает, что применение принципа исключенного третьего в естественных науках зависит от свойств конечности и дискретности физического мира.
Конструктивизм школы А. А. Маркова начал оформляться в конце 40-х годов, как вариант интуиционизма, использующий уточнения понятий конструктивного объекта и алгоритма на базе теории рекурсивных функций либо ее вариантов. Не вдаваясь здесь в подробности определений, укажем лишь на некоторые характерные принципиальные установки этой школы.
«Реальность» конструктивистов составляют тексты в конечных алфавитах, подвергаемые процессам переработки, которые алго-ритмичны, в частности также описываемы текстами в конечном алфавите.
Потенциальная бесконечность допускается как абстракция текстов заранее не ограниченной длины и алгоритмов, работающих заранее не ограниченное время; актуальная бесконечность отвергается.
Существование математического объекта трактуется либо как •его предъявление, либо как возможность построить его алгориф-мически. Существенная тонкость состоит в том, что по А. А. Маркову возможность алгорифмического построения сама по себе мо-
156
жет устанавливаться классическими средствами, а не исключительно предъявлением такого построения. В частности, в таких доказательствах может использоваться редукция к противоречию.
Конструктивный континуум представлен парами алгорифмов, из которых первый задает вычислимую последовательность Коши рациональных чисел, а второй —? явные оценки скорости сходимости (в классическом смысле). С точки зрения классической математики конструктивный континуум счетен, сверх того, а) свойство пары алгорифмов определять вещественное число алгорифмически неразрешимо; б) свойство двух таких пар определять одно и то же число неразрешимо; точно так же неразрешимо свойство представлять данное число. По этим причинам конструктивный анализ резко отличается от обычного. Например, в качестве функций вещественной переменной рассматриваются алгорифмы, переводящие конструктивное вещественное число в другое такое же число. Но тогда такая простая функция, как }(х)=—1 при х^О, /(х)= 0 при х>0, не существует в конструктивном анализе, ибо иначе было бы разрешимо свойство числа «быть нулем». В действительности, все конструктивные функции непрерывны в классическом смысле слова.
