Драгалин А.Г. Конструктивная теория доказательств и нестандартный анализ.
("Математический интуиционизм. Введение в теорию доказательств", и др.)

Оглавление

Предисловие

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

Особенно важной из неклассических логик является, несомненно, интуиционистская логика. Прежде всего, само введение этой логики имеет глубокое и интересное философское обоснование, связанное с интуиционистской критикой классической математики, выдвинутой Брауэром. Кроме того, интуиционистская логика – пожалуй, единственная из неклассических логик, в рамках которой действительно фактически производилась достаточно глубокая разработка многих разделов математики. Интуиционистская логика лежит в основе построения многих математических теорий, базирующихся на различных концепциях конструктивности в математике, и позволяет тонко и точно анализировать трудный и важный вопрос о характере существования объектов исследования в математике. Накопленный здесь опыт свидетельствует о поразительном разнообразии возможных оттенков и вариантов различения эффективности в математике. Представление о практических попытках построения математических теорий на базе интуиционистской логики при том или ином понимании конструктивности можно получить из сводных монографий, например, Гейтинга [3], Гудстейна [1], Бишопа [1], Мартин-Лефа [3], Кушнерa [1]. В последней монографии систематически отражены результаты исследований советской школы конструктивной математики, работающей под руководством чл.-корр. АН СССР А.А.Маркова.

Цель этой небольшой книги – изложить важнейшие из методов теории доказательств в интуиционистской логике. Эта теория сейчас не менее богата методами и результатами, чем, например, пользующаяся заслуженной известностью классическая теория моделей. Автор стремился познакомить читателя с основными аксиоматическими теориями, основанными на интуиционистской логике, и их особенностями, часто весьма непривычными даже для специалиста-логика, но привыкшего иметь дело с классической логикой. Можно надеяться, что и специалист по неклассическим логикам обнаружит в книге некоторые новые результаты и методы.

Автор прилагал усилия, чтобы сделать изложение доступным для возможно более широкого круга читателей. От читателя требуется определенная математическая культура и готовность терпеливо восполнять недостающие рутинные шаги в многочисленных индуктивных доказательствах. Что касается логики, то достаточно владеть вводным в классическую математическую логику курсом. Учебник Мендельсона [1], например, содержит все необходимые сведения. Знакомство с литературой по интуиционистской логике, в особенности с книгой Гейтинга [3] и Клини и Весли [1], является желательным, но не необходимым. Возможно, при первом чтении книги читатель пожелает получить представление о различных интуиционистских теориях и способах их исследования и при этом избежать длинных и утомительных доказательств. В такой ситуации можно ограничиться чтением объяснительного текста, определений и формулировок теорем, а часть пятую и оба дополнения можно опустить. Однако для более полного овладения предметом следует, конечно, тщательно проработать доказательства. Книга не содержит специальных упражнений, но построена так, что проведение всех рутинных деталей составляет определенную самостоятельную работу, являющуюся органической частью тщательного изучения книги. Автор надеется, что овладение материалом книги подведет читателя к самостоятельным исследованиям в рассматриваемой области и позволит ему ориентироваться в журнальной литературе по специальности.

При написании книги некоторая проблема состояла в выборе стиля изложения: если излагаются и изучаются различные теории конструктивности в математике, то должен ли сам автор придерживаться в этом изложении некоторой конструктивной точки зрения? Был выбран компромиссный путь. Изложение принципиально не связано с какими-либо ограничениями и временами и является обычным теоретико-множественным рассуждением, таким же, какие употребляются при изложении "обыкновенных" содержательных математических теорий вроде топологии или теории меры. Вместе с тем автор старался, по возможности, избегать неконструктивных способов рассуждения и в особенно ответственных случаях (см., например, ч. 5) эта тема специально обсуждается и прилагаются особые усилия. Тем не менее никак нельзя сказать, что все изложение в книге выдержано в некоторых идейно последовательных интуиционистских рамках, – возможно, потому, что автор знаком со многими интересными интуиционистскими концепциями и искренне не знает, какой из них отдать предпочтение. Мы предпочтем изучать сами эти концепции аксиоматическим методом. Вo всяком случае, читатель, если того пожелает, всегда может считать, что книга представляет собой "взгляд на конструктивную математику с точки зрения классической", хотя такое мнение и не отразит полностью стремления автора не избегать теоретико-множественного изложения, но и не искать его там, где без него можно легко обойтись.

В книге частично представлено содержание нескольких курсов по интуиционистской математике, которые автор читал в течение ряда лет на механико-математическом факультете МГУ. Книга содержит пять частей и два дополнения. В первой части излагаются чисто синтаксические методы исследования интуиционистской логики предикатов, основанные на теореме Генцена об устранении сечения. В частности, доказана теорема Харропа о свойствах дизъюнктивности и экзистенциальности логики предикатов. Более сильный алгоритмический вариант теоремы Генцена с гораздо более сложным доказательством вынесен в дополнение Б. Во второй части, посвященной интуиционистской арифметике, основным инструментом исследования является принадлежащий Клини метод реализуемости. Здесь автор стремился подчеркнуть возможность принципиально различных алгоритмических истолкований логических связок. В третьей части рассматривается теория алгебраических моделей интуиционистской логики и, в частности, доказываются теоремы о полноте для различных вариантов таких моделей. Вновь на примере интуиционистской арифметики показывается полезность введенных понятий для исследования конкретных теорий. В четвертой части, относящейся к интуиционистскому анализу, основное внимание уделено обсуждению принципов интуиционистского анализа и обзору современных результатов в этой области. Превосходное изложение двух моделей типа реализуемости для анализа можно найти в монографии Клини и Весли [1]. Мы приводим две алгебраические модели для различных вариантов интуиционистского анализа. Наконец, в пятой части алгебраические модели используются для решения важной задачи синтаксического характера: теоремы об устранении сечения в интуиционистской логике высокого порядка. Показано, что решение этой задачи принципиально не может быть достигнуто элементарными синтаксическими методами. В дополнении А описывается класс структур, позволяющий с единых алгебраических позиций рассмотреть как алгебраические модели, так и модели типа реализуемости.

Автор благодарит своего учителя А.А.Маркова за внимание к своей работе, а слушателей своих спецкурсов за их постоянный энтузиазм и ценные замечания. При подготовке рукописи к печати мне помогали И.А.Ломакина, Ю.В.Гавриленко, Е.С.Божич, которым автор выражает свою искреннюю признательность.

Об авторе

Видный представитель российской школы математического конструктивизма. Родился 10 апреля 1941 года на острове Моржевец Архангельской области. Окончил механико-математический факультет МГУ им.М.В.Ломоносова, где работал с 1966 года. С 1983 года жил в Венгрии, заведовал кафедрой вычислительной математики университета им.Л.Кошута (г.Дебрецен). В 1988 году Венгерской Академией наук ему была присвоена степень доктора наук. Умер 18 декабря 1998 года в г.Дебрецен.

А.Г.Драгалин – автор фундаментальных трудов по теоретико-модельным и теоретико-доказательственным основаниям интуиционистской логики, конструктивным методам нестандартного анализа.

Опечатки

К читателю

Издательство URSS первоначально планировало публикацию двухтомника избранных трудов А.Г.Драгалина и А.Н.Колмогорова по логике и философии математики, во второй том которого был включен учебник А.Н.Колмогорова и А.Г.Драгалина "Математическая логика". Перед самым выходом первого тома в издательство обратились от имени Ученого совета механико-математического факультета МГУ и предложили опубликовать учебник А.Н.Колмогорова и А.Г.Драгалина в серии "Классический университетский учебник", на что наше издательство дало согласие. Первый том вышел под названием: Драгалин А.Г. Конструктивная теория доказательств и нестандартный анализ. Ссылки на второй том, сохранившиеся по техническим причинам в тексте этой книги (см. с.11, 15, 354, 453, 471, 482), следует рассматривать как относящиеся к изданию: Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия: Классический университетский учебник.