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